theorem
proved
postingStep_oneBitDiff
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 146.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
cost -
cost -
of -
as -
of -
LedgerState -
LedgerState -
of -
LedgerState -
LedgerState -
parity -
parity_oneBitDiff_of_post -
PostingStep -
total -
that -
total -
OneBitDiff -
LedgerState -
L -
L
used by
formal source
143def PostingStep {d : Nat} (L L' : LedgerState d) : Prop :=
144 ∃ k : Fin d, ∃ side : Side, L' = post L k side
145
146theorem postingStep_oneBitDiff {d : Nat} {L L' : LedgerState d} (h : PostingStep (d := d) L L') :
147 OneBitDiff (parity d L) (parity d L') := by
148 rcases h with ⟨k, side, rfl⟩
149 simpa using parity_oneBitDiff_of_post (d := d) L k side
150
151/-! ## Optional deepening: a cost/legality predicate that implies `PostingStep` -/
152
153/-- L1 cost of a ledger transition, measured as total absolute change in debit+credit counts. -/
154noncomputable def ledgerL1Cost {d : Nat} (L L' : LedgerState d) : Nat :=
155 (∑ i : Fin d, Int.natAbs (L'.debit i - L.debit i)) +
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 _)