minCost_monotoneStep_implies_postingStep

formal source

 927
 928/-! ### Optional B3-style tightening: minimal cost (among monotone, nontrivial steps) ⇒ posting -/
 929
 930theorem minCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
 931    {L L' : LedgerState d}
 932    (hmono : MonotoneLedger (d := d) L L')
 933    (hneq : L ≠ L')
 934    (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
 935      ledgerL1Cost (d := d) L L' ≤ ledgerL1Cost (d := d) L L'') :
 936    PostingStep (d := d) L L' := by
 937  classical
 938  -- compare against a concrete single-post candidate (cost = 1)
 939  let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
 940  have hpostNe : L ≠ post L k0 Side.debit := by
 941    intro hEq
 942    have hdeb : L.debit k0 = L.debit k0 + 1 := by
 943      -- RHS is `L.debit k0 + 1`
 944      have := congrArg (fun s => s.debit k0) hEq
 945      simpa [post] using this
 946    linarith
 947  have hle1 : ledgerL1Cost (d := d) L L' ≤ 1 := by
 948    have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
 949      post_monotone (d := d) L k0 Side.debit
 950    have hcost' : ledgerL1Cost (d := d) L (post L k0 Side.debit) = 1 :=
 951      ledgerL1Cost_post (d := d) L k0 Side.debit
 952    have := hmin (post L k0 Side.debit) hmono' hpostNe
 953    simpa [hcost'] using this
 954  have hcostNe0 : ledgerL1Cost (d := d) L L' ≠ 0 := by
 955    intro h0
 956    have : L' = L := (ledgerL1Cost_eq_zero_iff (d := d) L L').1 h0
 957    exact hneq (by simpa [this])
 958  have hcost1 : ledgerL1Cost (d := d) L L' = 1 := by
 959    have hcases := Nat.le_one_iff_eq_zero_or_eq_one.1 hle1
 960    cases hcases with