chartOnQuotient
plain-language theorem explainer
chartOnQuotient equips any RecognitionChart with a coordinate function on the local quotient space by selecting a representative configuration and applying the chart map. Researchers constructing atlases for recognition geometries cite this when moving from local charts to well-defined maps on equivalence classes. The definition proceeds by choice of representative followed by direct application of the chart's toFun.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and $n$ a dimension. For a recognition chart $φ$ with domain $U$, the induced map sends each quotient class $q$ (admitting a representative $c ∈ U$) to the coordinates $φ(c) ∈ ℝ^n$.
background
A RecognitionChart consists of a domain set in the local config space, a proof that the domain is a neighborhood of some point, a coordinate map toFun : domain → Fin n → ℝ, and the respects_indistinguishable axiom ensuring that indistinguishable configurations receive identical coordinates. The module develops these charts as local coordinate systems that respect recognition structure, bridging to classical manifold theory by quotienting out indistinguishability so that the resulting space may admit smooth coordinates. The construction relies on the RecognitionQuotient type from the imported Quotient module, which encodes equivalence classes under the recognizer.
proof idea
The definition is a one-line wrapper that applies the chart's toFun after using choice to select a representative c from the quotient class and confirming membership in the domain.
why it matters
This definition supplies the quotient-level coordinate maps required by charts_status, which records that charts induce maps on the quotient as part of establishing spacetime as a smooth recognition geometry. It advances the module's program of showing that local recognition dimensions (including the 3 spatial dimensions forced by the eight-tick octave) arise from compatible charts on the quotient. The step touches the open question of chart existence under finite-resolution constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.