indistinguishable_status
plain-language theorem explainer
This definition assembles a status string confirming completion of the indistinguishability relation and its properties under a recognizer map in Recognition Geometry. Researchers auditing the Recognition Science formalization cite it to verify that RG3 has been established with the required equivalence and partition structures. The construction is a direct string concatenation of fixed completion messages for each subcomponent.
Claim. The module status is the string affirming that the indistinguishability relation on configurations, defined by equality of events under the recognizer map, has been shown to be an equivalence whose classes form resolution cells that partition the space.
background
Recognition Geometry starts from a recognizer map R from configurations C to events E. Indistinguishability is the relation where two configurations are related precisely when they map to the same event; this is an equivalence relation whose classes are the resolution cells, the smallest units distinguishable by R. The module also defines LocalResolution as the induced partition of any subset U and Distinguishable as the negation of the relation.
proof idea
The definition is a direct string concatenation of fixed messages, each reporting completion of one subcomponent: the indistinguishability definition, the equivalence theorem, the resolution cell and fiber equalities, the partition property, and the local resolution and distinguishability definitions.
why it matters
This status definition marks completion of axiom RG3, the statement that recognition is lossy and therefore induces equivalence classes on configurations. It confirms the geometric foundation for resolution cells that later layers of the framework rely upon. The module documentation states that these classes are the smallest units of configuration that can be told apart by the given recognition map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.