PostingStep

formal source

 140/-! ## Posting-step relation (ledger constraint ⇒ adjacency) -/
 141
 142/-- One atomic posting step between ledger states. -/
 143def PostingStep {d : Nat} (L L' : LedgerState d) : Prop :=
 144  ∃ k : Fin d, ∃ side : Side, L' = post L k side
 145
 146theorem postingStep_oneBitDiff {d : Nat} {L L' : LedgerState d} (h : PostingStep (d := d) L L') :
 147    OneBitDiff (parity d L) (parity d L') := by
 148  rcases h with ⟨k, side, rfl⟩
 149  simpa using parity_oneBitDiff_of_post (d := d) L k side
 150
 151/-! ## Optional deepening: a cost/legality predicate that implies `PostingStep` -/
 152
 153/-- L1 cost of a ledger transition, measured as total absolute change in debit+credit counts. -/
 154noncomputable def ledgerL1Cost {d : Nat} (L L' : LedgerState d) : Nat :=
 155  (∑ i : Fin d, Int.natAbs (L'.debit i - L.debit i)) +
 156  (∑ i : Fin d, Int.natAbs (L'.credit i - L.credit i))
 157
 158/-- Monotone-posting constraint: debit/credit counts never decrease. -/
 159def MonotoneLedger {d : Nat} (L L' : LedgerState d) : Prop :=
 160  (∀ i : Fin d, L.debit i ≤ L'.debit i) ∧ (∀ i : Fin d, L.credit i ≤ L'.credit i)
 161
 162/-- A small “legality” predicate: monotone ledger counts + unit L1 step. -/
 163def LegalAtomicTick {d : Nat} (L L' : LedgerState d) : Prop :=
 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 ℝ). -/
 169noncomputable def ledgerJlogCost {d : Nat} (L L' : LedgerState d) : ℝ :=
 170  (∑ i : Fin d, Cost.Jlog ((L'.debit i - L.debit i : ℤ) : ℝ)) +
 171  (∑ i : Fin d, Cost.Jlog ((L'.credit i - L.credit i : ℤ) : ℝ))
 172
 173theorem ledgerJlogCost_nonneg {d : Nat} (L L' : LedgerState d) : 0 ≤ ledgerJlogCost (d := d) L L' := by