recognition_dimension_unique_hypothesis
plain-language theorem explainer
recognition_dimension_unique_hypothesis defines the proposition that any two recognition charts sharing a configuration point must assign it the same dimension. A researcher constructing a recognition manifold for spacetime would cite it to enforce local dimension invariance. The declaration is introduced directly as an axiom justified by Brouwer invariance of domain.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and let $U, V$ be neighborhoods in $L$. Suppose $n, m$ are natural numbers and let $c$ belong to the domains of two recognition charts $U$ to $R^n$ and $V$ to $R^m$ that respect indistinguishability. Then $n = m$.
background
A recognition chart is a local coordinate map from a neighborhood in the configuration space to $R^n$ that sends indistinguishable configurations to the same point and is defined on a valid neighborhood of some configuration, per the RecognitionChart structure. The module develops the link between recognition geometry and classical manifold theory, where charts label configurations while respecting observable equivalences. Dimension counts the independent ways to distinguish configurations locally, and the physical setting treats spacetime coordinates as recognition charts.
proof idea
This is a direct definition packaging the invariance implication as a named proposition. No lemmas or tactics are applied; the body simply states the two membership premises imply equality of the dimension parameters.
why it matters
The definition supplies the hypothesis used by the downstream theorem recognition_dimension_unique to conclude that overlapping charts share the same dimension. It encodes the axiom that dimension is well-defined on the recognition atlas, consistent with the framework derivation of three spatial dimensions from the eight-tick octave and the self-similar fixed point. It leaves open how recognition structures induce smooth manifolds globally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.