physical_space_is_quotient
plain-language theorem explainer
This definition shows that for any RS measurement the recognition quotient of the induced recognizer is canonically isomorphic to the image of the measurement map. Researchers linking Recognition Science ledger states to geometric observables would cite it when identifying physical space with measurement ranges. The proof is a one-line wrapper that specializes the generic quotient_equiv_image theorem after applying toRecognizer.
Claim. For a measurement $m:L→E$ on an RS configuration space $L$, the recognition quotient of the recognizer induced by $m$ is isomorphic to the range of $m$.
background
The RSBridge module supplies the structural link between Recognition Science and Recognition Geometry. RSConfigSpace equips ledger states with nonemptiness and decidable equality so they form a configuration space. RSMeasurement packages a function measure : L → E together with a nontriviality witness that at least two states are distinguished. The module states that physical space arises as the recognition quotient under these measurements, with the eight-tick cycle supplying finite resolution.
proof idea
The definition is a one-line wrapper. It invokes quotient_equiv_image on the recognizer obtained by toRecognizer m and uses simpa to rewrite the toRecognizer definition away.
why it matters
The construction supplies the precise Lean counterpart of the paper claim that observable space is congruent to the image of the recognizer. It is referenced by rsbridge_status to confirm that RS satisfies the Recognition Geometry axioms, including the identification of physical space with the recognition quotient. The result sits at the T8 step where three spatial dimensions are forced from the quotient structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.