chartCompatible_symm
plain-language theorem explainer
Symmetry of chart compatibility follows directly from the overlap agreement definition for recognition charts. Atlas constructors cite it to treat the compatibility relation as bidirectional when assembling local coordinate systems. The term proof introduces the configuration and domain hypotheses then applies symmetry to the coordinate equality.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and $n$ a natural number. If recognition charts $φ_1$ and $φ_2$ satisfy $φ_1.toFun(c) = φ_2.toFun(c)$ for every configuration $c$ in the intersection of their domains, then $φ_2.toFun(c) = φ_1.toFun(c)$ holds for the same $c$.
background
Recognition charts are local coordinate maps from a neighborhood in the configuration space to $ℝ^n$ that send indistinguishable configurations to identical points, as defined by the structure with domain, domain_is_nbhd, toFun, and respects_indistinguishable fields. ChartCompatible is the predicate requiring that the coordinate functions of two such charts agree exactly on the overlap of their domains. The module develops recognition geometry by connecting these charts to classical manifold ideas, where quotients by indistinguishability can admit smooth local coordinates when recognizers vary continuously.
proof idea
The term proof is a one-line wrapper. It introduces the configuration $c$ together with the two domain membership hypotheses, then applies symmetry to the equality supplied by the ChartCompatible assumption.
why it matters
This result confirms that chart compatibility is symmetric, a basic property needed before RecognitionAtlas can be defined as a family of mutually compatible charts covering the quotient space. It fills the symmetry step in the local coordinate construction described in the module, supporting the interpretation that spacetime dimension arises as a recognition dimension counting independent distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.