IndisputableMonolith.RecogGeom.Composition
The Composition module defines the composite of two recognizers acting on the product of their configuration spaces, realizing RG6 in Recognition Geometry. Researchers formalizing geometric recognition models or building effective manifolds cite it when extending quotient constructions to products. The module supplies the core CompositeRecognizer definition together with basic equality and refinement lemmas.
claimLet $R_1 : C_1 / {}_1$ and $R_2 : C_2 / {}_2$ be recognizers with their respective indistinguishability quotients. Their composite $R_1 R_2$ is the recognizer on the product space $C_1 times C_2$ whose events are pairs of events from $R_1$ and $R_2$, with the induced indistinguishability relation.
background
The module imports the recognition quotient $C_R = C / sim$ from Quotient, where $sim$ collapses configurations indistinguishable by the recognizer. CompositeRecognizer is the central definition; the sibling lemmas composite_R_eq, composite_indistinguishable_iff, composite_refines_left and composite_refines_right establish its basic algebraic properties. The local setting is Recognition Geometry, whose three pillars (as stated in Foundations) rest on quotients, composition, and dimension extraction.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Composition supplies the product-space operation required by Dimension for recognition dimension and by EffectiveManifold for the U1-U4 structural conditions. It is cited as RG6 in DraftV1 and feeds the integration summary in Integration and the RSBridge link to the eight-tick cycle. The module closes the gap between single-recognizer quotients and multi-recognizer geometry.
scope and limits
- Does not construct the full effective manifold from the composite.
- Does not derive dimension formulas or the eight-tick octave.
- Does not connect to Recognition Science constants or the phi-ladder.
- Does not treat infinite or continuous families of recognizers.
used by (7)
depends on (1)
declarations in this module (19)
-
def
CompositeRecognizer -
theorem
composite_R_eq -
theorem
composite_indistinguishable_iff -
theorem
composite_refines_left -
theorem
composite_refines_right -
theorem
composite_distinguishes -
theorem
composite_resolutionCell -
theorem
composite_cell_subset_left -
theorem
composite_cell_subset_right -
def
quotientMapLeft -
def
quotientMapRight -
theorem
quotientMapLeft_surjective -
theorem
quotientMapRight_surjective -
theorem
refinement_theorem -
theorem
composite_comm_events -
theorem
composite_comm_indistinguishable -
theorem
composite_info_monotone_left -
theorem
composite_info_monotone_right -
def
composition_status