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

MPForcesLedger

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)

  86class MPForcesLedger (X : Type*) where
  87  /-- Recognition structure exists. -/
  88  recognition : RecognitionStructure X
  89  /-- Charge assignment exists. -/
  90  charge : X → ℤ
  91  /-- Non-trivial transactions balance. -/
  92  balanced : ∀ (txn : List X), txn.length > 1 → (txn.map charge).sum = 0
  93
  94/-- The trivial model satisfies MPForcesLedger (with zero charge). -/
  95instance : MPForcesLedger Unit := {

proof body

Definition body.

  96  recognition := { recognizes := fun _ _ => True, has_self_recognition := ⟨(), trivial⟩ },
  97  charge := fun _ => 0,
  98  balanced := fun _ _ => by simp
  99}
 100
 101/-! ## Self-Similarity Principle -/
 102
 103/-- Self-similarity: a scaling transformation.
 104
 105The claim is that recognition structures are invariant under rescaling
 106by a specific factor.
 107-/

used by (1)

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

depends on (14)

Lean names referenced from this declaration's body.