`minJlogCost_monotoneStep_implies_postingStep`

proved

show as: view math explainer →

module: IndisputableMonolith.LedgerPostingAdjacency
domain: LedgerPostingAdjacency
line: 969 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 969.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 966
 967/-! ### Optional B4-style tightening: Jlog-cost minimality (among monotone, nontrivial steps) ⇒ posting -/
 968
 969theorem minJlogCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
 970    {L L' : LedgerState d}
 971    (hmono : MonotoneLedger (d := d) L L')
 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
 994theorem legalAtomicTick_oneBitDiff {d : Nat} {L L' : LedgerState d}
 995    (h : LegalAtomicTick (d := d) L L') :
 996    OneBitDiff (parity d L) (parity d L') :=
 997  postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep (d := d) h)
 998
 999/-! ## Workstream B tightening: RS AtomicTick ⇒ PostingStep (legality predicate) -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.