MonotoneLedger

formal source

 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
 174  classical
 175  have h₁ : 0 ≤ ∑ i : Fin d, Cost.Jlog ((L'.debit i - L.debit i : ℤ) : ℝ) :=
 176    Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
 177  have h₂ : 0 ≤ ∑ i : Fin d, Cost.Jlog ((L'.credit i - L.credit i : ℤ) : ℝ) :=
 178    Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
 179  -- unfold once; avoid `simp` expanding `Jlog` into exponentials.
 180  dsimp [ledgerJlogCost]
 181  exact add_nonneg h₁ h₂
 182
 183private lemma ledgerJlogCost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
 184    ledgerJlogCost (d := d) L (post L k side) = Cost.Jlog (1 : ℝ) := by
 185  classical
 186  cases side with
 187  | debit =>
 188      -- debit has one +1 delta at k; credit deltas are 0
 189      have hdeb :