IndisputableMonolith.LedgerPostingAdjacency
IndisputableMonolith/LedgerPostingAdjacency.lean · 1043 lines · 43 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Recognition
3import IndisputableMonolith.Cost.Jlog
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/-! ### Jlog-cost tightening: if a monotone nontrivial tick has Jlog-cost ≤ Jlog(1), it is a posting step. -/
242
243private lemma intCast_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) : ((z : ℤ) : ℝ) ≠ 0 := by
244 exact_mod_cast hz
245
246private lemma jlog_lt_jlog_of_one_lt {x : ℝ} (hx : 1 < x) :
247 Cost.Jlog (1 : ℝ) < Cost.Jlog x := by
248 -- strict monotone on `Ici 0`, and `1 < x` implies `0 ≤ 1` and `0 ≤ x`
249 have hmono := Cost.Jlog_strictMonoOn_Ici0
250 have hx0 : (0 : ℝ) ≤ x := le_trans (show (0 : ℝ) ≤ (1 : ℝ) by linarith) (le_of_lt hx)
251 exact hmono (by simp) (by simpa [Set.mem_Ici] using hx0) hx
252
253theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 {d : Nat} {L L' : LedgerState d}
254 (hmono : MonotoneLedger (d := d) L L')
255 (hneq : L ≠ L')
256 (hle : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ)) :
257 PostingStep (d := d) L L' := by
258 classical
259 -- helper: deltas
260 let dΔ : Fin d → ℤ := fun i => L'.debit i - L.debit i
261 let cΔ : Fin d → ℤ := fun i => L'.credit i - L.credit i
262 have hdNonneg : ∀ i : Fin d, 0 ≤ dΔ i := by
263 intro i
264 have : L.debit i ≤ L'.debit i := hmono.1 i
265 dsimp [dΔ]
266 linarith
267 have hcNonneg : ∀ i : Fin d, 0 ≤ cΔ i := by
268 intro i
269 have : L.credit i ≤ L'.credit i := hmono.2 i
270 dsimp [cΔ]
271 linarith
272
273 -- show every delta is ≤ 1 (otherwise cost would exceed Jlog 1)
274 have hdLeOne : ∀ i : Fin d, dΔ i ≤ 1 := by
275 intro i
276 by_contra hgt
277 have hlt : (1 : ℤ) < dΔ i := lt_of_not_ge hgt
278 have h2 : (2 : ℤ) ≤ dΔ i := by
279 -- `2 ≤ z ↔ 1 < z`
280 exact (Int.add_one_le_iff).2 hlt
281 -- strict lower bound on this term
282 have hx : (1 : ℝ) < ((dΔ i : ℤ) : ℝ) := by
283 -- cast `1 < dΔ i` to ℝ
284 exact_mod_cast hlt
285 have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((dΔ i : ℤ) : ℝ) :=
286 jlog_lt_jlog_of_one_lt (x := ((dΔ i : ℤ) : ℝ)) hx
287 -- this term is bounded by total cost (single term ≤ sum) and total cost ≤ Jlog 1: contradiction
288 let fD : Fin d → ℝ := fun j => Cost.Jlog ((dΔ j : ℤ) : ℝ)
289 have hterm_le_sum : fD i ≤ ∑ j : Fin d, fD j := by
290 -- `fD i ≤ sum univ fD` by nonneg
291 have hnonneg : ∀ j : Fin d, 0 ≤ fD j := fun _ => Cost.Jlog_nonneg _
292 -- use `i` in univ
293 -- work directly with `Finset.univ` to avoid rewriting via `Fintype.sum`
294 have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
295 Finset.single_le_sum (by
296 intro j hj
297 exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
298 simpa using this
299 have hsum_le_cost : (∑ j : Fin d, fD j) ≤ ledgerJlogCost (d := d) L L' := by
300 -- debit sum ≤ debit sum + credit sum
301 have hcredit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((cΔ j : ℤ) : ℝ) :=
302 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
303 dsimp [ledgerJlogCost, dΔ, cΔ]
304 exact le_add_of_nonneg_right hcredit_nonneg
305 have hterm_le_cost : Cost.Jlog ((dΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
306 -- rewrite `fD i` and compose inequalities
307 have : fD i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
308 simpa [fD] using this
309 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
310 lt_of_lt_of_le hterm_lt hterm_le_cost
311 exact (not_lt_of_ge hle) this
312
313 have hcLeOne : ∀ i : Fin d, cΔ i ≤ 1 := by
314 intro i
315 by_contra hgt
316 have hlt : (1 : ℤ) < cΔ i := lt_of_not_ge hgt
317 have hx : (1 : ℝ) < ((cΔ i : ℤ) : ℝ) := by exact_mod_cast hlt
318 have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((cΔ i : ℤ) : ℝ) :=
319 jlog_lt_jlog_of_one_lt (x := ((cΔ i : ℤ) : ℝ)) hx
320 let fC : Fin d → ℝ := fun j => Cost.Jlog ((cΔ j : ℤ) : ℝ)
321 have hterm_le_sum : fC i ≤ ∑ j : Fin d, fC j := by
322 have hnonneg : ∀ j : Fin d, 0 ≤ fC j := fun _ => Cost.Jlog_nonneg _
323 have : fC i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
324 Finset.single_le_sum (by
325 intro j hj
326 exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
327 simpa using this
328 have hsum_le_cost : (∑ j : Fin d, fC j) ≤ ledgerJlogCost (d := d) L L' := by
329 have hdebit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((dΔ j : ℤ) : ℝ) :=
330 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
331 dsimp [ledgerJlogCost, dΔ, cΔ]
332 exact le_add_of_nonneg_left hdebit_nonneg
333 have hterm_le_cost : Cost.Jlog ((cΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
334 have : fC i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
335 simpa [fC] using this
336 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
337 lt_of_lt_of_le hterm_lt hterm_le_cost
338 exact (not_lt_of_ge hle) this
339
340 -- Convert bounded deltas to `{0,1}` cases.
341 have hd01 : ∀ i : Fin d, dΔ i = 0 ∨ dΔ i = 1 := by
342 intro i
343 have h0 : 0 ≤ dΔ i := hdNonneg i
344 have h1 : dΔ i ≤ 1 := hdLeOne i
345 cases hdi : dΔ i with
346 | ofNat n =>
347 have hn : n ≤ 1 := by
348 have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hdi] using h1
349 exact (Int.ofNat_le).1 this
350 rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hdi]
351 | negSucc n =>
352 exfalso
353 have : ¬ (0 ≤ (Int.negSucc n)) := by
354 have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
355 exact not_le_of_gt this
356 exact this (by simpa [hdi] using h0)
357
358 have hc01 : ∀ i : Fin d, cΔ i = 0 ∨ cΔ i = 1 := by
359 intro i
360 have h0 : 0 ≤ cΔ i := hcNonneg i
361 have h1 : cΔ i ≤ 1 := hcLeOne i
362 cases hci : cΔ i with
363 | ofNat n =>
364 have hn : n ≤ 1 := by
365 have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hci] using h1
366 exact (Int.ofNat_le).1 this
367 rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hci]
368 | negSucc n =>
369 exfalso
370 have : ¬ (0 ≤ (Int.negSucc n)) := by
371 have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
372 exact not_le_of_gt this
373 exact this (by simpa [hci] using h0)
374
375 -- existence of some 1 (since L ≠ L')
376 have hex1 : (∃ i : Fin d, dΔ i = 1) ∨ (∃ i : Fin d, cΔ i = 1) := by
377 by_contra hnone
378 have hnoneD : ∀ i : Fin d, dΔ i = 0 := by
379 intro i
380 have : ¬ dΔ i = 1 := by
381 have : ¬ (∃ i : Fin d, dΔ i = 1) := (not_or.mp hnone).1
382 exact fun hi => this ⟨i, hi⟩
383 cases hd01 i with
384 | inl hz => exact hz
385 | inr h1 => exact (this h1).elim
386 have hnoneC : ∀ i : Fin d, cΔ i = 0 := by
387 intro i
388 have : ¬ cΔ i = 1 := by
389 have : ¬ (∃ i : Fin d, cΔ i = 1) := (not_or.mp hnone).2
390 exact fun hi => this ⟨i, hi⟩
391 cases hc01 i with
392 | inl hz => exact hz
393 | inr h1 => exact (this h1).elim
394 -- all deltas are 0 ⇒ ledger equal
395 cases L with
396 | mk debit credit =>
397 cases L' with
398 | mk debit' credit' =>
399 have hdebitEq : debit' = debit := by
400 funext i
401 have : debit' i - debit i = 0 := by simpa [dΔ] using hnoneD i
402 linarith
403 have hcreditEq : credit' = credit := by
404 funext i
405 have : credit' i - credit i = 0 := by simpa [cΔ] using hnoneC i
406 linarith
407 exact hneq (by cases hdebitEq; cases hcreditEq; rfl)
408 -- uniqueness: cannot have both a debit-1 and a credit-1, and cannot have two debit-1s, etc., else cost > Jlog 1.
409 have j1pos : 0 < Cost.Jlog (1 : ℝ) := by
410 -- `1 ≠ 0`
411 have : (1 : ℝ) ≠ 0 := by norm_num
412 exact (Cost.Jlog_pos_iff (1 : ℝ)).2 this
413 have not_two_ones :
414 ¬((∃ i : Fin d, dΔ i = 1) ∧ (∃ j : Fin d, cΔ j = 1)) := by
415 intro hboth
416 rcases hboth with ⟨⟨i, hi⟩, ⟨j, hj⟩⟩
417 -- each side contributes at least Jlog 1
418 let fD : Fin d → ℝ := fun k => Cost.Jlog ((dΔ k : ℤ) : ℝ)
419 let fC : Fin d → ℝ := fun k => Cost.Jlog ((cΔ k : ℤ) : ℝ)
420 have hDi : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
421 -- `fD i = Jlog 1` and all terms nonneg
422 have hnonneg : ∀ k : Fin d, 0 ≤ fD k := fun _ => Cost.Jlog_nonneg _
423 have : fD i ≤ ∑ k : Fin d, fD k := by
424 have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
425 Finset.single_le_sum (by
426 intro k hk; exact hnonneg k) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
427 simpa using this
428 have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
429 simpa [fD, hi] using this
430 exact this
431 have hCj : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
432 have hnonneg : ∀ k : Fin d, 0 ≤ fC k := fun _ => Cost.Jlog_nonneg _
433 have : fC j ≤ ∑ k : Fin d, fC k := by
434 have : fC j ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
435 Finset.single_le_sum (by
436 intro k hk; exact hnonneg k) (by simp : j ∈ (Finset.univ : Finset (Fin d)))
437 simpa using this
438 have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
439 simpa [fC, hj] using this
440 exact this
441 -- so total cost ≥ 2*Jlog1
442 have hcost_ge :
443 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
444 -- debitSum + creditSum
445 dsimp [ledgerJlogCost, dΔ, cΔ]
446 exact add_le_add hDi hCj
447 have hlt : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
448 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
449 exact lt_of_lt_of_le this hcost_ge
450 exact (not_lt_of_ge hle) hlt
451
452 -- Choose which side has the unique 1.
453 cases hex1 with
454 | inl hd =>
455 rcases hd with ⟨k, hk⟩
456 have : ¬ (∃ j : Fin d, cΔ j = 1) := by
457 intro hc
458 exact not_two_ones ⟨⟨k, hk⟩, hc⟩
459 -- all credit deltas are 0
460 have hcAll0 : ∀ j : Fin d, cΔ j = 0 := by
461 intro j
462 have hn1 : ¬ cΔ j = 1 := by
463 intro hj
464 exact this ⟨j, hj⟩
465 cases hc01 j with
466 | inl hz => exact hz
467 | inr h1 => exact (hn1 h1).elim
468 -- all debit deltas are 0 except at k
469 have hdAll : ∀ j : Fin d, j ≠ k → dΔ j = 0 := by
470 intro j hjk
471 have hn1 : ¬ dΔ j = 1 := by
472 intro hj1
473 -- two debit ones would force cost > Jlog 1 similarly (simpler: use L1 minimality lemma later)
474 -- We can derive contradiction by comparing debitSum with two Jlog1 terms.
475 let fD : Fin d → ℝ := fun t => Cost.Jlog ((dΔ t : ℤ) : ℝ)
476 have hnonneg : ∀ t : Fin d, 0 ≤ fD t := fun _ => Cost.Jlog_nonneg _
477 have hi : fD k = Cost.Jlog (1 : ℝ) := by simpa [fD, hk]
478 have hj : fD j = Cost.Jlog (1 : ℝ) := by simpa [fD, hj1]
479 -- show debitSum ≥ fD k + fD j
480 have hsplit :=
481 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fD) (a := k) (by simp))
482 have hjmem : j ∈ (Finset.univ.erase k : Finset (Fin d)) := by simp [hjk]
483 have hj_le_rest :
484 fD j ≤ Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
485 exact Finset.single_le_sum (by
486 intro t ht; exact hnonneg t) hjmem
487 have hdebit_ge :
488 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ∑ t : Fin d, fD t := by
489 -- rewrite sum and use `hj_le_rest`
490 calc
491 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ)
492 = fD k + fD j := by simp [hi, hj]
493 _ ≤ fD k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
494 linarith
495 _ = ∑ t : Fin d, fD t := by simpa using hsplit.symm
496 -- total cost ≥ debitSum
497 have hcredit_nonneg : 0 ≤ ∑ t : Fin d, Cost.Jlog ((cΔ t : ℤ) : ℝ) :=
498 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
499 have hcost_ge : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
500 dsimp [ledgerJlogCost, dΔ, cΔ]
501 exact le_trans (le_trans hdebit_ge (le_add_of_nonneg_right hcredit_nonneg)) (le_rfl)
502 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
503 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
504 exact lt_of_lt_of_le this hcost_ge
505 exact (not_lt_of_ge hle) this
506 cases hd01 j with
507 | inl hz => exact hz
508 | inr h1 => exact (hn1 h1).elim
509 -- now show L' = post L k debit
510 refine ⟨k, Side.debit, ?_⟩
511 cases L with
512 | mk debit credit =>
513 cases L' with
514 | mk debit' credit' =>
515 have hdebit' : debit' = fun i => if i = k then debit i + 1 else debit i := by
516 funext i
517 by_cases hik : i = k
518 · subst hik
519 have hdiff : debit' i - debit i = 1 := by simpa [dΔ] using hk
520 have : debit' i = debit i + 1 := by linarith
521 simpa using this
522 · have : debit' i - debit i = 0 := by
523 have := hdAll i hik
524 simpa [dΔ] using this
525 simp [hik]
526 linarith
527 have hcredit' : credit' = credit := by
528 funext i
529 have : credit' i - credit i = 0 := by simpa [cΔ] using hcAll0 i
530 linarith
531 subst hdebit' hcredit'
532 simp [post]
533 ext i <;> by_cases h : i = k <;> simp [h]
534 | inr hc =>
535 rcases hc with ⟨k, hk⟩
536 have : ¬ (∃ j : Fin d, dΔ j = 1) := by
537 intro hd
538 exact not_two_ones ⟨hd, ⟨k, hk⟩⟩
539 -- symmetric to debit case: build post on credit
540 have hdAll0 : ∀ j : Fin d, dΔ j = 0 := by
541 intro j
542 have hn1 : ¬ dΔ j = 1 := by
543 intro hj
544 exact this ⟨j, hj⟩
545 cases hd01 j with
546 | inl hz => exact hz
547 | inr h1 => exact (hn1 h1).elim
548 have hcAll : ∀ j : Fin d, j ≠ k → cΔ j = 0 := by
549 intro j hjk
550 have hn1 : ¬ cΔ j = 1 := by
551 intro hj1
552 -- two credit ones would force cost > Jlog 1 (same argument as in debit case)
553 let fC : Fin d → ℝ := fun t => Cost.Jlog ((cΔ t : ℤ) : ℝ)
554 have hnonneg : ∀ t : Fin d, 0 ≤ fC t := fun _ => Cost.Jlog_nonneg _
555 have hi : fC k = Cost.Jlog (1 : ℝ) := by simpa [fC, hk]
556 have hj : fC j = Cost.Jlog (1 : ℝ) := by simpa [fC, hj1]
557 have hsplit :=
558 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fC) (a := k) (by simp))
559 have hjmem : j ∈ (Finset.univ.erase k : Finset (Fin d)) := by simp [hjk]
560 have hj_le_rest :
561 fC j ≤ Finset.sum (Finset.univ.erase k : Finset (Fin d)) fC := by
562 exact Finset.single_le_sum (by
563 intro t ht; exact hnonneg t) hjmem
564 have hcredit_ge :
565 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ∑ t : Fin d, fC t := by
566 calc
567 Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ)
568 = fC k + fC j := by simp [hi, hj]
569 _ ≤ fC k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) fC := by
570 linarith
571 _ = ∑ t : Fin d, fC t := by simpa using hsplit.symm
572 have hdebit_nonneg : 0 ≤ ∑ t : Fin d, Cost.Jlog ((dΔ t : ℤ) : ℝ) :=
573 Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
574 have hcost_ge : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
575 dsimp [ledgerJlogCost, dΔ, cΔ]
576 exact le_trans (le_trans hcredit_ge (le_add_of_nonneg_left hdebit_nonneg)) (le_rfl)
577 have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
578 have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
579 exact lt_of_lt_of_le this hcost_ge
580 exact (not_lt_of_ge hle) this
581 cases hc01 j with
582 | inl hz => exact hz
583 | inr h1 => exact (hn1 h1).elim
584 refine ⟨k, Side.credit, ?_⟩
585 cases L with
586 | mk debit credit =>
587 cases L' with
588 | mk debit' credit' =>
589 have hcredit' : credit' = fun i => if i = k then credit i + 1 else credit i := by
590 funext i
591 by_cases hik : i = k
592 · subst hik
593 have hdiff : credit' i - credit i = 1 := by simpa [cΔ] using hk
594 have : credit' i = credit i + 1 := by linarith
595 simpa using this
596 · have : credit' i - credit i = 0 := by
597 have := hcAll i hik
598 simpa [cΔ] using this
599 simp [hik]
600 linarith
601 have hdebit' : debit' = debit := by
602 funext i
603 have : debit' i - debit i = 0 := by simpa [dΔ] using hdAll0 i
604 linarith
605 subst hcredit' hdebit'
606 simp [post]
607 ext i <;> by_cases h : i = k <;> simp [h]
608
609/-! ### Zero-cost characterization -/
610
611theorem ledgerL1Cost_eq_zero_iff {d : Nat} (L L' : LedgerState d) :
612 ledgerL1Cost (d := d) L L' = 0 ↔ L' = L := by
613 classical
614 cases L with
615 | mk debit credit =>
616 cases L' with
617 | mk debit' credit' =>
618 constructor
619 · intro h0
620 -- split into debit/credit sums
621 let dSum : Nat := ∑ i : Fin d, Int.natAbs (debit' i - debit i)
622 let cSum : Nat := ∑ i : Fin d, Int.natAbs (credit' i - credit i)
623 have hsplit : dSum + cSum = 0 := by
624 simpa [ledgerL1Cost, dSum, cSum] using h0
625 have hd0 : dSum = 0 ∧ cSum = 0 := Nat.add_eq_zero_iff.mp hsplit
626 have hdebit0 :
627 ∀ i : Fin d, Int.natAbs (debit' i - debit i) = 0 := by
628 have h' :
629 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (debit' i - debit i)) = 0 := by
630 simpa [dSum] using hd0.1
631 have hall :=
632 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
633 (f := fun i => Int.natAbs (debit' i - debit i))
634 (fun _ _ => Nat.zero_le _)).1 h'
635 intro i
636 exact hall i (by simp)
637 have hcredit0 :
638 ∀ i : Fin d, Int.natAbs (credit' i - credit i) = 0 := by
639 have h' :
640 Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (credit' i - credit i)) = 0 := by
641 simpa [cSum] using hd0.2
642 have hall :=
643 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
644 (f := fun i => Int.natAbs (credit' i - credit i))
645 (fun _ _ => Nat.zero_le _)).1 h'
646 intro i
647 exact hall i (by simp)
648 have hdebitEq : debit' = debit := by
649 funext i
650 have hz : (debit' i - debit i) = 0 := Int.natAbs_eq_zero.mp (hdebit0 i)
651 linarith
652 have hcreditEq : credit' = credit := by
653 funext i
654 have hz : (credit' i - credit i) = 0 := Int.natAbs_eq_zero.mp (hcredit0 i)
655 linarith
656 subst hdebitEq hcreditEq
657 rfl
658 · intro hEq
659 cases hEq
660 simp [ledgerL1Cost]
661
662/-! ### Posting steps satisfy `LegalAtomicTick` (and conversely, by `legalAtomicTick_implies_PostingStep`) -/
663
664private lemma post_monotone {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
665 MonotoneLedger (d := d) L (post L k side) := by
666 classical
667 cases side with
668 | debit =>
669 refine ⟨?_, ?_⟩
670 · intro i
671 by_cases hik : i = k
672 · subst hik
673 simp [post]
674 · simp [post, hik]
675 · intro i
676 simp [post]
677 | credit =>
678 refine ⟨?_, ?_⟩
679 · intro i
680 simp [post]
681 · intro i
682 by_cases hik : i = k
683 · subst hik
684 simp [post]
685 · simp [post, hik]
686
687private lemma ledgerL1Cost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
688 ledgerL1Cost (d := d) L (post L k side) = 1 := by
689 classical
690 cases side with
691 | debit =>
692 -- debit changes by +1 at k; credit unchanged
693 have hdebit :
694 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).debit i - L.debit i)) = 1 := by
695 -- isolate `k` and show everything else is 0
696 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.debit).debit i - L.debit i)
697 have hsplit :=
698 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
699 have fk : f k = 1 := by
700 simp [f, post]
701 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
702 refine Finset.sum_eq_zero ?_
703 intro i hi
704 have hik : i ≠ k := by
705 simpa [Finset.mem_erase] using hi
706 simp [f, post, hik]
707 -- rewrite `∑ univ` using `hsplit.symm`
708 simpa [f] using (by
709 calc
710 (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
711 simpa using hsplit.symm
712 _ = 1 := by simp [fk, hErase])
713 have hcredit :
714 (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i - L.credit i)) = 0 := by
715 -- credit is unchanged everywhere
716 refine Finset.sum_eq_zero ?_
717 intro i _
718 simp [post]
719 -- assemble
720 simp [ledgerL1Cost, hdebit, hcredit]
721 | credit =>
722 -- credit changes by +1 at k; debit unchanged
723 have hdebit :
724 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).debit i - L.debit i)) = 0 := by
725 refine Finset.sum_eq_zero ?_
726 intro i _
727 simp [post]
728 have hcredit :
729 (∑ i : Fin d, Int.natAbs ((post L k Side.credit).credit i - L.credit i)) = 1 := by
730 let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.credit).credit i - L.credit i)
731 have hsplit :=
732 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
733 have fk : f k = 1 := by
734 simp [f, post]
735 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
736 refine Finset.sum_eq_zero ?_
737 intro i hi
738 have hik : i ≠ k := by
739 simpa [Finset.mem_erase] using hi
740 simp [f, post, hik]
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 simp [ledgerL1Cost, hdebit, hcredit]
747
748theorem legalAtomicTick_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
749 LegalAtomicTick (d := d) L (post L k side) := by
750 refine ⟨post_monotone (d := d) L k side, ledgerL1Cost_post (d := d) L k side⟩
751
752theorem postingStep_implies_legalAtomicTick {d : Nat} {L L' : LedgerState d}
753 (h : PostingStep (d := d) L L') : LegalAtomicTick (d := d) L L' := by
754 rcases h with ⟨k, side, rfl⟩
755 exact legalAtomicTick_of_post (d := d) L k side
756
757private lemma int_natAbs_eq_one_of_nonneg {z : ℤ} (hz : Int.natAbs z = 1) (hznn : 0 ≤ z) :
758 z = 1 := by
759 cases z with
760 | ofNat n =>
761 -- natAbs (ofNat n) = n
762 have : n = 1 := by simpa using hz
763 simpa [this]
764 | negSucc n =>
765 -- negative contradiction
766 have : ¬ (0 ≤ Int.negSucc n) := by
767 -- `negSucc n = -(n+1) < 0`
768 have : Int.negSucc n < 0 := by
769 simpa using (Int.negSucc_lt_zero n)
770 exact not_le_of_gt this
771 exact (this hznn).elim
772
773private lemma int_eq_of_natAbs_eq_zero {z : ℤ} (hz : Int.natAbs z = 0) : z = 0 := by
774 exact (Int.natAbs_eq_zero.mp hz)
775
776private lemma exists_unique_of_sum_univ_eq_one {d : Nat} (f : Fin d → Nat)
777 (hs : (∑ i : Fin d, f i) = 1) :
778 ∃ k : Fin d, f k = 1 ∧ ∀ i : Fin d, i ≠ k → f i = 0 := by
779 classical
780 have hs_ne0 : (∑ i : Fin d, f i) ≠ 0 := by
781 simpa [hs] using Nat.one_ne_zero
782 obtain ⟨k, _hkMem, hkne0⟩ := Finset.exists_ne_zero_of_sum_ne_zero (s := (Finset.univ : Finset (Fin d)))
783 (f := fun i => f i) hs_ne0
784 have hdecomp : f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 1 := by
785 -- `f k + sum (erase k) = sum univ`
786 have := (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fun i => f i) (a := k) (by simp))
787 simpa [hs] using this
788 have hk_cases := Nat.add_eq_one_iff.mp hdecomp
789 have hk1 : f k = 1 ∧ Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
790 cases hk_cases with
791 | inl h0 =>
792 -- f k = 0 contradicts hkne0
793 exfalso
794 exact hkne0 h0.1
795 | inr h1 =>
796 exact h1
797 refine ⟨k, hk1.1, ?_⟩
798 intro i hik
799 have hi' : i ∈ (Finset.univ.erase k : Finset (Fin d)) := by
800 simp [Finset.mem_erase, hik]
801 -- sum=0 on erase ⇒ every term on erase is 0
802 have hall0 :
803 ∀ j : Fin d, j ∈ (Finset.univ.erase k : Finset (Fin d)) → f j = 0 := by
804 have :=
805 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ.erase k : Finset (Fin d)))
806 (f := fun j => f j) (fun _ _ => Nat.zero_le _)).1 hk1.2
807 simpa using this
808 exact hall0 i hi'
809
810theorem legalAtomicTick_implies_PostingStep {d : Nat} {L L' : LedgerState d}
811 (h : LegalAtomicTick (d := d) L L') : PostingStep (d := d) L L' := by
812 classical
813 rcases h with ⟨hmono, hcost⟩
814 rcases hmono with ⟨hmonoD, hmonoC⟩
815 -- split the total cost into debit-cost and credit-cost
816 let dCost : Nat := ∑ i : Fin d, Int.natAbs (L'.debit i - L.debit i)
817 let cCost : Nat := ∑ i : Fin d, Int.natAbs (L'.credit i - L.credit i)
818 have hsplit : dCost + cCost = 1 := by
819 simpa [ledgerL1Cost, dCost, cCost] using hcost
820 have hcases := Nat.add_eq_one_iff.mp hsplit
821 cases hcases with
822 | inl hc =>
823 -- dCost = 0, cCost = 1 → credit posting
824 have hd0 : dCost = 0 := hc.1
825 have hc1 : cCost = 1 := hc.2
826 -- choose the unique changed credit coordinate
827 have ⟨k, hk1, hkrest⟩ :=
828 exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.credit i - L.credit i)) hc1
829 -- debit diffs all 0
830 have hdAll :
831 ∀ i : Fin d, Int.natAbs (L'.debit i - L.debit i) = 0 := by
832 have hall0 :
833 ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.debit i - L.debit i) = 0 := by
834 have :=
835 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
836 (f := fun i => Int.natAbs (L'.debit i - L.debit i))
837 (fun _ _ => Nat.zero_le _)).1 hd0
838 simpa [dCost] using this
839 intro i; exact hall0 i (by simp)
840 -- build PostingStep = post at k on credit side
841 refine ⟨k, Side.credit, ?_⟩
842 -- prove L' = post L k credit by field ext (no `[ext]` lemma registered)
843 cases L with
844 | mk debit credit =>
845 cases L' with
846 | mk debit' credit' =>
847 -- show the debit field is unchanged
848 have hdebit' : debit' = debit := by
849 funext i
850 have hz := int_eq_of_natAbs_eq_zero (hdAll i)
851 have hz' : (debit' i - debit i) = 0 := by simpa using hz
852 linarith
853 -- show the credit field matches the `post` update
854 have hcredit' :
855 credit' = (fun i => if i = k then credit i + 1 else credit i) := by
856 funext i
857 by_cases hik : i = k
858 · subst hik
859 -- goal reduces to `credit' i = credit i + 1`
860 simp
861 have hzabs : Int.natAbs (credit' i - credit i) = 1 := hk1
862 have hnn : 0 ≤ (credit' i - credit i) := by
863 have : credit i ≤ credit' i := hmonoC i
864 linarith
865 have hz : (credit' i - credit i) = 1 :=
866 int_natAbs_eq_one_of_nonneg (z := (credit' i - credit i)) hzabs hnn
867 linarith
868 · -- goal reduces to `credit' i = credit i`
869 have hzabs : Int.natAbs (credit' i - credit i) = 0 := hkrest i hik
870 have hz : (credit' i - credit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
871 simp [hik]
872 linarith
873 -- finish
874 subst hdebit' hcredit'
875 simp [post]
876 ext i <;> by_cases h : i = k <;> simp [h]
877 | inr hc =>
878 -- dCost = 1, cCost = 0 → debit posting
879 have hd1 : dCost = 1 := hc.1
880 have hc0 : cCost = 0 := hc.2
881 have ⟨k, hk1, hkrest⟩ :=
882 exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.debit i - L.debit i)) hd1
883 have hcAll :
884 ∀ i : Fin d, Int.natAbs (L'.credit i - L.credit i) = 0 := by
885 have hall0 :
886 ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.credit i - L.credit i) = 0 := by
887 have :=
888 (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
889 (f := fun i => Int.natAbs (L'.credit i - L.credit i))
890 (fun _ _ => Nat.zero_le _)).1 hc0
891 simpa [cCost] using this
892 intro i; exact hall0 i (by simp)
893 refine ⟨k, Side.debit, ?_⟩
894 cases L with
895 | mk debit credit =>
896 cases L' with
897 | mk debit' credit' =>
898 have hcredit' : credit' = credit := by
899 funext i
900 have hz := int_eq_of_natAbs_eq_zero (hcAll i)
901 have hz' : (credit' i - credit i) = 0 := by simpa using hz
902 linarith
903 have hdebit' :
904 debit' = (fun i => if i = k then debit i + 1 else debit i) := by
905 funext i
906 by_cases hik : i = k
907 · subst hik
908 simp
909 have hzabs : Int.natAbs (debit' i - debit i) = 1 := hk1
910 have hnn : 0 ≤ (debit' i - debit i) := by
911 have : debit i ≤ debit' i := hmonoD i
912 linarith
913 have hz : (debit' i - debit i) = 1 :=
914 int_natAbs_eq_one_of_nonneg (z := (debit' i - debit i)) hzabs hnn
915 linarith
916 · have hzabs : Int.natAbs (debit' i - debit i) = 0 := hkrest i hik
917 have hz : (debit' i - debit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
918 simp [hik]
919 linarith
920 subst hcredit' hdebit'
921 simp [post]
922 ext i <;> by_cases h : i = k <;> simp [h]
923
924theorem postingStep_iff_legalAtomicTick {d : Nat} {L L' : LedgerState d} :
925 PostingStep (d := d) L L' ↔ LegalAtomicTick (d := d) L L' :=
926 ⟨postingStep_implies_legalAtomicTick (d := d), legalAtomicTick_implies_PostingStep (d := d)⟩
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
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
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) -/
1000
1001/-- Choose the unique posted account at tick `t` from an RS `AtomicTick` instance. -/
1002noncomputable def accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) : Fin d :=
1003 Classical.choose (ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t))
1004
1005lemma postedAt_accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) :
1006 AtomicTick.postedAt (M := AccountRS d) t (accountAt (d := d) t) := by
1007 have hex : ∃ u : Fin d, AtomicTick.postedAt (M := AccountRS d) t u :=
1008 ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t)
1009 simpa [accountAt] using (Classical.choose_spec hex)
1010
1011/-- An RS-atomic tick step, parameterized by an explicit debit/credit side schedule. -/
1012noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1013 LedgerState d :=
1014 post L (accountAt (d := d) t) (sideAt t)
1015
1016lemma stepAt_isPostingStep {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1017 PostingStep (d := d) L (stepAt (d := d) sideAt t L) := by
1018 refine ⟨accountAt (d := d) t, sideAt t, rfl⟩
1019
1020theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1021 OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=
1022 postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1023
1024/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/
1025
1026/-- A per-tick posting instruction: (account index, side). -/
1027abbrev PostInstr (d : Nat) : Type := Fin d × Side
1028
1029/-- Run a ledger forward under a per-tick posting schedule. -/
1030noncomputable def run {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) : Nat → LedgerState d
1031| 0 => L0
1032| (t + 1) =>
1033 let prev := run L0 sched t
1034 post prev (sched t).1 (sched t).2
1035
1036theorem run_step_oneBitDiff {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) (t : Nat) :
1037 OneBitDiff (parity d (run L0 sched t)) (parity d (run L0 sched (t + 1))) := by
1038 -- unfold one step of `run` and apply the single-post theorem
1039 simp [run, parity_oneBitDiff_of_post, parity]
1040
1041end LedgerPostingAdjacency
1042end IndisputableMonolith
1043