theorem
proved
tactic proof
minCost_monotoneStep_implies_postingStep
show as:
view Lean formalization →
formal statement (Lean)
930theorem minCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
931 {L L' : LedgerState d}
932 (hmono : MonotoneLedger (d := d) L L')
proof body
Tactic-mode proof.
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
961 | inl h0 => exact (hcostNe0 h0).elim
962 | inr h1 => exact h1
963 -- conclude via the `PostingStep ↔ LegalAtomicTick` equivalence
964 have hlegal : LegalAtomicTick (d := d) L L' := ⟨hmono, hcost1⟩
965 exact (postingStep_iff_legalAtomicTick (d := d)).2 hlegal
966
967/-! ### Optional B4-style tightening: Jlog-cost minimality (among monotone, nontrivial steps) ⇒ posting -/
968