theorem
proved
tactic proof
minJlogCost_monotoneStep_implies_postingStep
show as:
view Lean formalization →
formal statement (Lean)
969theorem minJlogCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
970 {L L' : LedgerState d}
971 (hmono : MonotoneLedger (d := d) L L')
proof body
Tactic-mode proof.
972 (hneq : L ≠ L')
973 (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
974 ledgerJlogCost (d := d) L L' ≤ ledgerJlogCost (d := d) L L'') :
975 PostingStep (d := d) L L' := by
976 classical
977 -- compare against a concrete single-post candidate (Jlog-cost = Jlog 1)
978 let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
979 have hpostNe : L ≠ post L k0 Side.debit := by
980 intro hEq
981 have hdeb : L.debit k0 = L.debit k0 + 1 := by
982 have := congrArg (fun s => s.debit k0) hEq
983 simpa [post] using this
984 linarith
985 have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
986 post_monotone (d := d) L k0 Side.debit
987 have hcost' : ledgerJlogCost (d := d) L (post L k0 Side.debit) = Cost.Jlog (1 : ℝ) :=
988 ledgerJlogCost_post (d := d) L k0 Side.debit
989 have hleJ1 : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ) := by
990 have := hmin (post L k0 Side.debit) hmono' hpostNe
991 simpa [hcost'] using this
992 exact postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 (d := d) (L := L) (L' := L') hmono hneq hleJ1
993