toRecognizer
plain-language theorem explainer
The definition converts an RSMeasurement structure into a Recognizer by extracting its measure function as the recognition map R while copying the nontriviality witness. Researchers bridging ledger-based physics to geometric recognition axioms cite it when instantiating RG2 from concrete RS data. The construction is a direct record projection with no additional lemmas.
Claim. Let $L$ be a type carrying the RSConfigSpace structure and let $m$ be an RSMeasurement from $L$ to $E$. The induced recognizer is the record whose recognition function satisfies $R(ℓ) = m.measure(ℓ)$ for every ledger state $ℓ$, together with the witness that $m$ distinguishes at least two states.
background
RSConfigSpace equips a ledger type $L$ with nonemptiness and decidable equality so that states can be compared. RSMeasurement packages a map measure : $L → E$ with a nontriviality witness asserting that at least two ledger states produce distinct outcomes. The module supplies the structural bridge that turns RS ledger states into configuration spaces, R̂ neighborhoods into local structure, and measurements into recognizers.
proof idea
The definition is a one-line wrapper that constructs the Recognizer record by setting its R field to m.measure and its nontrivial field to m.nontrivial.
why it matters
This supplies the RSRecognizer component required by RS_instantiates_RG, which shows that the 8-tick hypothesis yields Recognition Geometry's finite-resolution axiom RG4. It is also invoked inside physical_space_is_quotient to identify the observable space with the image of the measurement map. The construction realizes the module's claim that RS measurements instantiate recognizers within the Recognition Geometry framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.