pith. sign in
module module high

IndisputableMonolith.RecogGeom.Integration

show as:
view Lean formalization →

The Integration module supplies the central type-theoretic definition of a complete recognition geometry by assembling all prior structures from its imported submodules. Researchers building global models in Recognition Science would cite this bundled type when moving from local recognizers to a unified geometric object. The module is a pure definition with no proofs or arguments inside it.

claimA recognition geometry is the bundled structure $\mathcal{RG}$ that contains a recognition chart, a comparative recognizer, a composition law satisfying the refinement theorem, a connectivity relation on resolution cells, core recognition maps, and a dimension assignment derived from recognizer structure.

background

Recognition Geometry treats space as emergent from the structure of recognition maps rather than assuming a pre-existing metric. The Core module supplies the foundational types. Charts module develops local coordinate systems that respect recognition structure. Comparative module shows how metric-like relations arise from qualitative "more than" comparisons. Composition module proves the Refinement Theorem for composite recognizers. Connectivity module defines paths that remain inside single resolution cells. Dimension module links recognizer structure to geometric dimension.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module completes the RecognitionGeometry type that assembles the components required for higher-level work in the Recognition Science framework. It directly supports the transition from local recognition data to global structures used in the forcing chain (T0-T8) and the derivation of constants such as the eight-tick octave and D=3. The definition is referenced by sibling modules complete_summary and next_steps.

scope and limits

depends on (15)

Lean names referenced from this declaration's body.

declarations in this module (3)