pith. machine review for the scientific record. sign in
class definition def or abbrev

RSConfigSpace

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Definition body.

  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). -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.