chartCompatible_symm
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any recognition chart on a given neighborhood.
- Does not establish transitivity of the compatibility relation.
- Does not constrain the dimension parameter $n$ or link it to the phi-ladder.
- Does not address finite-resolution obstructions or quotient smoothness.
formal statement (Lean)
116theorem chartCompatible_symm (φ₁ φ₂ : RecognitionChart L r n)
117 (hcompat : ChartCompatible L r φ₁ φ₂) :
118 ChartCompatible L r φ₂ φ₁ := by
proof body
Term-mode proof.
119 intro c h₂ h₁
120 exact (hcompat c h₁ h₂).symm
121
122/-! ## Recognition Atlas -/
123
124/-- A recognition atlas is a family of compatible charts that cover the space -/