chartCompatible_refl
plain-language theorem explainer
Reflexivity of chart compatibility states that every recognition chart agrees with itself on its domain. Workers constructing recognition atlases cite this to confirm the compatibility relation forms an equivalence. The proof is a term-mode reduction that applies equality reflexivity after introducing a configuration point and its two domain-membership witnesses.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and $n$ a dimension. For any recognition chart $φ$ with domain a neighborhood in $L$, the compatibility predicate holds: for every configuration $c$ in the domain of $φ$, the coordinate map of $φ$ applied to $c$ equals itself.
background
A recognition chart is a local coordinate map from a neighborhood in the local configuration space to $ℝ^n$ that sends indistinguishable configurations to the same point. Chart compatibility requires two charts to assign identical coordinates to any configuration lying in the intersection of their domains. The module develops local coordinates that respect recognition structure after quotienting by indistinguishability, with charts existing when recognizers vary continuously with configuration.
proof idea
The proof is a term-mode wrapper. It introduces the configuration $c$ together with the two membership proofs that $c$ lies in the domain of each copy of $φ$, then reduces directly by reflexivity of equality on the coordinate values.
why it matters
This lemma supplies the reflexive leg of the compatibility relation needed to form recognition atlases as families of mutually compatible charts. It feeds the atlas-covering results and the recognition-dimension uniqueness statements in the same module, supporting the local-coordinate interpretation of spacetime dimension in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.