IndisputableMonolith.RecogGeom.Composition
The Composition module defines the composite of two recognizers acting on product spaces, realizing RG6 in Recognition Geometry. Dimension and EffectiveManifold authors cite it when building refined quotients from pairs of recognizers. The module supplies the CompositeRecognizer definition together with equality and indistinguishability lemmas that follow directly from the underlying quotient construction.
claimGiven recognizers $R_1$ and $R_2$, the composite $R_1 ullet R_2$ yields events in the product space $C_{R_1} imes C_{R_2}$ with the induced indistinguishability relation on the product quotient.
background
The upstream Quotient module constructs the recognition quotient $C_R = C / \sim$ where $\sim$ is the indistinguishability relation induced by recognizer $R$. This module extends that construction to pairs by introducing CompositeRecognizer, which maps a pair of configurations to a joint event. The local theoretical setting is the development of geometric operations on recognition quotients that later support dimension extraction and manifold refinement.
proof idea
This is a definition module. It introduces CompositeRecognizer and proves supporting statements (composite_R_eq, composite_indistinguishable_iff, composite_refines_left, composite_refines_right) by direct appeal to the quotient equivalence relation imported from Quotient.
why it matters in Recognition Science
The module supplies the composition operation required by the Recognition Geometry framework and is imported by Dimension, EffectiveManifold, Foundations, Integration, RSBridge, and ZornRefinement. It realizes the RG6 statement given in the module documentation and thereby feeds the fundamental theorems collected in Foundations and the bridge to Recognition Science.
scope and limits
- Does not derive the Recognition Composition Law from the J-function.
- Does not treat infinite or continuous families of recognizers.
- Does not connect the composite to the phi-ladder or mass formulas.
- Does not establish uniqueness of the composite up to canonical isomorphism.
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