RSConfigSpace

formal source

  55
  56    This is infinite-dimensional (one dimension per possible entity)
  57    but locally finite (only finitely many entities interact locally). -/
  58class RSConfigSpace (L : Type*) where
  59  /-- The ledger space is nonempty (there's at least one possible state) -/
  60  nonempty : Nonempty L
  61  /-- Two ledger states can be compared -/
  62  eq_decidable : DecidableEq L
  63
  64/-- RS ledger states satisfy RG0 -/
  65instance (L : Type*) [RSConfigSpace L] : ConfigSpace L where
  66  nonempty := RSConfigSpace.nonempty
  67
  68/-! ## RS Locality from R̂ Operator -/
  69
  70/-- **Structural Definition**: The R̂ operator defines locality on the ledger.
  71
  72    Two ledger states are "close" if they differ only in a localized region—
  73    i.e., if an R̂ operation could transform one into the other.
  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.