RecognitionChart
plain-language theorem explainer
RecognitionChart defines a local coordinate system on a neighborhood in configuration space that is constant on indistinguishable configurations and injective across resolution classes. Researchers deriving manifold-like structure from recognizers or extracting spacetime dimension as recognition dimension would cite this structure. The definition is given directly by its five fields encoding domain, neighborhood membership, coordinate function, and the two equivalence axioms.
Claim. A recognition chart for local configuration space $L$ and recognizer $r$ in dimension $n$ consists of a set $U$ that belongs to some neighborhood in $L$, together with a map $U$ to $R^n$ such that the map is constant on pairs indistinguishable by $r$ and equal values imply indistinguishability by $r$.
background
LocalConfigSpace supplies the collection of neighborhoods on configuration space $C$. Recognizer $r : C to E$ maps each configuration to an observable event; Indistinguishable $r$ $c_1$ $c_2$ holds precisely when $r$ $c_1$ equals $r$ $c_2$. RecognitionLatticeFromRecognizer.neighborhood defines finite-resolution neighborhoods as the set of all cells sharing a fixed observed label. The module develops recognition geometry as the bridge between recognizer structure and classical manifold theory, with charts serving as the local coordinate systems that descend to the quotient by indistinguishability.
proof idea
This declaration is a structure definition. Its fields directly encode the mathematical requirements: domain membership in $L.N$, the coordinate map to $Fin n to R$, and the two conditions on the map with respect to Indistinguishable.
why it matters
RecognitionChart is the basic building block for ChartCompatible, chartOnQuotient, and RecognitionAtlas. It is used to induce well-defined maps on the local quotient and to prove chart existence implies either finite domain or infinite image under $r$. In the Recognition Science framework it supports the emergence of $D=3$ spatial dimensions as the recognition dimension $n$ when an atlas of such charts covers the quotient space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.