ChartCompatible
plain-language theorem explainer
ChartCompatible is the predicate requiring two recognition charts to assign identical coordinates to every configuration in the intersection of their domains. It is cited by anyone constructing atlases or proving local coordinate properties in recognition geometry. The definition is a direct universal quantification over the overlap, with no additional lemmas required.
Claim. Two recognition charts $φ_1, φ_2$ (each a domain set in the local configuration space together with a coordinate map to $ℝ^n$ that respects indistinguishability) are compatible when, for every configuration $c$ belonging to both domains, the coordinate tuple produced by the first map equals the coordinate tuple produced by the second.
background
A RecognitionChart consists of a domain set declared to be a neighborhood in the local configuration space, a coordinate function from that domain into $ℝ^n$, and the requirement that indistinguishable configurations receive the same coordinates. The module develops the link between recognition geometry and classical manifold theory by treating such charts as local coordinate systems that respect observable equivalences. ChartCompatible is the direct translation of the standard manifold condition that overlapping charts must agree on their common domain.
proof idea
This is a definition rather than a derived theorem. It encodes agreement by quantifying over every configuration $c$ that lies in both domains and asserting equality of the two toFun applications at the corresponding subtype elements.
why it matters
ChartCompatible supplies the compatibility relation required by the RecognitionAtlas structure, which in turn appears in the charts_status summary asserting that spacetime is a smooth recognition geometry whose four dimensions count independent ways to distinguish events. It therefore occupies the same position in the recognition-geometry development as the chart-transition condition in differential geometry, directly supporting the module's claim that local coordinates arise from recognizer structure rather than being presupposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.