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

ledgerProperties

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)

 118def ledgerProperties : List String := [

proof body

Definition body.

 119  "Discrete microstates from ledger entries",
 120  "J-cost plays role of energy",
 121  "Degeneracy from ledger symmetries",
 122  "Conservation laws from ledger balance"
 123]
 124
 125/-! ## The J-Cost Connection -/
 126
 127/-- The fundamental connection:
 128
 129    E_state ↔ J_cost(ledger_entry)
 130
 131    A low J-cost state is "low energy" and favored.
 132    A high J-cost state is "high energy" and suppressed. -/

depends on (18)

Lean names referenced from this declaration's body.