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

LegalAtomicTick

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)

 163def LegalAtomicTick {d : Nat} (L L' : LedgerState d) : Prop :=

proof body

Definition body.

 164  MonotoneLedger (d := d) L L' ∧ ledgerL1Cost (d := d) L L' = 1
 165
 166/-! ## Optional deepening: Jlog-cost version (closer to RS cost than L1) -/
 167
 168/-- A Jlog-based step cost over integer ledger deltas (cast to ℝ). -/

used by (7)

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

depends on (18)

Lean names referenced from this declaration's body.