92noncomputable def toLocalConfigSpace {L : Type*} [RSConfigSpace L] 93 (rs : RSLocalityFromRHat L) : LocalConfigSpace L where 94 N := fun ℓ => {U | ∃ k : ℕ, k > 0 ∧ U = rs.RHat ℓ} -- Single step for now
proof body
Definition body.
95 -- For a full implementation, would use k-step R̂ neighborhoods 96 mem_of_mem_N := fun ℓ U ⟨k, hk, hU⟩ => hU ▸ rs.self_in_RHat ℓ 97 N_nonempty := fun ℓ => ⟨rs.RHat ℓ, 1, Nat.one_pos, rfl⟩ 98 intersection_closed := fun ℓ U V ⟨k₁, hk1, hU⟩ ⟨k₂, hk2, hV⟩ => by 99 -- Both U and V are rs.RHat ℓ, so their intersection is rs.RHat ℓ 100 subst hU hV 101 refine ⟨rs.RHat ℓ, ⟨1, Nat.one_pos, rfl⟩, ?_⟩ 102 rw [Set.inter_self] 103 refinement := fun ℓ U ℓ' ⟨k, hk, hU⟩ hℓ' => by 104 subst hU 105 -- We need: ∃ W ∈ N(ℓ'), W ⊆ RHat ℓ 106 -- N(ℓ') = {W | ∃ k, k > 0 ∧ W = RHat ℓ'}, so W = RHat ℓ' 107 -- Need: RHat ℓ' ⊆ RHat ℓ (recognition transitivity) 108 refine ⟨rs.RHat ℓ', ⟨1, Nat.one_pos, rfl⟩, ?_⟩ 109 exact rs.transitivity ℓ ℓ' hℓ' 110 111/-! ## RS Recognizers from Measurement -/ 112 113/-- **Structural Definition**: Measurement maps in RS are recognizers. 114 115 A measurement in RS: 116 - Takes a ledger state ℓ 117 - Returns an observable event e 118 - Two states with the same measurement outcome are indistinguishable 119 120 The 8-tick cadence ensures measurements have finite local resolution. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.