IndisputableMonolith.LedgerPostingAdjacency
IndisputableMonolith/LedgerPostingAdjacency.lean · 1076 lines · 45 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Recognition
3import IndisputableMonolith.Cost
4import IndisputableMonolith.LedgerParityAdjacency
5
6/-!
7# Posting-style ledger updates ⇒ parity one-bit adjacency
8
9This file upgrades Workstream B from a “vector lemma” to an explicit **ledger-shaped**
10model: a ledger state consists of `(debit, credit)` and a tick posts exactly one unit
11to exactly one account (either as debit or credit).
12
13Key theorem (THEOREM level):
14- A single post changes `phi = debit-credit` by ±1 at exactly one coordinate, hence the
15 induced parity pattern changes in exactly one bit.
16
17Claim hygiene:
18- This is still a mathematical model. It is the missing glue between “ledger” language
19 and the parity/Gray adjacency lemma in `LedgerParityAdjacency.lean`.
20- Deriving why *nature* must use this posting model is a separate MECH/AXIOM/bridge step.
21-/
22
23namespace IndisputableMonolith
24namespace LedgerPostingAdjacency
25
26open IndisputableMonolith.Recognition
27open IndisputableMonolith.Patterns
28open IndisputableMonolith.LedgerParityAdjacency
29open IndisputableMonolith.Cost
30open scoped BigOperators
31
32/-! ## A minimal recognition carrier: accounts = `Fin d` -/
33
34/-- Minimal carrier for a d-account ledger. The recognition relation is irrelevant here. -/
35def AccountRS (d : Nat) : RecognitionStructure :=
36 { U := Fin d, R := fun _ _ => True }
37
38/-!
39### AtomicTick availability (Workstream B tightening)
40
41For the concrete carrier `Fin d` (with `d ≠ 0`), we can construct an `AtomicTick` instance
42directly: at tick `t`, the posted account is the canonical `Fin d` coercion of `t`.
43
44Claim hygiene: this is a *model existence* theorem (THEOREM-level within Lean), not an empirical
45claim about nature’s tick scheduling.
46-/
47
48noncomputable instance accountRS_atomicTick (d : Nat) [NeZero d] : Recognition.AtomicTick (AccountRS d) :=
49{ postedAt := fun t u =>
50 u = ⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩
51 unique_post := by
52 intro t
53 refine ⟨⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩, rfl, ?_⟩
54 intro u hu
55 simpa [hu]
56}
57
58abbrev LedgerState (d : Nat) : Type := Recognition.Ledger (AccountRS d)
59
60abbrev phiVec {d : Nat} (L : LedgerState d) : Fin d → ℤ :=
61 Recognition.phi L
62
63abbrev parity (d : Nat) (L : LedgerState d) : Pattern d :=
64 parityPattern (phiVec (d := d) L)
65
66/-! ## Posting model -/
67
68inductive Side where
69 | debit
70 | credit
71deriving DecidableEq, Repr
72
73/-- Apply a single unit post (either debit or credit) at account `k`. -/
74noncomputable def post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) : LedgerState d := by
75 classical
76 exact match side with
77 | Side.debit =>
78 { debit := fun i => if i = k then L.debit i + 1 else L.debit i
79 , credit := L.credit }
80 | Side.credit =>
81 { debit := L.debit
82 , credit := fun i => if i = k then L.credit i + 1 else L.credit i }
83
84@[simp] lemma phiVec_post_debit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
85 phiVec (d := d) (post L k Side.debit) i =
86 (if i = k then phiVec (d := d) L i + 1 else phiVec (d := d) L i) := by
87 by_cases hik : i = k
88 · subst hik
89 simp [post, phiVec, Recognition.phi]
90 ring_nf
91 · simp [post, phiVec, Recognition.phi, hik]
92
93@[simp] lemma phiVec_post_credit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) :
94 phiVec (d := d) (post L k Side.credit) i =
95 (if i = k then phiVec (d := d) L i - 1 else phiVec (d := d) L i) := by
96 by_cases hik : i = k
97 · subst hik
98 simp [post, phiVec, Recognition.phi]
99 ring_nf
100 · simp [post, phiVec, Recognition.phi, hik]
101
102/-! ## Bridge: a post induces a coord-atomic step on `phi` -/
103
104lemma phiVec_coordAtomicStep_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
105 coordAtomicStep (d := d) (phiVec (d := d) L) (phiVec (d := d) (post L k side)) := by
106 classical
107 refine ⟨k, ?_, ?_⟩
108 · cases side with
109 | debit =>
110 left
111 -- at k, phi increases by 1
112 simpa using (by
113 have := (phiVec_post_debit (d := d) L k k)
114 simpa using this)
115 | credit =>
116 right
117 -- at k, phi decreases by 1
118 simpa using (by
119 have := (phiVec_post_credit (d := d) L k k)
120 simpa using this)
121 · intro i hik
122 cases side with
123 | debit =>
124 -- other coordinates unchanged
125 have := (phiVec_post_debit (d := d) L k i)
126 simpa [hik] using this
127 | credit =>
128 have := (phiVec_post_credit (d := d) L k i)
129 simpa [hik] using this
130
131/-! ## Main theorem: posting ⇒ parity adjacency -/
132
133theorem parity_oneBitDiff_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
134 OneBitDiff (parity d L) (parity d (post L k side)) := by
135 -- reduce to the coord-atomic step lemma and reuse `coordAtomicStep_oneBitDiff`
136 have hstep := phiVec_coordAtomicStep_of_post (d := d) L k side
137 simpa [parity] using (coordAtomicStep_oneBitDiff (d := d) (x := phiVec (d := d) L)
138 (y := phiVec (d := d) (post L k side)) hstep)
139
140/-! ## Posting-step relation (ledger constraint ⇒ adjacency) -/
141
142/-- One atomic posting step between ledger states. -/
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 _)
177 have h₂ : 0 ≤ ∑ i : Fin d, Cost.Jlog ((L'.credit i - L.credit i : ℤ) : ℝ) :=
178 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
179 -- unfold once; avoid `simp` expanding `Jlog` into exponentials.
180 dsimp [ledgerJlogCost]
181 exact add_nonneg h₁ h₂
182
183private lemma ledgerJlogCost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
184 ledgerJlogCost (d := d) L (post L k side) = Cost.Jlog (1 : ℝ) := by
185 classical
186 cases side with
187 | debit =>
188 -- debit has one +1 delta at k; credit deltas are 0
189 have hdeb :
190 (∑ i : Fin d, Cost.Jlog (((post L k Side.debit).debit i - L.debit i : ℤ) : ℝ))
191 = Cost.Jlog (1 : ℝ) := by
192 let f : Fin d → ℝ := fun i => Cost.Jlog (((post L k Side.debit).debit i - L.debit i : ℤ) : ℝ)
193 have hsplit :=
194 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
195 have fk : f k = Cost.Jlog (1 : ℝ) := by
196 simp [f, post]
197 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
198 refine Finset.sum_eq_zero ?_
199 intro i hi
200 have hik : i ≠ k := by simpa [Finset.mem_erase] using hi
201 simp [f, post, hik]
202 -- `sum univ = f k + sum (erase k)`
203 calc
204 (∑ i : Fin d, f i) =
205 f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
206 simpa using hsplit.symm
207 _ = Cost.Jlog (1 : ℝ) := by simp [fk, hErase]
208 have hcred :
209 (∑ i : Fin d, Cost.Jlog (((post L k Side.debit).credit i - L.credit i : ℤ) : ℝ)) = 0 := by
210 refine Finset.sum_eq_zero ?_
211 intro i _
212 simp [post]
213 -- avoid `simp` unfolding `Jlog` into exp-sums (it introduces `-↑d` terms).
214 simp only [ledgerJlogCost, hdeb, hcred, add_zero, zero_add]
215 | credit =>
216 have hdeb :
217 (∑ i : Fin d, Cost.Jlog (((post L k Side.credit).debit i - L.debit i : ℤ) : ℝ)) = 0 := by
218 refine Finset.sum_eq_zero ?_
219 intro i _
220 simp [post]
221 have hcred :
222 (∑ i : Fin d, Cost.Jlog (((post L k Side.credit).credit i - L.credit i : ℤ) : ℝ))
223 = Cost.Jlog (1 : ℝ) := by
224 let f : Fin d → ℝ := fun i => Cost.Jlog (((post L k Side.credit).credit i - L.credit i : ℤ) : ℝ)
225 have hsplit :=
226 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
227 have fk : f k = Cost.Jlog (1 : ℝ) := by
228 simp [f, post]
229 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
230 refine Finset.sum_eq_zero ?_
231 intro i hi
232 have hik : i ≠ k := by simpa [Finset.mem_erase] using hi
233 simp [f, post, hik]
234 calc
235 (∑ i : Fin d, f i) =
236 f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
237 simpa using hsplit.symm
238 _ = Cost.Jlog (1 : ℝ) := by simp [fk, hErase]
239 simp only [ledgerJlogCost, hdeb, hcred, add_zero, zero_add]
240
241/-- Every one-account posting has exactly the unit `Jlog` transition cost. -/
242theorem ledgerJlogCost_eq_Jlog1_of_postingStep
243 {d : Nat} {L L' : LedgerState d}
244 (h : PostingStep (d := d) L L') :
245 ledgerJlogCost (d := d) L L' = Cost.Jlog (1 : ℝ) := by
246 rcases h with ⟨k, side, rfl⟩
247 exact ledgerJlogCost_post L k side
248
249/-! ### Jlog-cost tightening: if a monotone nontrivial tick has Jlog-cost ≤ Jlog(1), it is a posting step. -/
250
251private lemma intCast_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) : ((z : ℤ) : ℝ) ≠ 0 := by
252 exact_mod_cast hz
253
254private lemma jlog_lt_jlog_of_one_lt {x : ℝ} (hx : 1 < x) :
255 Cost.Jlog (1 : ℝ) < Cost.Jlog x := by
256 unfold Cost.Jlog
257 apply Cost.Jcost_strict_mono_on_one_infty
258 · exact Real.exp_pos 1
259 · exact Real.exp_pos x
260 · exact Real.one_le_exp (by norm_num)
261 · exact Real.exp_lt_exp.mpr hx
262
263theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 {d : Nat} {L L' : LedgerState d}
264 (hmono : MonotoneLedger (d := d) L L')
265 (hneq : L ≠ L')
266 (hle : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ)) :
267 PostingStep (d := d) L L' := by
268 classical
269 -- helper: deltas
270 let dΔ : Fin d → ℤ := fun i => L'.debit i - L.debit i
271 let cΔ : Fin d → ℤ := fun i => L'.credit i - L.credit i
272 have hdNonneg : ∀ i : Fin d, 0 ≤ dΔ i := by
273 intro i
274 have : L.debit i ≤ L'.debit i := hmono.1 i
275 dsimp [dΔ]
276 linarith
277 have hcNonneg : ∀ i : Fin d, 0 ≤ cΔ i := by
278 intro i
279 have : L.credit i ≤ L'.credit i := hmono.2 i
280 dsimp [cΔ]
281 linarith
282
283 -- show every delta is ≤ 1 (otherwise cost would exceed Jlog 1)
284 have hdLeOne : ∀ i : Fin d, dΔ i ≤ 1 := by
285 intro i
286 by_contra hgt
287 have hlt : (1 : ℤ) < dΔ i := lt_of_not_ge hgt
288 have h2 : (2 : ℤ) ≤ dΔ i := by
289 -- `2 ≤ z ↔ 1 < z`
290 exact (Int.add_one_le_iff).2 hlt
291 -- strict lower bound on this term
292 have hx : (1 : ℝ) < ((dΔ i : ℤ) : ℝ) := by
293 -- cast `1 < dΔ i` to ℝ
294 exact_mod_cast hlt
295 have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((dΔ i : ℤ) : ℝ) :=
296 jlog_lt_jlog_of_one_lt (x := ((dΔ i : ℤ) : ℝ)) hx
297 -- this term is bounded by total cost (single term ≤ sum) and total cost ≤ Jlog 1: contradiction
298 let fD : Fin d → ℝ := fun j => Cost.Jlog ((dΔ j : ℤ) : ℝ)
299 have hterm_le_sum : fD i ≤ ∑ j : Fin d, fD j := by
300 -- `fD i ≤ sum univ fD` by nonneg
301 have hnonneg : ∀ j : Fin d, 0 ≤ fD j := fun _ => Cost.Jlog_nonneg _
302 -- use `i` in univ
303 -- work directly with `Finset.univ` to avoid rewriting via `Fintype.sum`
304 have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
305 Finset.single_le_sum (by
306 intro j hj
307 exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
308 simpa using this
309 have hsum_le_cost : (∑ j : Fin d, fD j) ≤ ledgerJlogCost (d := d) L L' := by
310 -- debit sum ≤ debit sum + credit sum
311 have hcredit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((cΔ j : ℤ) : ℝ) :=
312 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
313 dsimp [ledgerJlogCost, dΔ, cΔ]
314 exact le_add_of_nonneg_right hcredit_nonneg
315 have hterm_le_cost : Cost.Jlog ((dΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
316 -- rewrite `fD i` and compose inequalities
317 have : fD i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
318 simpa [fD] using this
319 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
320 lt_of_lt_of_le hterm_lt hterm_le_cost
321 exact (not_lt_of_ge hle) this
322
323 have hcLeOne : ∀ i : Fin d, cΔ i ≤ 1 := by
324 intro i
325 by_contra hgt
326 have hlt : (1 : ℤ) < cΔ i := lt_of_not_ge hgt
327 have hx : (1 : ℝ) < ((cΔ i : ℤ) : ℝ) := by exact_mod_cast hlt
328 have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((cΔ i : ℤ) : ℝ) :=
329 jlog_lt_jlog_of_one_lt (x := ((cΔ i : ℤ) : ℝ)) hx
330 let fC : Fin d → ℝ := fun j => Cost.Jlog ((cΔ j : ℤ) : ℝ)
331 have hterm_le_sum : fC i ≤ ∑ j : Fin d, fC j := by
332 have hnonneg : ∀ j : Fin d, 0 ≤ fC j := fun _ => Cost.Jlog_nonneg _
333 have : fC i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
334 Finset.single_le_sum (by
335 intro j hj
336 exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
337 simpa using this
338 have hsum_le_cost : (∑ j : Fin d, fC j) ≤ ledgerJlogCost (d := d) L L' := by
339 have hdebit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((dΔ j : ℤ) : ℝ) :=
340 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
341 dsimp [ledgerJlogCost, dΔ, cΔ]
342 exact le_add_of_nonneg_left hdebit_nonneg
343 have hterm_le_cost : Cost.Jlog ((cΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
344 have : fC i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
345 simpa [fC] using this
346 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
347 lt_of_lt_of_le hterm_lt hterm_le_cost
348 exact (not_lt_of_ge hle) this
349
350 -- Convert bounded deltas to `{0,1}` cases.
351 have hd01 : ∀ i : Fin d, dΔ i = 0 ∨ dΔ i = 1 := by
352 intro i
353 have h0 : 0 ≤ dΔ i := hdNonneg i
354 have h1 : dΔ i ≤ 1 := hdLeOne i
355 cases hdi : dΔ i with
356 | ofNat n =>
357 have hn : n ≤ 1 := by
358 have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hdi] using h1
359 exact (Int.ofNat_le).1 this
360 rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hdi]
361 | negSucc n =>
362 exfalso
363 have : ¬ (0 ≤ (Int.negSucc n)) := by
364 have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
365 exact not_le_of_gt this
366 exact this (by simpa [hdi] using h0)
367
368 have hc01 : ∀ i : Fin d, cΔ i = 0 ∨ cΔ i = 1 := by
369 intro i
370 have h0 : 0 ≤ cΔ i := hcNonneg i
371 have h1 : cΔ i ≤ 1 := hcLeOne i
372 cases hci : cΔ i with
373 | ofNat n =>
374 have hn : n ≤ 1 := by
375 have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hci] using h1
376 exact (Int.ofNat_le).1 this
377 rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hci]
378 | negSucc n =>
379 exfalso
380 have : ¬ (0 ≤ (Int.negSucc n)) := by
381 have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
382 exact not_le_of_gt this
383 exact this (by simpa [hci] using h0)
384
385 -- existence of some 1 (since L ≠ L')
386 have hex1 : (∃ i : Fin d, dΔ i = 1) ∨ (∃ i : Fin d, cΔ i = 1) := by
387 by_contra hnone
388 have hnoneD : ∀ i : Fin d, dΔ i = 0 := by
389 intro i
390 have : ¬ dΔ i = 1 := by
391 have : ¬ (∃ i : Fin d, dΔ i = 1) := (not_or.mp hnone).1
392 exact fun hi => this ⟨i, hi⟩
393 cases hd01 i with
394 | inl hz => exact hz
395 | inr h1 => exact (this h1).elim
396 have hnoneC : ∀ i : Fin d, cΔ i = 0 := by
397 intro i
398 have : ¬ cΔ i = 1 := by
399 have : ¬ (∃ i : Fin d, cΔ i = 1) := (not_or.mp hnone).2
400 exact fun hi => this ⟨i, hi⟩
401 cases hc01 i with
402 | inl hz => exact hz
403 | inr h1 => exact (this h1).elim
404 -- all deltas are 0 ⇒ ledger equal
405 cases L with
406 | mk debit credit =>
407 cases L' with
408 | mk debit' credit' =>
409 have hdebitEq : debit' = debit := by
410 funext i
411 have : debit' i - debit i = 0 := by simpa [dΔ] using hnoneD i
412 linarith
413 have hcreditEq : credit' = credit := by
414 funext i
415 have : credit' i - credit i = 0 := by simpa [cΔ] using hnoneC i
416 linarith
417 exact hneq (by cases hdebitEq; cases hcreditEq; rfl)
418 -- uniqueness: cannot have both a debit-1 and a credit-1, and cannot have two debit-1s, etc., else cost > Jlog 1.
419 have j1pos : 0 < Cost.Jlog (1 : ℝ) := by
420 have hnonneg : 0 ≤ Cost.Jlog (1 : ℝ) := Cost.Jlog_nonneg 1
421 have hne : Cost.Jlog (1 : ℝ) ≠ 0 := by
422 intro hzero
423 have : (1 : ℝ) = 0 := (Cost.Jlog_eq_zero_iff 1).mp hzero
424 norm_num at this
425 exact lt_of_le_of_ne hnonneg (Ne.symm hne)
426 have not_two_ones :
427 ¬((∃ i : Fin d, dΔ i = 1) ∧ (∃ j : Fin d, cΔ j = 1)) := by
428 intro hboth
429 rcases hboth with ⟨⟨i, hi⟩, ⟨j, hj⟩⟩
430 -- each side contributes at least Jlog 1
431 let fD : Fin d → ℝ := fun k => Cost.Jlog ((dΔ k : ℤ) : ℝ)
432 let fC : Fin d → ℝ := fun k => Cost.Jlog ((cΔ k : ℤ) : ℝ)
433 have hDi : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
434 -- `fD i = Jlog 1` and all terms nonneg
435 have hnonneg : ∀ k : Fin d, 0 ≤ fD k := fun _ => Cost.Jlog_nonneg _
436 have : fD i ≤ ∑ k : Fin d, fD k := by
437 have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
438 Finset.single_le_sum (by
439 intro k hk; exact hnonneg k) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
440 simpa using this
441 have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
442 simpa [fD, hi] using this
443 exact this
444 have hCj : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
445 have hnonneg : ∀ k : Fin d, 0 ≤ fC k := fun _ => Cost.Jlog_nonneg _
446 have : fC j ≤ ∑ k : Fin d, fC k := by
447 have : fC j ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
448 Finset.single_le_sum (by
449 intro k hk; exact hnonneg k) (by simp : j ∈ (Finset.univ : Finset (Fin d)))
450 simpa using this
451 have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
452 simpa [fC, hj] using this
453 exact this
454 -- so total cost ≥ 2*Jlog1
455 have hcost_ge :
456 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
457 -- debitSum + creditSum
458 dsimp [ledgerJlogCost, dΔ, cΔ]
459 exact add_le_add hDi hCj
460 have hlt : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
461 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
462 exact lt_of_lt_of_le this hcost_ge
463 exact (not_lt_of_ge hle) hlt
464
465 -- Choose which side has the unique 1.
466 cases hex1 with
467 | inl hd =>
468 rcases hd with ⟨k, hk⟩
469 have : ¬ (∃ j : Fin d, cΔ j = 1) := by
470 intro hc
471 exact not_two_ones ⟨⟨k, hk⟩, hc⟩
472 -- all credit deltas are 0
473 have hcAll0 : ∀ j : Fin d, cΔ j = 0 := by
474 intro j
475 have hn1 : ¬ cΔ j = 1 := by
476 intro hj
477 exact this ⟨j, hj⟩
478 cases hc01 j with
479 | inl hz => exact hz
480 | inr h1 => exact (hn1 h1).elim
481 -- all debit deltas are 0 except at k
482 have hdAll : ∀ j : Fin d, j ≠ k → dΔ j = 0 := by
483 intro j hjk
484 have hn1 : ¬ dΔ j = 1 := by
485 intro hj1
486 -- two debit ones would force cost > Jlog 1 similarly (simpler: use L1 minimality lemma later)
487 -- We can derive contradiction by comparing debitSum with two Jlog1 terms.
488 let fD : Fin d → ℝ := fun t => Cost.Jlog ((dΔ t : ℤ) : ℝ)
489 have hnonneg : ∀ t : Fin d, 0 ≤ fD t := fun _ => Cost.Jlog_nonneg _
490 have hi : fD k = Cost.Jlog (1 : ℝ) := by simpa [fD, hk]
491 have hj : fD j = Cost.Jlog (1 : ℝ) := by simpa [fD, hj1]
492 -- show debitSum ≥ fD k + fD j
493 have hsplit :=
494 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fD) (a := k) (by simp))
495 have hjmem : j ∈ (Finset.univ.erase k : Finset (Fin d)) := by simp [hjk]
496 have hj_le_rest :
497 fD j ≤ Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
498 exact Finset.single_le_sum (by
499 intro t ht; exact hnonneg t) hjmem
500 have hdebit_ge :
501 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ∑ t : Fin d, fD t := by
502 -- rewrite sum and use `hj_le_rest`
503 calc
504 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ)
505 = fD k + fD j := by simp [hi, hj]
506 _ ≤ fD k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
507 linarith
508 _ = ∑ t : Fin d, fD t := by simpa using hsplit.symm
509 -- total cost ≥ debitSum
510 have hcredit_nonneg : 0 ≤ ∑ t : Fin d, Cost.Jlog ((cΔ t : ℤ) : ℝ) :=
511 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
512 have hcost_ge : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
513 dsimp [ledgerJlogCost, dΔ, cΔ]
514 exact le_trans (le_trans hdebit_ge (le_add_of_nonneg_right hcredit_nonneg)) (le_rfl)
515 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
516 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
517 exact lt_of_lt_of_le this hcost_ge
518 exact (not_lt_of_ge hle) this
519 cases hd01 j with
520 | inl hz => exact hz
521 | inr h1 => exact (hn1 h1).elim
522 -- now show L' = post L k debit
523 refine ⟨k, Side.debit, ?_⟩
524 cases L with
525 | mk debit credit =>
526 cases L' with
527 | mk debit' credit' =>
528 have hdebit' : debit' = fun i => if i = k then debit i + 1 else debit i := by
529 funext i
530 by_cases hik : i = k
531 · subst hik
532 have hdiff : debit' i - debit i = 1 := by simpa [dΔ] using hk
533 have : debit' i = debit i + 1 := by linarith
534 simpa using this
535 · have : debit' i - debit i = 0 := by
536 have := hdAll i hik
537 simpa [dΔ] using this
538 simp [hik]
539 linarith
540 have hcredit' : credit' = credit := by
541 funext i
542 have : credit' i - credit i = 0 := by simpa [cΔ] using hcAll0 i
543 linarith
544 subst hdebit' hcredit'
545 simp [post]
546 ext i <;> by_cases h : i = k <;> simp [h]
547 | inr hc =>
548 rcases hc with ⟨k, hk⟩
549 have : ¬ (∃ j : Fin d, dΔ j = 1) := by
550 intro hd
551 exact not_two_ones ⟨hd, ⟨k, hk⟩⟩
552 -- symmetric to debit case: build post on credit
553 have hdAll0 : ∀ j : Fin d, dΔ j = 0 := by
554 intro j
555 have hn1 : ¬ dΔ j = 1 := by
556 intro hj
557 exact this ⟨j, hj⟩
558 cases hd01 j with
559 | inl hz => exact hz
560 | inr h1 => exact (hn1 h1).elim
561 have hcAll : ∀ j : Fin d, j ≠ k → cΔ j = 0 := by
562 intro j hjk
563 have hn1 : ¬ cΔ j = 1 := by
564 intro hj1
565 -- two credit ones would force cost > Jlog 1 (same argument as in debit case)
566 let fC : Fin d → ℝ := fun t => Cost.Jlog ((cΔ t : ℤ) : ℝ)
567 have hnonneg : ∀ t : Fin d, 0 ≤ fC t := fun _ => Cost.Jlog_nonneg _
568 have hi : fC k = Cost.Jlog (1 : ℝ) := by simpa [fC, hk]
569 have hj : fC j = Cost.Jlog (1 : ℝ) := by simpa [fC, hj1]
570 have hsplit :=
571 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fC) (a := k) (by simp))
572 have hjmem : j ∈ (Finset.univ.erase k : Finset (Fin d)) := by simp [hjk]
573 have hj_le_rest :
574 fC j ≤ Finset.sum (Finset.univ.erase k : Finset (Fin d)) fC := by
575 exact Finset.single_le_sum (by
576 intro t ht; exact hnonneg t) hjmem
577 have hcredit_ge :
578 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ∑ t : Fin d, fC t := by
579 calc
580 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ)
581 = fC k + fC j := by simp [hi, hj]
582 _ ≤ fC k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) fC := by
583 linarith
584 _ = ∑ t : Fin d, fC t := by simpa using hsplit.symm
585 have hdebit_nonneg : 0 ≤ ∑ t : Fin d, Cost.Jlog ((dΔ t : ℤ) : ℝ) :=
586 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
587 have hcost_ge : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
588 dsimp [ledgerJlogCost, dΔ, cΔ]
589 exact le_trans (le_trans hcredit_ge (le_add_of_nonneg_left hdebit_nonneg)) (le_rfl)
590 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
591 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
592 exact lt_of_lt_of_le this hcost_ge
593 exact (not_lt_of_ge hle) this
594 cases hc01 j with
595 | inl hz => exact hz
596 | inr h1 => exact (hn1 h1).elim
597 refine ⟨k, Side.credit, ?_⟩
598 cases L with
599 | mk debit credit =>
600 cases L' with
601 | mk debit' credit' =>
602 have hcredit' : credit' = fun i => if i = k then credit i + 1 else credit i := by
603 funext i
604 by_cases hik : i = k
605 · subst hik
606 have hdiff : credit' i - credit i = 1 := by simpa [cΔ] using hk
607 have : credit' i = credit i + 1 := by linarith
608 simpa using this
609 · have : credit' i - credit i = 0 := by
610 have := hcAll i hik
611 simpa [cΔ] using this
612 simp [hik]
613 linarith
614 have hdebit' : debit' = debit := by
615 funext i
616 have : debit' i - debit i = 0 := by simpa [dΔ] using hdAll0 i
617 linarith
618 subst hcredit' hdebit'
619 simp [post]
620 ext i <;> by_cases h : i = k <;> simp [h]
621
622/-- Every monotone nontrivial transition costs at least one unit of `Jlog`.
623Together with `ledgerJlogCost_eq_Jlog1_of_postingStep`, this makes the
624minimum-J posting semantics used downstream explicitly non-vacuous. -/
625theorem Jlog1_le_ledgerJlogCost_of_monotone_nontrivial
626 {d : Nat} {L L' : LedgerState d}
627 (hmono : MonotoneLedger (d := d) L L')
628 (hneq : L ≠ L') :
629 Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
630 by_contra hnot
631 have hlt :
632 ledgerJlogCost (d := d) L L' < Cost.Jlog (1 : ℝ) :=
633 lt_of_not_ge hnot
634 have hpost :
635 PostingStep (d := d) L L' :=
636 postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1
637 hmono hneq (le_of_lt hlt)
638 have heq :=
639 ledgerJlogCost_eq_Jlog1_of_postingStep hpost
640 linarith
641
642/-! ### Zero-cost characterization -/
643
644theorem ledgerL1Cost_eq_zero_iff {d : Nat} (L L' : LedgerState d) :
645 ledgerL1Cost (d := d) L L' = 0 ↔ L' = L := by
646 classical
647 cases L with
648 | mk debit credit =>
649 cases L' with
650 | mk debit' credit' =>
651 constructor
652 · intro h0
653 -- split into debit/credit sums
654 let dSum : Nat := ∑ i : Fin d, Int.natAbs (debit' i - debit i)
655 let cSum : Nat := ∑ i : Fin d, Int.natAbs (credit' i - credit i)
656 have hsplit : dSum + cSum = 0 := by
657 simpa [ledgerL1Cost, dSum, cSum] using h0
658 have hd0 : dSum = 0 ∧ cSum = 0 := Nat.add_eq_zero_iff.mp hsplit
659 have hdebit0 :
660 ∀ i : Fin d, Int.natAbs (debit' i - debit i) = 0 := by
661 have h' :
662 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (debit' i - debit i)) = 0 := by
663 simpa [dSum] using hd0.1
664 have hall :=
665 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
666 (f := fun i => Int.natAbs (debit' i - debit i))
667 (fun _ _ => Nat.zero_le _)).1 h'
668 intro i
669 exact hall i (by simp)
670 have hcredit0 :
671 ∀ i : Fin d, Int.natAbs (credit' i - credit i) = 0 := by
672 have h' :
673 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (credit' i - credit i)) = 0 := by
674 simpa [cSum] using hd0.2
675 have hall :=
676 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
677 (f := fun i => Int.natAbs (credit' i - credit i))
678 (fun _ _ => Nat.zero_le _)).1 h'
679 intro i
680 exact hall i (by simp)
681 have hdebitEq : debit' = debit := by
682 funext i
683 have hz : (debit' i - debit i) = 0 := Int.natAbs_eq_zero.mp (hdebit0 i)
684 linarith
685 have hcreditEq : credit' = credit := by
686 funext i
687 have hz : (credit' i - credit i) = 0 := Int.natAbs_eq_zero.mp (hcredit0 i)
688 linarith
689 subst hdebitEq hcreditEq
690 rfl
691 · intro hEq
692 cases hEq
693 simp [ledgerL1Cost]
694
695/-! ### Posting steps satisfy `LegalAtomicTick` (and conversely, by `legalAtomicTick_implies_PostingStep`) -/
696
697private lemma post_monotone {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
698 MonotoneLedger (d := d) L (post L k side) := by
699 classical
700 cases side with
701 | debit =>
702 refine ⟨?_, ?_⟩
703 · intro i
704 by_cases hik : i = k
705 · subst hik
706 simp [post]
707 · simp [post, hik]
708 · intro i
709 simp [post]
710 | credit =>
711 refine ⟨?_, ?_⟩
712 · intro i
713 simp [post]
714 · intro i
715 by_cases hik : i = k
716 · subst hik
717 simp [post]
718 · simp [post, hik]
719
720private lemma ledgerL1Cost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
721 ledgerL1Cost (d := d) L (post L k side) = 1 := by
722 classical
723 cases side with
724 | debit =>
725 -- debit changes by +1 at k; credit unchanged
726 have hdebit :
727 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).debit i - L.debit i)) = 1 := by
728 -- isolate `k` and show everything else is 0
729 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.debit).debit i - L.debit i)
730 have hsplit :=
731 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
732 have fk : f k = 1 := by
733 simp [f, post]
734 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
735 refine Finset.sum_eq_zero ?_
736 intro i hi
737 have hik : i ≠ k := by
738 simpa [Finset.mem_erase] using hi
739 simp [f, post, hik]
740 -- rewrite `∑ univ` using `hsplit.symm`
741 simpa [f] using (by
742 calc
743 (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
744 simpa using hsplit.symm
745 _ = 1 := by simp [fk, hErase])
746 have hcredit :
747 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i - L.credit i)) = 0 := by
748 -- credit is unchanged everywhere
749 refine Finset.sum_eq_zero ?_
750 intro i _
751 simp [post]
752 -- assemble
753 simp [ledgerL1Cost, hdebit, hcredit]
754 | credit =>
755 -- credit changes by +1 at k; debit unchanged
756 have hdebit :
757 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).debit i - L.debit i)) = 0 := by
758 refine Finset.sum_eq_zero ?_
759 intro i _
760 simp [post]
761 have hcredit :
762 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).credit i - L.credit i)) = 1 := by
763 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.credit).credit i - L.credit i)
764 have hsplit :=
765 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
766 have fk : f k = 1 := by
767 simp [f, post]
768 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
769 refine Finset.sum_eq_zero ?_
770 intro i hi
771 have hik : i ≠ k := by
772 simpa [Finset.mem_erase] using hi
773 simp [f, post, hik]
774 simpa [f] using (by
775 calc
776 (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
777 simpa using hsplit.symm
778 _ = 1 := by simp [fk, hErase])
779 simp [ledgerL1Cost, hdebit, hcredit]
780
781theorem legalAtomicTick_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
782 LegalAtomicTick (d := d) L (post L k side) := by
783 refine ⟨post_monotone (d := d) L k side, ledgerL1Cost_post (d := d) L k side⟩
784
785theorem postingStep_implies_legalAtomicTick {d : Nat} {L L' : LedgerState d}
786 (h : PostingStep (d := d) L L') : LegalAtomicTick (d := d) L L' := by
787 rcases h with ⟨k, side, rfl⟩
788 exact legalAtomicTick_of_post (d := d) L k side
789
790private lemma int_natAbs_eq_one_of_nonneg {z : ℤ} (hz : Int.natAbs z = 1) (hznn : 0 ≤ z) :
791 z = 1 := by
792 cases z with
793 | ofNat n =>
794 -- natAbs (ofNat n) = n
795 have : n = 1 := by simpa using hz
796 simpa [this]
797 | negSucc n =>
798 -- negative contradiction
799 have : ¬ (0 ≤ Int.negSucc n) := by
800 -- `negSucc n = -(n+1) < 0`
801 have : Int.negSucc n < 0 := by
802 simpa using (Int.negSucc_lt_zero n)
803 exact not_le_of_gt this
804 exact (this hznn).elim
805
806private lemma int_eq_of_natAbs_eq_zero {z : ℤ} (hz : Int.natAbs z = 0) : z = 0 := by
807 exact (Int.natAbs_eq_zero.mp hz)
808
809private lemma exists_unique_of_sum_univ_eq_one {d : Nat} (f : Fin d → Nat)
810 (hs : (∑ i : Fin d, f i) = 1) :
811 ∃ k : Fin d, f k = 1 ∧ ∀ i : Fin d, i ≠ k → f i = 0 := by
812 classical
813 have hs_ne0 : (∑ i : Fin d, f i) ≠ 0 := by
814 simpa [hs] using Nat.one_ne_zero
815 obtain ⟨k, _hkMem, hkne0⟩ := Finset.exists_ne_zero_of_sum_ne_zero (s := (Finset.univ : Finset (Fin d)))
816 (f := fun i => f i) hs_ne0
817 have hdecomp : f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 1 := by
818 -- `f k + sum (erase k) = sum univ`
819 have := (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fun i => f i) (a := k) (by simp))
820 simpa [hs] using this
821 have hk_cases := Nat.add_eq_one_iff.mp hdecomp
822 have hk1 : f k = 1 ∧ Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
823 cases hk_cases with
824 | inl h0 =>
825 -- f k = 0 contradicts hkne0
826 exfalso
827 exact hkne0 h0.1
828 | inr h1 =>
829 exact h1
830 refine ⟨k, hk1.1, ?_⟩
831 intro i hik
832 have hi' : i ∈ (Finset.univ.erase k : Finset (Fin d)) := by
833 simp [Finset.mem_erase, hik]
834 -- sum=0 on erase ⇒ every term on erase is 0
835 have hall0 :
836 ∀ j : Fin d, j ∈ (Finset.univ.erase k : Finset (Fin d)) → f j = 0 := by
837 have :=
838 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ.erase k : Finset (Fin d)))
839 (f := fun j => f j) (fun _ _ => Nat.zero_le _)).1 hk1.2
840 simpa using this
841 exact hall0 i hi'
842
843theorem legalAtomicTick_implies_PostingStep {d : Nat} {L L' : LedgerState d}
844 (h : LegalAtomicTick (d := d) L L') : PostingStep (d := d) L L' := by
845 classical
846 rcases h with ⟨hmono, hcost⟩
847 rcases hmono with ⟨hmonoD, hmonoC⟩
848 -- split the total cost into debit-cost and credit-cost
849 let dCost : Nat := ∑ i : Fin d, Int.natAbs (L'.debit i - L.debit i)
850 let cCost : Nat := ∑ i : Fin d, Int.natAbs (L'.credit i - L.credit i)
851 have hsplit : dCost + cCost = 1 := by
852 simpa [ledgerL1Cost, dCost, cCost] using hcost
853 have hcases := Nat.add_eq_one_iff.mp hsplit
854 cases hcases with
855 | inl hc =>
856 -- dCost = 0, cCost = 1 → credit posting
857 have hd0 : dCost = 0 := hc.1
858 have hc1 : cCost = 1 := hc.2
859 -- choose the unique changed credit coordinate
860 have ⟨k, hk1, hkrest⟩ :=
861 exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.credit i - L.credit i)) hc1
862 -- debit diffs all 0
863 have hdAll :
864 ∀ i : Fin d, Int.natAbs (L'.debit i - L.debit i) = 0 := by
865 have hall0 :
866 ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.debit i - L.debit i) = 0 := by
867 have :=
868 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
869 (f := fun i => Int.natAbs (L'.debit i - L.debit i))
870 (fun _ _ => Nat.zero_le _)).1 hd0
871 simpa [dCost] using this
872 intro i; exact hall0 i (by simp)
873 -- build PostingStep = post at k on credit side
874 refine ⟨k, Side.credit, ?_⟩
875 -- prove L' = post L k credit by field ext (no `[ext]` lemma registered)
876 cases L with
877 | mk debit credit =>
878 cases L' with
879 | mk debit' credit' =>
880 -- show the debit field is unchanged
881 have hdebit' : debit' = debit := by
882 funext i
883 have hz := int_eq_of_natAbs_eq_zero (hdAll i)
884 have hz' : (debit' i - debit i) = 0 := by simpa using hz
885 linarith
886 -- show the credit field matches the `post` update
887 have hcredit' :
888 credit' = (fun i => if i = k then credit i + 1 else credit i) := by
889 funext i
890 by_cases hik : i = k
891 · subst hik
892 -- goal reduces to `credit' i = credit i + 1`
893 simp
894 have hzabs : Int.natAbs (credit' i - credit i) = 1 := hk1
895 have hnn : 0 ≤ (credit' i - credit i) := by
896 have : credit i ≤ credit' i := hmonoC i
897 linarith
898 have hz : (credit' i - credit i) = 1 :=
899 int_natAbs_eq_one_of_nonneg (z := (credit' i - credit i)) hzabs hnn
900 linarith
901 · -- goal reduces to `credit' i = credit i`
902 have hzabs : Int.natAbs (credit' i - credit i) = 0 := hkrest i hik
903 have hz : (credit' i - credit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
904 simp [hik]
905 linarith
906 -- finish
907 subst hdebit' hcredit'
908 simp [post]
909 ext i <;> by_cases h : i = k <;> simp [h]
910 | inr hc =>
911 -- dCost = 1, cCost = 0 → debit posting
912 have hd1 : dCost = 1 := hc.1
913 have hc0 : cCost = 0 := hc.2
914 have ⟨k, hk1, hkrest⟩ :=
915 exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.debit i - L.debit i)) hd1
916 have hcAll :
917 ∀ i : Fin d, Int.natAbs (L'.credit i - L.credit i) = 0 := by
918 have hall0 :
919 ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.credit i - L.credit i) = 0 := by
920 have :=
921 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
922 (f := fun i => Int.natAbs (L'.credit i - L.credit i))
923 (fun _ _ => Nat.zero_le _)).1 hc0
924 simpa [cCost] using this
925 intro i; exact hall0 i (by simp)
926 refine ⟨k, Side.debit, ?_⟩
927 cases L with
928 | mk debit credit =>
929 cases L' with
930 | mk debit' credit' =>
931 have hcredit' : credit' = credit := by
932 funext i
933 have hz := int_eq_of_natAbs_eq_zero (hcAll i)
934 have hz' : (credit' i - credit i) = 0 := by simpa using hz
935 linarith
936 have hdebit' :
937 debit' = (fun i => if i = k then debit i + 1 else debit i) := by
938 funext i
939 by_cases hik : i = k
940 · subst hik
941 simp
942 have hzabs : Int.natAbs (debit' i - debit i) = 1 := hk1
943 have hnn : 0 ≤ (debit' i - debit i) := by
944 have : debit i ≤ debit' i := hmonoD i
945 linarith
946 have hz : (debit' i - debit i) = 1 :=
947 int_natAbs_eq_one_of_nonneg (z := (debit' i - debit i)) hzabs hnn
948 linarith
949 · have hzabs : Int.natAbs (debit' i - debit i) = 0 := hkrest i hik
950 have hz : (debit' i - debit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
951 simp [hik]
952 linarith
953 subst hcredit' hdebit'
954 simp [post]
955 ext i <;> by_cases h : i = k <;> simp [h]
956
957theorem postingStep_iff_legalAtomicTick {d : Nat} {L L' : LedgerState d} :
958 PostingStep (d := d) L L' ↔ LegalAtomicTick (d := d) L L' :=
959 ⟨postingStep_implies_legalAtomicTick (d := d), legalAtomicTick_implies_PostingStep (d := d)⟩
960
961/-! ### Optional B3-style tightening: minimal cost (among monotone, nontrivial steps) ⇒ posting -/
962
963theorem minCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
964 {L L' : LedgerState d}
965 (hmono : MonotoneLedger (d := d) L L')
966 (hneq : L ≠ L')
967 (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
968 ledgerL1Cost (d := d) L L' ≤ ledgerL1Cost (d := d) L L'') :
969 PostingStep (d := d) L L' := by
970 classical
971 -- compare against a concrete single-post candidate (cost = 1)
972 let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
973 have hpostNe : L ≠ post L k0 Side.debit := by
974 intro hEq
975 have hdeb : L.debit k0 = L.debit k0 + 1 := by
976 -- RHS is `L.debit k0 + 1`
977 have := congrArg (fun s => s.debit k0) hEq
978 simpa [post] using this
979 linarith
980 have hle1 : ledgerL1Cost (d := d) L L' ≤ 1 := by
981 have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
982 post_monotone (d := d) L k0 Side.debit
983 have hcost' : ledgerL1Cost (d := d) L (post L k0 Side.debit) = 1 :=
984 ledgerL1Cost_post (d := d) L k0 Side.debit
985 have := hmin (post L k0 Side.debit) hmono' hpostNe
986 simpa [hcost'] using this
987 have hcostNe0 : ledgerL1Cost (d := d) L L' ≠ 0 := by
988 intro h0
989 have : L' = L := (ledgerL1Cost_eq_zero_iff (d := d) L L').1 h0
990 exact hneq (by simpa [this])
991 have hcost1 : ledgerL1Cost (d := d) L L' = 1 := by
992 have hcases := Nat.le_one_iff_eq_zero_or_eq_one.1 hle1
993 cases hcases with
994 | inl h0 => exact (hcostNe0 h0).elim
995 | inr h1 => exact h1
996 -- conclude via the `PostingStep ↔ LegalAtomicTick` equivalence
997 have hlegal : LegalAtomicTick (d := d) L L' := ⟨hmono, hcost1⟩
998 exact (postingStep_iff_legalAtomicTick (d := d)).2 hlegal
999
1000/-! ### Optional B4-style tightening: Jlog-cost minimality (among monotone, nontrivial steps) ⇒ posting -/
1001
1002theorem minJlogCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
1003 {L L' : LedgerState d}
1004 (hmono : MonotoneLedger (d := d) L L')
1005 (hneq : L ≠ L')
1006 (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
1007 ledgerJlogCost (d := d) L L' ≤ ledgerJlogCost (d := d) L L'') :
1008 PostingStep (d := d) L L' := by
1009 classical
1010 -- compare against a concrete single-post candidate (Jlog-cost = Jlog 1)
1011 let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
1012 have hpostNe : L ≠ post L k0 Side.debit := by
1013 intro hEq
1014 have hdeb : L.debit k0 = L.debit k0 + 1 := by
1015 have := congrArg (fun s => s.debit k0) hEq
1016 simpa [post] using this
1017 linarith
1018 have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
1019 post_monotone (d := d) L k0 Side.debit
1020 have hcost' : ledgerJlogCost (d := d) L (post L k0 Side.debit) = Cost.Jlog (1 : ℝ) :=
1021 ledgerJlogCost_post (d := d) L k0 Side.debit
1022 have hleJ1 : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ) := by
1023 have := hmin (post L k0 Side.debit) hmono' hpostNe
1024 simpa [hcost'] using this
1025 exact postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 (d := d) (L := L) (L' := L') hmono hneq hleJ1
1026
1027theorem legalAtomicTick_oneBitDiff {d : Nat} {L L' : LedgerState d}
1028 (h : LegalAtomicTick (d := d) L L') :
1029 OneBitDiff (parity d L) (parity d L') :=
1030 postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep (d := d) h)
1031
1032/-! ## Workstream B tightening: RS AtomicTick ⇒ PostingStep (legality predicate) -/
1033
1034/-- Choose the unique posted account at tick `t` from an RS `AtomicTick` instance. -/
1035noncomputable def accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) : Fin d :=
1036 Classical.choose (ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t))
1037
1038lemma postedAt_accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) :
1039 AtomicTick.postedAt (M := AccountRS d) t (accountAt (d := d) t) := by
1040 have hex : ∃ u : Fin d, AtomicTick.postedAt (M := AccountRS d) t u :=
1041 ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t)
1042 simpa [accountAt] using (Classical.choose_spec hex)
1043
1044/-- An RS-atomic tick step, parameterized by an explicit debit/credit side schedule. -/
1045noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1046 LedgerState d :=
1047 post L (accountAt (d := d) t) (sideAt t)
1048
1049lemma stepAt_isPostingStep {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1050 PostingStep (d := d) L (stepAt (d := d) sideAt t L) := by
1051 refine ⟨accountAt (d := d) t, sideAt t, rfl⟩
1052
1053theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1054 OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=
1055 postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1056
1057/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/
1058
1059/-- A per-tick posting instruction: (account index, side). -/
1060abbrev PostInstr (d : Nat) : Type := Fin d × Side
1061
1062/-- Run a ledger forward under a per-tick posting schedule. -/
1063noncomputable def run {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) : Nat → LedgerState d
1064| 0 => L0
1065| (t + 1) =>
1066 let prev := run L0 sched t
1067 post prev (sched t).1 (sched t).2
1068
1069theorem run_step_oneBitDiff {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) (t : Nat) :
1070 OneBitDiff (parity d (run L0 sched t)) (parity d (run L0 sched (t + 1))) := by
1071 -- unfold one step of `run` and apply the single-post theorem
1072 simp [run, parity_oneBitDiff_of_post, parity]
1073
1074end LedgerPostingAdjacency
1075end IndisputableMonolith
1076