RSMeasurement
plain-language theorem explainer
RSMeasurement packages a map from ledger states L to events E together with a witness that the map separates at least two states. Bridge builders between Recognition Science and Recognition Geometry cite the structure when they need an explicit recognizer instance. The declaration is a pure structural definition that directly assembles the function and the existential condition.
Claim. Let $L$ be a ledger space equipped with the RS configuration space structure and let $E$ be an event type. An RS measurement consists of a function $m:L→E$ such that there exist distinct states $ℓ_1,ℓ_2∈L$ with $m(ℓ_1)≠m(ℓ_2)$.
background
RSConfigSpace asserts that the ledger type L is nonempty and carries decidable equality. In the Recognition Science setting this models the complete instantaneous state of the universe ledger: every registered entity, its current recognition relations, and the full configuration space, which is infinite-dimensional with one coordinate per possible entity.
proof idea
The declaration is a structure definition. It simply records the measure field and the nontrivial existential witness; no lemmas or tactics are applied.
why it matters
RSMeasurement supplies the recognizer component required by EightTickFiniteResolution, physical_space_is_quotient, and RS_instantiates_RG. It realizes the module's RG2 slot (measurement maps are recognizers) and feeds the 8-tick finite-resolution argument that yields HasFiniteResolution for the induced local configuration space. The construction therefore closes one link in the chain from ledger states through the eight-tick octave to the recognition quotient that models physical space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.