RSLocalityFromRHat
plain-language theorem explainer
RSLocalityFromRHat equips an RS ledger space L with an R̂ operator whose neighborhoods collect states reachable by one recognition event. Researchers bridging RS ledger states to Recognition Geometry locality axioms cite this structure when establishing RG1. The declaration is a structure definition that directly encodes self-inclusion, refinement, and transitivity as fields.
Claim. Let $L$ be a type with the RSConfigSpace structure. Then RSLocalityFromRHat $L$ consists of a map $R̂ : L → Set L$ such that $ℓ ∈ R̂(ℓ)$ for every $ℓ$, every neighborhood admits a refinement $U$ with $ℓ' ∈ U ⊆ R̂(ℓ')$, and $R̂(ℓ') ⊆ R̂(ℓ)$ whenever $ℓ' ∈ R̂(ℓ)$.
background
In the Recognition Geometry bridge module, RS ledger states form a configuration space via the RSConfigSpace class, which requires the space to be nonempty and to carry decidable equality. The R̂ operator abstracts recognition events so that the neighborhood of a ledger state ℓ consists of all states reachable by a single application. Upstream results such as the identity event from ObserverForcing and ledger factorization supply the concrete operations that this structure abstracts over.
proof idea
This declaration is a structure definition. It directly encodes the R̂ map together with the three required properties (self_in_RHat, refinement, transitivity) as fields. No lemmas or tactics are invoked; the structure itself supplies the interface used by toLocalConfigSpace and EightTickFiniteResolution.
why it matters
RSLocalityFromRHat supplies the locality structure (RG1) that feeds EightTickFiniteResolution and the master theorem RS_instantiates_RG, which shows the RS 8-tick cycle yields Recognition Geometry's finite-resolution axiom. It fills the RG1 slot in the module's bridge from RS ledger states and R̂ neighborhoods to the geometric framework. The open question it touches is the pending concrete construction of R̂ from full RS ledger primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.