quotient_status
plain-language theorem explainer
quotient_status defines a fixed string that reports completion of the recognition quotient C_R = C/~ together with its projection, event map injectivity, and lifting operations. Researchers auditing the Recognition Geometry layer cite this marker to confirm that indistinguishability classes have been collapsed without loss of observable structure. The definition is a direct string concatenation with no lemmas or computation.
Claim. The status string asserts that the recognition quotient $C_R = C/{~}$ (where $c_1 {~} c_2$ iff $R(c_1) = R(c_2)$), the canonical projection $π : C → C_R$, the induced event map $R̄ : C_R → E$, and the lifting and neighborhood constructions are all defined and satisfy the listed properties.
background
The module RecogGeom.Quotient builds the quotient type RecognitionQuotient as the set of equivalence classes under the indistinguishability relation induced by a recognition map R : C → E. Key sibling definitions include recognitionQuotientMk (the class constructor), quotientEventMap (the induced map to events), quotientEventMap_injective (injectivity of the induced map), and liftToQuotient (lifting of functions through the quotient). The local setting is given by the module documentation: given R, one forms C_R = C/~ with c₁ ~ c₂ precisely when R(c₁) = R(c₂). Upstream results such as LinearLogicBridge.eval supply resource evaluation used in related ledger constructions, while SpectralEmergence.E defines the edge count |E| = D · 2^(D-1) that appears in the event space.
proof idea
The definition is a direct string concatenation that lists eight status lines verifying the quotient construction, the projection, the equivalence relation, the event map, its injectivity, the equivalence to the image, the lifting operation, and the induced neighborhoods, followed by a completion banner. No tactics or lemmas are applied; the body is a literal string.
why it matters
This definition serves as the terminal status marker for the entire RecogGeom.Quotient module, confirming that the recognition quotient construction is complete and ready for use in higher Recognition Science layers. It directly supports the summary theorem recognition_quotient_summary that asserts surjectivity of recognitionQuotientMk and injectivity of quotientEventMap. Within the framework it closes the geometric quotient step that precedes spectral and mechanism-design constructions, aligning with the indistinguishability collapse required before the eight-tick octave and D = 3 emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.