RSLocalityFromRHat

formal source

  74
  75    The neighborhood N(ℓ) of a ledger state ℓ consists of all states reachable
  76    by a single R̂ application (recognition event). -/
  77structure RSLocalityFromRHat (L : Type*) [RSConfigSpace L] where
  78  /-- The R̂ operator: recognition events -/
  79  RHat : L → Set L
  80  /-- Self is always reachable (identity recognition) -/
  81  self_in_RHat : ∀ ℓ, ℓ ∈ RHat ℓ
  82  /-- R̂ neighborhoods have a refinement property -/
  83  refinement : ∀ ℓ ℓ', ℓ' ∈ RHat ℓ → ∃ U ⊆ RHat ℓ, ℓ' ∈ U ∧ U ⊆ RHat ℓ'
  84  /-- Recognition transitivity: when ℓ' is reachable from ℓ, then anything reachable
  85      from ℓ' is also reachable from ℓ. This is the RS analog of neighborhood containment. -/
  86  transitivity : ∀ ℓ ℓ' : L, ℓ' ∈ RHat ℓ → RHat ℓ' ⊆ RHat ℓ
  87
  88/-- Convert RS locality to RecogGeom locality.
  89
  90    Note: Full implementation requires showing R̂ neighborhoods satisfy
  91    the refinement property. This structural version shows the pattern. -/
  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
  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)