chartOnQuotient_well_defined
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.