recognition_dimension_unique
plain-language theorem explainer
Recognition charts on a fixed local configuration space and recognizer have a unique dimension. A physicist constructing local coordinates for observable configurations would cite this to ensure dimension is chart-independent. The proof is a one-line application of the uniqueness hypothesis to the two domain-membership facts.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and let $n,m$ be natural numbers. If recognition charts $φ$ and $ψ$ of dimensions $n$ and $m$ both contain a configuration $c$ in their domains and the uniqueness hypothesis holds for $φ$, $ψ$, and $c$, then $n=m$.
background
The module develops recognition geometry as a bridge to classical manifold theory. A recognition chart is a local coordinate map $φ: U → ℝ^n$ on a neighborhood $U$ of the local configuration space such that indistinguishable configurations are sent to the same point and the map respects the recognizer structure. The RecognitionChart structure records the domain, a neighborhood witness, the coordinate function to Fin n → ℝ, and the indistinguishability-respecting property. The local theoretical setting is that charts exist precisely when recognizers vary continuously with configuration, allowing the quotient space to carry a smooth structure even though raw neighborhoods may be finite-resolution.
proof idea
This is a one-line wrapper that applies the hypothesis recognition_dimension_unique_hypothesis directly to the two domain-membership facts hφ and hψ.
why it matters
The result guarantees that local dimension extracted from recognition structure is unambiguous, supporting the construction of a RecognitionAtlas whose charts are dimensionally compatible. It fills the step that makes the recognition dimension well-defined before atlas_covers_quotient can be stated. In the broader framework it aligns with the forcing chain that produces D=3 spatial dimensions from the eight-tick octave, ensuring the local coordinate count is forced rather than arbitrary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.