hasRecognitionDimension
Recognition dimension at a configuration point c is n precisely when c lies inside the domain of at least one recognition chart of dimension n. Workers establishing local manifold structure on quotiented recognition spaces cite this when they need a coordinate-independent notion of dimension. The definition is an immediate existential quantification over the RecognitionChart type already constructed in the module.
claimA configuration point $c$ has recognition dimension $n$ if there exists a recognition chart of dimension $n$ whose domain contains $c$.
background
Recognition geometry equips the quotient space of configurations with local charts that are homeomorphisms respecting indistinguishability. A recognition chart is a local homeomorphism from a subset of the configuration space to Euclidean space of dimension n that maps equivalent configurations to the same point. The module develops this after quotienting by the indistinguishability relation, so that charts exist precisely when recognizers vary continuously with configuration. Upstream, spatial dimension is introduced as a natural number in the dimension-forcing framework and is tied to the eight-tick period; ledger-factorization and phi-forcing structures supply the J-cost calibration that underlies the recognition relation itself.
proof idea
This is a direct definition that packages the existential statement over the RecognitionChart type; no lemmas are applied beyond the type declaration of RecognitionChart already available in the module.
why it matters in Recognition Science
The definition supplies the local-dimension predicate used by charts_status, which concludes that spacetime is a smooth recognition geometry whose four dimensions count independent ways recognizers distinguish events (three spatial, one temporal). It realizes the geometry-axiom clause that dimension is well-defined by invariance of domain and sits inside the forcing chain that derives D=3 from the eight-tick octave. No open scaffolding remains at this node.
scope and limits
- Does not construct any explicit chart.
- Does not prove existence of a chart for a given c.
- Does not constrain the global topology of the atlas.
- Does not encode the finite-resolution obstruction to charts.
formal statement (Lean)
147def hasRecognitionDimension (c : C) (n : ℕ) : Prop :=
proof body
Definition body.
148 ∃ φ : RecognitionChart L r n, c ∈ φ.domain
149
150/-- **GEOMETRY AXIOM**: Dimension is well-defined.
151
152 **Status**: Axiom (invariance of domain)
153 **Justification**: Brouwer's invariance of domain theorem
154 **Reference**: Standard topology; Mathlib.Topology.Basic -/