module module high

`IndisputableMonolith.RecogGeom.Charts`

Recognition charts supply local coordinate maps on configuration space that collapse indistinguishable states under a given recognizer. The module defines the chart structure, compatibility relations, and atlas using the quotient and finite-resolution constructions from its imports. It supplies the coordinate layer for the Recognition Geometry framework and is referenced by the complete integration summary. This is a definitions module with no proofs.

claimGiven recognizer $R: C→E$ and neighborhood $U$, a recognition chart is a map $φ:U→ℝ^n$ that is injective on resolution cells and continuous under small configuration changes.

background

Recognition Geometry builds local coordinate systems on the quotient space of configurations. The upstream FiniteResolution module states axiom RG4: every bounded neighborhood admits only finitely many distinguishable configurations, providing the bridge to discrete scales. The Quotient module defines the recognition quotient $C_R=C/∼$ that collapses states indistinguishable by the recognizer.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Integration module that assembles the full Recognition Geometry framework. It supplies the local coordinate step required for atlas constructions and dimension uniqueness statements used in the complete summary.

scope and limits

Does not prove existence of charts for every recognizer and neighborhood.
Does not derive physical laws or constants from the chart maps.
Does not establish the recognition dimension equals three.
Does not address global manifold structure or dynamics.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RecogGeom.Integration module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.FiniteResolution module_import
IndisputableMonolith.RecogGeom.Quotient module_import

declarations in this module (17)

structure RecognitionChart L57
theorem chart_respects_equiv L76
def chartOnQuotient L82
theorem chartOnQuotient_well_defined L91
def ChartCompatible L104
theorem chartCompatible_refl L109
theorem chartCompatible_symm L116
structure RecognitionAtlas L125
theorem atlas_covers_quotient L134
def hasRecognitionDimension L147
def recognition_dimension_unique_hypothesis L155
theorem recognition_dimension_unique L159
def finite_resolution_no_chart_hypothesis L178
theorem finite_resolution_no_chart L184
theorem chart_exists_implies L193
def IsSmoothRecognitionGeometry L212
def charts_status L239