chart_respects_equiv
plain-language theorem explainer
A recognition chart assigns identical coordinates to any pair of indistinguishable configurations. Researchers constructing local models of spacetime as recognition structures cite this to confirm charts factor through the equivalence relation. The proof is a direct one-line application of the chart's built-in respect field.
Claim. Let $U$ be the domain of a recognition chart for recognizer $r$ with target dimension $n$. If configurations $c_1, c_2$ lie in $U$ and satisfy $r(c_1) = r(c_2)$, then the coordinate values agree: the image of $c_1$ equals the image of $c_2$.
background
Recognition geometry equips configuration spaces with local charts that respect the indistinguishability relation induced by a recognizer. A recognition chart consists of a neighborhood domain together with a coordinate map to real $n$-space that is constant on indistinguishable pairs and satisfies a continuity condition with respect to the local structure. The indistinguishability relation identifies configurations that produce identical events under the recognizer. This module develops the analogy to manifold charts, where the quotient by indistinguishability may admit smooth structure even if the raw configuration space does not. The RecognitionChart structure encodes the respect property directly, while the Indistinguishable predicate formalizes the equivalence $c_1$ equivalent to $c_2$ under $r$ precisely when the recognizer outputs match.
proof idea
The proof is a one-line term that applies the respects_indistinguishable field of the RecognitionChart structure to the supplied configurations and hypothesis.
why it matters
This result ensures charts descend to well-defined functions on the local quotient space. It supports the construction of RecognitionAtlas and the claim that spacetime dimensions arise as recognition dimensions counting independent distinction modes. The parent summaries in charts_status and complete_summary record it as a verified property. It fills the step showing local coordinates respect observable equivalences, consistent with the framework view that dimension counts independent ways recognizers distinguish events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.