RSConfigSpace
plain-language theorem explainer
RSConfigSpace equips a ledger type L with the structure of a configuration space by mandating that L is nonempty and carries decidable equality. Modelers of the RS ledger cite this when they need the abstract ConfigSpace axioms to hold for concrete recognition states before building locality or measurement maps. The declaration proceeds by a type-class definition followed by a direct instance that forwards the nonempty requirement.
Claim. Let $L$ be a type. $L$ forms an RS configuration space when it is nonempty and equality on its elements is decidable. This supplies the structure of a configuration space: an empty configuration, a commutative join operation, a consistency predicate, and an independence relation satisfying the monoid laws.
background
A configuration space, as defined upstream, consists of an empty configuration emp, a binary join operation, a consistency predicate IsConsistent, and an independence relation Independent such that join forms a commutative monoid with emp as identity and independence is symmetric with emp independent of every configuration. The RSConfigSpace class adds the minimal requirements that the ledger type L is nonempty and that equality on L is decidable, allowing L to serve as the concrete carrier for these operations. The module sets the local theoretical setting by identifying RS ledger states with configuration space C, R̂ neighborhoods with local structure, and the 8-tick cycle with finite resolution, thereby linking the concrete physics of recognition events to the abstract axioms of Recognition Geometry.
proof idea
The declaration is a type-class definition whose fields are the nonempty and eq_decidable requirements. It immediately registers an instance of the upstream ConfigSpace class by delegating the nonempty field to the class member; the remaining ConfigSpace structure is inherited from the imported definition without additional proof steps.
why it matters
This is the base declaration that lets Recognition Science instantiate Recognition Geometry. It is invoked by RS_instantiates_RG, EightTickFiniteResolution, and physical_space_is_quotient to establish that the 8-tick cycle yields finite resolution (RG4) and that observable space arises as the recognition quotient. In the framework it corresponds to the ledger-to-configuration-space step that precedes the quotient construction for physical space and the emergence of J-cost metrics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.