chartOnQuotient_well_defined
The declaration shows that a recognition chart's coordinate function is constant on equivalence classes of the recognition quotient. Researchers modeling local geometry via recognition structures would invoke this to ensure coordinate assignments are unambiguous. The short tactic proof reduces quotient equality to indistinguishability via the quotient equivalence theorem and then applies the chart's respect property.
claimLet $L$ be a local configuration space, $r$ a recognizer, and $n$ a natural number. Let $U$ be the domain of a recognition chart $φ$ for $r$ with dimension $n$. For any point $q$ in the recognition quotient and configurations $c_1, c_2$ in $U$ whose images under the canonical projection both equal $q$, the coordinate values $φ(c_1)$ and $φ(c_2)$ are equal.
background
Recognition geometry studies local coordinate systems that respect indistinguishability under a recognizer. A RecognitionChart consists of a domain set in the configuration space, a proof that it is a neighborhood, a coordinate map to $ℝ^n$, and a guarantee that indistinguishable configurations receive identical coordinates. The recognition quotient is the space of equivalence classes under the indistinguishability relation, where two configurations are equivalent if they produce the same event under the recognizer. The theorem quotientMk_eq_iff states that two configurations map to the same quotient element if and only if they are indistinguishable.
proof idea
The proof first obtains an indistinguishability relation between $c_1$ and $c_2$ by rewriting the given quotient equalities using the quotientMk_eq_iff theorem in both directions. It then directly invokes the respects_indistinguishable field of the RecognitionChart structure on the paired domain elements to conclude that the coordinate values agree.
why it matters in Recognition Science
This theorem guarantees that recognition charts descend to well-defined functions on the quotient space, enabling the construction of atlases and the assignment of local dimensions in recognition geometry. It supports the physical view that spacetime coordinates label configurations while respecting observable equivalences. The result closes a key step toward atlas_covers_quotient and recognition_dimension_unique by ensuring coordinate consistency on equivalence classes.
scope and limits
- Does not establish existence of any recognition chart.
- Does not address compatibility between multiple charts.
- Does not constrain the possible dimensions n.
- Does not extend to global sections or non-local structures.
formal statement (Lean)
91theorem chartOnQuotient_well_defined (φ : RecognitionChart L r n)
92 (q : RecognitionQuotient r)
93 (c₁ c₂ : C) (h₁ : c₁ ∈ φ.domain) (h₂ : c₂ ∈ φ.domain)
94 (hq₁ : recognitionQuotientMk r c₁ = q) (hq₂ : recognitionQuotientMk r c₂ = q) :
95 φ.toFun ⟨c₁, h₁⟩ = φ.toFun ⟨c₂, h₂⟩ := by
proof body
Tactic-mode proof.
96 have h : Indistinguishable r c₁ c₂ := by
97 rw [← quotientMk_eq_iff r]
98 rw [hq₁, hq₂]
99 exact φ.respects_indistinguishable ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ h
100
101/-! ## Chart Compatibility -/
102
103/-- Two charts are compatible if they agree on their overlap -/