IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3import IndisputableMonolith.NumberTheory.Primes.Squarefree
   4
   5/-!
   6# Arithmetic functions (Möbius footholds)
   7
   8This file provides small wrappers around Mathlib's arithmetic function library, starting with the
   9Möbius function `μ` (spelled `ArithmeticFunction.moebius` in code).
  10
  11We keep the statements lightweight here; deeper Dirichlet algebra and inversion can be layered on
  12once the basic interfaces stabilize.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace NumberTheory
  17namespace Primes
  18
  19open scoped ArithmeticFunction.Moebius
  20open scoped ArithmeticFunction.Omega
  21open scoped ArithmeticFunction.omega
  22
  23/-- The Möbius function (as an arithmetic function `ℕ → ℤ`). -/
  24abbrev mobius : ArithmeticFunction ℤ := ArithmeticFunction.moebius
  25
  26@[simp] theorem mobius_def : mobius = ArithmeticFunction.moebius := rfl
  27
  28/-- Möbius at a prime: `μ(p) = -1`. -/
  29theorem mobius_prime {p : ℕ} (hp : Prime p) : (mobius p) = -1 := by
  30  -- Mathlib lemma is `ArithmeticFunction.moebius_apply_prime` with `Nat.Prime`.
  31  have hp' : Nat.Prime p := (prime_iff p).1 hp
  32  simpa [mobius] using (ArithmeticFunction.moebius_apply_prime hp')
  33
  34/-- Möbius at a prime square: `μ(p^2) = 0`. -/
  35theorem mobius_prime_sq {p : ℕ} (hp : Prime p) : (mobius (p ^ 2)) = 0 := by
  36  have hp' : Nat.Prime p := (prime_iff p).1 hp
  37  -- Use the prime-power formula with `k = 2`: `μ(p^2) = if 2 = 1 then -1 else 0 = 0`.
  38  simpa [mobius] using
  39    (ArithmeticFunction.moebius_apply_prime_pow (p := p) (k := 2) hp' (by decide : (2 : ℕ) ≠ 0))
  40
  41/-- If `n` is not squarefree, then `μ n = 0`. -/
  42theorem mobius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) : mobius n = 0 := by
  43  simpa [mobius] using (ArithmeticFunction.moebius_eq_zero_of_not_squarefree (n := n) h)
  44
  45/-- `μ n ≠ 0` iff `n` is squarefree. -/
  46theorem mobius_ne_zero_iff_squarefree {n : ℕ} : mobius n ≠ 0 ↔ Squarefree n := by
  47  simpa [mobius] using (ArithmeticFunction.moebius_ne_zero_iff_squarefree (n := n))
  48
  49/-- `μ n = 0` iff `n` is not squarefree. -/
  50theorem mobius_eq_zero_iff_not_squarefree {n : ℕ} : mobius n = 0 ↔ ¬Squarefree n := by
  51  -- Negate `μ n ≠ 0 ↔ Squarefree n`.
  52  simpa [not_ne_iff] using (not_congr (mobius_ne_zero_iff_squarefree (n := n)))
  53
  54/-- If `n` is squarefree then `μ n = (-1)^(cardFactors n)`. -/
  55theorem mobius_apply_of_squarefree {n : ℕ} (hn : Squarefree n) :
  56    mobius n = (-1) ^ ArithmeticFunction.cardFactors n := by
  57  simpa [mobius] using (ArithmeticFunction.moebius_apply_of_squarefree (n := n) hn)
  58
  59/-- A useful bridge: for `n ≠ 0`, `μ n ≠ 0` iff all prime exponents are ≤ 1. -/
  60theorem mobius_ne_zero_iff_vp_le_one {n : ℕ} (hn : n ≠ 0) :
  61    mobius n ≠ 0 ↔ ∀ p : ℕ, vp p n ≤ 1 := by
  62  constructor
  63  · intro hμ
  64    have hsq : Squarefree n := (mobius_ne_zero_iff_squarefree (n := n)).1 hμ
  65    exact (squarefree_iff_vp_le_one (n := n) hn).1 hsq
  66  · intro hvp
  67    have hsq : Squarefree n := (squarefree_iff_vp_le_one (n := n) hn).2 hvp
  68    exact (mobius_ne_zero_iff_squarefree (n := n)).2 hsq
  69
  70/-! ### Additional arithmetic function wrappers -/
  71
  72/-- Number of prime factors (with multiplicity) — Ω(n). -/
  73abbrev bigOmega : ArithmeticFunction ℕ := ArithmeticFunction.cardFactors
  74
  75@[simp] theorem bigOmega_def : bigOmega = ArithmeticFunction.cardFactors := rfl
  76
  77/-- `Ω(n) = n.primeFactorsList.length`. -/
  78theorem bigOmega_apply {n : ℕ} : bigOmega n = n.primeFactorsList.length := by
  79  simp only [bigOmega, ArithmeticFunction.cardFactors_apply]
  80
  81/-- Number of distinct prime divisors — ω(n). -/
  82abbrev omega : ArithmeticFunction ℕ := ArithmeticFunction.cardDistinctFactors
  83
  84@[simp] theorem omega_def : omega = ArithmeticFunction.cardDistinctFactors := rfl
  85
  86/-- `ω(n) = n.primeFactorsList.dedup.length`. -/
  87theorem omega_apply {n : ℕ} : omega n = n.primeFactorsList.dedup.length := by
  88  simp only [omega, ArithmeticFunction.cardDistinctFactors_apply]
  89
  90/-- For squarefree `n ≠ 0`, `Ω(n) = ω(n)` (all exponents are 1). -/
  91theorem bigOmega_eq_omega_of_squarefree {n : ℕ} (hn : n ≠ 0) (hsq : Squarefree n) :
  92    bigOmega n = omega n := by
  93  simp only [bigOmega, omega]
  94  exact ((ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree hn).mpr hsq).symm
  95
  96/-! ### Euler's totient function φ (via `Nat.totient`) -/
  97
  98/-- Euler's totient function wrapper. -/
  99def totient (n : ℕ) : ℕ := Nat.totient n
 100
 101@[simp] theorem totient_apply {n : ℕ} : totient n = Nat.totient n := rfl
 102
 103/-- φ(1) = 1. -/
 104theorem totient_one : totient 1 = 1 := by
 105  simp [totient, Nat.totient_one]
 106
 107/-- φ(p) = p - 1 for prime p. -/
 108theorem totient_prime {p : ℕ} (hp : Prime p) : totient p = p - 1 := by
 109  have hp' : Nat.Prime p := (prime_iff p).1 hp
 110  simp [totient, Nat.totient_prime hp']
 111
 112/-- φ(p^k) = p^(k-1) * (p - 1) for prime p and k ≥ 1. -/
 113theorem totient_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) :
 114    totient (p ^ k) = p ^ (k - 1) * (p - 1) := by
 115  have hp' : Nat.Prime p := (prime_iff p).1 hp
 116  simp [totient, Nat.totient_prime_pow hp' hk]
 117
 118/-- φ is multiplicative for coprime arguments. -/
 119theorem totient_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 120    totient (m * n) = totient m * totient n := by
 121  simp [totient, Nat.totient_mul h]
 122
 123/-- The sum of φ(d) over divisors of n equals n: ∑_{d|n} φ(d) = n. -/
 124theorem totient_divisor_sum {n : ℕ} : ∑ d ∈ n.divisors, totient d = n := by
 125  simp only [totient]
 126  exact Nat.sum_totient n
 127
 128/-- φ(n) ≤ n for all n. -/
 129theorem totient_le (n : ℕ) : totient n ≤ n := by
 130  simp only [totient]
 131  exact Nat.totient_le n
 132
 133/-- φ(n) > 0 iff n > 0. -/
 134theorem totient_pos_iff {n : ℕ} : 0 < totient n ↔ 0 < n := by
 135  simp only [totient]
 136  exact Nat.totient_pos
 137
 138/-! ### Von Mangoldt function Λ -/
 139
 140/-- The von Mangoldt function (as an arithmetic function `ℕ → ℝ`). -/
 141noncomputable abbrev vonMangoldt : ArithmeticFunction ℝ := ArithmeticFunction.vonMangoldt
 142
 143@[simp] theorem vonMangoldt_def : vonMangoldt = ArithmeticFunction.vonMangoldt := rfl
 144
 145/-- Λ(p) = log(p) for prime p. -/
 146theorem vonMangoldt_prime {p : ℕ} (hp : Prime p) : vonMangoldt p = Real.log p := by
 147  have hp' : Nat.Prime p := (prime_iff p).1 hp
 148  simp [vonMangoldt, ArithmeticFunction.vonMangoldt_apply_prime hp']
 149
 150/-- Λ(n) = 0 unless n is a prime power. -/
 151theorem vonMangoldt_eq_zero_of_not_prime_pow {n : ℕ} (h : ¬ IsPrimePow n) :
 152    vonMangoldt n = 0 := by
 153  simp [vonMangoldt, ArithmeticFunction.vonMangoldt_eq_zero_iff.mpr h]
 154
 155/-- Λ(p^k) = log(p) for prime p and k ≥ 1. -/
 156theorem vonMangoldt_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) :
 157    vonMangoldt (p ^ k) = Real.log p := by
 158  have hp' : Nat.Prime p := (prime_iff p).1 hp
 159  have hk' : k ≠ 0 := Nat.pos_iff_ne_zero.mp hk
 160  rw [vonMangoldt, ArithmeticFunction.vonMangoldt_apply_pow hk']
 161  exact vonMangoldt_prime hp
 162
 163/-! ### Multiplicativity -/
 164
 165/-- The Möbius function is multiplicative. -/
 166theorem mobius_isMultiplicative : ArithmeticFunction.IsMultiplicative mobius := by
 167  simp only [mobius]
 168  exact ArithmeticFunction.isMultiplicative_moebius
 169
 170/-! ### Sigma function (sum of divisors) -/
 171
 172/-- The sum-of-divisors function σ_k. -/
 173abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k
 174
 175@[simp] theorem sigma_def (k : ℕ) : sigma k = ArithmeticFunction.sigma k := rfl
 176
 177/-- σ_k(n) = ∑ d ∣ n, d^k. -/
 178theorem sigma_apply {k n : ℕ} : sigma k n = ∑ d ∈ n.divisors, d ^ k := by
 179  simp only [sigma, ArithmeticFunction.sigma_apply]
 180
 181/-- σ_0(n) = number of divisors of n. -/
 182theorem sigma_zero_apply {n : ℕ} : sigma 0 n = n.divisors.card := by
 183  simp only [sigma, ArithmeticFunction.sigma_zero_apply]
 184
 185/-- σ_1(n) = sum of divisors of n. -/
 186theorem sigma_one_apply {n : ℕ} : sigma 1 n = ∑ d ∈ n.divisors, d := by
 187  simp only [sigma, ArithmeticFunction.sigma_one_apply]
 188
 189/-- σ_k is multiplicative. -/
 190theorem sigma_isMultiplicative (k : ℕ) : ArithmeticFunction.IsMultiplicative (sigma k) := by
 191  simp only [sigma]
 192  exact ArithmeticFunction.isMultiplicative_sigma
 193
 194/-- σ_0(p) = 2 for prime p. -/
 195theorem sigma_zero_prime {p : ℕ} (hp : Prime p) : sigma 0 p = 2 := by
 196  have hp' : Nat.Prime p := (prime_iff p).1 hp
 197  simp only [sigma_zero_apply, hp'.divisors]
 198  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 199  rw [Finset.card_insert_of_notMem (by simp [h_ne]), Finset.card_singleton]
 200
 201/-- σ_1(p) = p + 1 for prime p. -/
 202theorem sigma_one_prime {p : ℕ} (hp : Prime p) : sigma 1 p = p + 1 := by
 203  have hp' : Nat.Prime p := (prime_iff p).1 hp
 204  simp only [sigma_one_apply, hp'.divisors]
 205  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 206  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, add_comm]
 207
 208/-- σ_k(p) = 1 + p^k for prime p. -/
 209theorem sigma_prime {k : ℕ} {p : ℕ} (hp : Prime p) : sigma k p = 1 + p ^ k := by
 210  have hp' : Nat.Prime p := (prime_iff p).1 hp
 211  simp only [sigma_apply, hp'.divisors]
 212  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 213  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, one_pow, add_comm]
 214
 215/-! ### Zeta function (constant 1) and Dirichlet convolution -/
 216
 217/-- The arithmetic zeta function ζ (constant 1 on positive integers). -/
 218abbrev zeta : ArithmeticFunction ℕ := ArithmeticFunction.zeta
 219
 220@[simp] theorem zeta_def : zeta = ArithmeticFunction.zeta := rfl
 221
 222/-- ζ(n) = 1 for n ≥ 1. -/
 223theorem zeta_apply {n : ℕ} (hn : n ≠ 0) : zeta n = 1 := by
 224  simp only [zeta, ArithmeticFunction.zeta_apply, hn, ↓reduceIte]
 225
 226/-- ζ(0) = 0. -/
 227theorem zeta_zero : zeta 0 = 0 := by
 228  simp only [zeta, ArithmeticFunction.zeta_apply, ↓reduceIte]
 229
 230/-- ζ is multiplicative. -/
 231theorem zeta_isMultiplicative : ArithmeticFunction.IsMultiplicative zeta := by
 232  simp only [zeta]
 233  exact ArithmeticFunction.isMultiplicative_zeta
 234
 235/-! ### Möbius inversion fundamentals -/
 236
 237/-- The key identity: μ * ζ = ε (the Dirichlet identity).
 238This is the foundation of Möbius inversion. -/
 239theorem moebius_mul_zeta : (mobius : ArithmeticFunction ℤ) * ↑zeta = 1 := by
 240  simp only [mobius, zeta]
 241  exact ArithmeticFunction.moebius_mul_coe_zeta
 242
 243/-- Symmetric form: ζ * μ = ε. -/
 244theorem zeta_mul_moebius : (↑zeta : ArithmeticFunction ℤ) * mobius = 1 := by
 245  simp only [mobius, zeta]
 246  exact ArithmeticFunction.coe_zeta_mul_moebius
 247
 248/-- For the identity (Dirichlet unit), we wrap ε = δ_1. -/
 249abbrev dirichletOne : ArithmeticFunction ℤ := 1
 250
 251@[simp] theorem dirichletOne_def : dirichletOne = 1 := rfl
 252
 253/-- ε(1) = 1. -/
 254theorem dirichletOne_one : dirichletOne 1 = 1 := by
 255  simp [dirichletOne]
 256
 257/-- ε(n) = 0 for n > 1. -/
 258theorem dirichletOne_ne_one {n : ℕ} (hn : n ≠ 1) : dirichletOne n = 0 := by
 259  simp [dirichletOne, hn]
 260
 261/-! ### Additional multiplicativity lemmas -/
 262
 263/-- ω (number of distinct prime factors) is additive on coprimes: ω(mn) = ω(m) + ω(n). -/
 264theorem omega_mul_of_coprime {m n : ℕ} (_hm : m ≠ 0) (_hn : n ≠ 0) (h : Nat.Coprime m n) :
 265    omega (m * n) = omega m + omega n := by
 266  simp only [omega]
 267  exact ArithmeticFunction.cardDistinctFactors_mul h
 268
 269/-- Ω (number of prime factors with multiplicity) is additive: Ω(mn) = Ω(m) + Ω(n). -/
 270theorem bigOmega_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 271    bigOmega (m * n) = bigOmega m + bigOmega n := by
 272  simp only [bigOmega]
 273  exact ArithmeticFunction.cardFactors_mul hm hn
 274
 275/-- Ω is completely additive on powers: Ω(n^k) = k * Ω(n). -/
 276theorem bigOmega_pow {n k : ℕ} : bigOmega (n ^ k) = k * bigOmega n := by
 277  simp only [bigOmega]
 278  exact ArithmeticFunction.cardFactors_pow
 279
 280/-! ### Liouville function λ -/
 281
 282/-- The Liouville function λ(n) = (-1)^Ω(n).
 283Note: We define this directly since Mathlib may not have a prebuilt version. -/
 284def liouville (n : ℕ) : ℤ :=
 285  if n = 0 then 0 else (-1) ^ bigOmega n
 286
 287/-- λ(0) = 0 (by convention). -/
 288@[simp] theorem liouville_zero : liouville 0 = 0 := by
 289  simp [liouville]
 290
 291/-- λ(n) = (-1)^Ω(n) for n ≠ 0. -/
 292theorem liouville_eq {n : ℕ} (hn : n ≠ 0) : liouville n = (-1) ^ bigOmega n := by
 293  simp [liouville, hn]
 294
 295/-- λ(1) = 1. -/
 296theorem liouville_one : liouville 1 = 1 := by
 297  simp [liouville, bigOmega_apply]
 298
 299/-- λ(p) = -1 for prime p. -/
 300theorem liouville_prime {p : ℕ} (hp : Prime p) : liouville p = -1 := by
 301  have hp' : Nat.Prime p := (prime_iff p).1 hp
 302  have hp_ne : p ≠ 0 := hp'.ne_zero
 303  simp only [liouville, hp_ne, ↓reduceIte, bigOmega]
 304  -- Ω(p) = 1 for prime p
 305  have hOmega : ArithmeticFunction.cardFactors p = 1 := ArithmeticFunction.cardFactors_apply_prime hp'
 306  rw [hOmega]
 307  norm_num
 308
 309/-- λ(p^k) = (-1)^k for prime p. -/
 310theorem liouville_prime_pow {p k : ℕ} (hp : Prime p) :
 311    liouville (p ^ k) = (-1) ^ k := by
 312  have hp' : Nat.Prime p := (prime_iff p).1 hp
 313  cases k with
 314  | zero => simp [liouville_one]
 315  | succ k =>
 316    have hpk : p ^ (k + 1) ≠ 0 := pow_ne_zero (k + 1) hp'.ne_zero
 317    simp only [liouville, hpk, ↓reduceIte, bigOmega]
 318    -- Ω(p^k) = k for prime p
 319    have hOmega : ArithmeticFunction.cardFactors (p ^ (k + 1)) = k + 1 :=
 320      ArithmeticFunction.cardFactors_apply_prime_pow hp'
 321    rw [hOmega]
 322
 323/-- λ(mn) = λ(m) * λ(n) for nonzero m, n (complete multiplicativity). -/
 324theorem liouville_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 325    liouville (m * n) = liouville m * liouville n := by
 326  have hmn : m * n ≠ 0 := mul_ne_zero hm hn
 327  simp only [liouville, hm, hn, hmn, ↓reduceIte]
 328  rw [bigOmega_mul hm hn, pow_add]
 329
 330/-! ### Identity function (for Dirichlet algebra) -/
 331
 332/-- The identity arithmetic function id(n) = n. -/
 333abbrev arithId : ArithmeticFunction ℕ := ArithmeticFunction.id
 334
 335@[simp] theorem arithId_def : arithId = ArithmeticFunction.id := rfl
 336
 337/-- id(n) = n. -/
 338theorem arithId_apply {n : ℕ} : arithId n = n := by
 339  simp [arithId]
 340
 341/-- The identity function is multiplicative. -/
 342theorem arithId_isMultiplicative : ArithmeticFunction.IsMultiplicative arithId := by
 343  simp only [arithId]
 344  exact ArithmeticFunction.isMultiplicative_id
 345
 346/-! ### Prime counting function π -/
 347
 348/-- The prime counting function π(n) = #{p ≤ n : p prime}. -/
 349def primeCounting (n : ℕ) : ℕ := Nat.primeCounting n
 350
 351@[simp] theorem primeCounting_def {n : ℕ} : primeCounting n = Nat.primeCounting n := rfl
 352
 353/-- π(0) = 0. -/
 354theorem primeCounting_zero : primeCounting 0 = 0 := by
 355  simp [primeCounting]
 356
 357/-- π(1) = 0. -/
 358theorem primeCounting_one : primeCounting 1 = 0 := by
 359  simp [primeCounting, Nat.primeCounting]
 360
 361/-- π(2) = 1. -/
 362theorem primeCounting_two : primeCounting 2 = 1 := by
 363  native_decide
 364
 365/-- π(3) = 2. -/
 366theorem primeCounting_three : primeCounting 3 = 2 := by
 367  native_decide
 368
 369/-- π(5) = 3. -/
 370theorem primeCounting_five : primeCounting 5 = 3 := by
 371  native_decide
 372
 373/-- π(10) = 4. -/
 374theorem primeCounting_ten : primeCounting 10 = 4 := by
 375  native_decide
 376
 377/-- π(7) = 4. -/
 378theorem primeCounting_seven : primeCounting 7 = 4 := by
 379  native_decide
 380
 381/-- π(11) = 5. -/
 382theorem primeCounting_eleven : primeCounting 11 = 5 := by
 383  native_decide
 384
 385/-- π(13) = 6. -/
 386theorem primeCounting_thirteen : primeCounting 13 = 6 := by
 387  native_decide
 388
 389/-- π(17) = 7. -/
 390theorem primeCounting_seventeen : primeCounting 17 = 7 := by
 391  native_decide
 392
 393/-- π(20) = 8. -/
 394theorem primeCounting_twenty : primeCounting 20 = 8 := by
 395  native_decide
 396
 397/-- π(100) = 25. -/
 398theorem primeCounting_hundred : primeCounting 100 = 25 := by
 399  native_decide
 400
 401/-- π is monotone: m ≤ n → π(m) ≤ π(n). -/
 402theorem primeCounting_mono {m n : ℕ} (h : m ≤ n) : primeCounting m ≤ primeCounting n := by
 403  simp only [primeCounting]
 404  exact Nat.monotone_primeCounting h
 405
 406/-! ### Liouville-squarefree connection -/
 407
 408/-- For squarefree n, λ(n) = μ(n). -/
 409theorem liouville_eq_mobius_of_squarefree {n : ℕ} (hn : n ≠ 0) (hsq : Squarefree n) :
 410    liouville n = mobius n := by
 411  rw [liouville_eq hn, mobius_apply_of_squarefree hsq, bigOmega_eq_omega_of_squarefree hn hsq]
 412
 413/-- μ(n)² = 1 iff n is squarefree. -/
 414theorem mobius_sq_eq_one_iff_squarefree {n : ℕ} : mobius n ^ 2 = 1 ↔ Squarefree n := by
 415  constructor
 416  · intro h
 417    by_contra hnsq
 418    have hμ : mobius n = 0 := mobius_eq_zero_of_not_squarefree hnsq
 419    simp [hμ] at h
 420  · intro hsq
 421    -- μ(n) ∈ {-1, 1} for squarefree n, so μ(n)² = 1
 422    have h_val := mobius_apply_of_squarefree hsq
 423    rw [h_val, ← pow_mul, mul_comm]
 424    have h_even : Even (2 * bigOmega n) := even_two_mul (bigOmega n)
 425    exact Even.neg_one_pow h_even
 426
 427/-! ### Values at 1 -/
 428
 429/-- μ(1) = 1. -/
 430theorem mobius_one : mobius 1 = 1 := by
 431  simp [mobius]
 432
 433/-- ω(1) = 0. -/
 434theorem omega_one : omega 1 = 0 := by
 435  simp [omega_apply]
 436
 437/-- Ω(1) = 0. -/
 438theorem bigOmega_one : bigOmega 1 = 0 := by
 439  simp [bigOmega_apply]
 440
 441/-- σ_k(1) = 1 for any k. -/
 442theorem sigma_one {k : ℕ} : sigma k 1 = 1 := by
 443  simp [sigma_apply]
 444
 445/-- ζ(1) = 1. -/
 446theorem zeta_one : zeta 1 = 1 := by
 447  exact zeta_apply (by decide)
 448
 449/-! ### Values at primes -/
 450
 451/-- ω(p) = 1 for prime p. -/
 452theorem omega_prime {p : ℕ} (hp : Prime p) : omega p = 1 := by
 453  have hp' : Nat.Prime p := (prime_iff p).1 hp
 454  simp only [omega]
 455  exact ArithmeticFunction.cardDistinctFactors_apply_prime hp'
 456
 457/-- Ω(p) = 1 for prime p. -/
 458theorem bigOmega_prime {p : ℕ} (hp : Prime p) : bigOmega p = 1 := by
 459  have hp' : Nat.Prime p := (prime_iff p).1 hp
 460  exact ArithmeticFunction.cardFactors_apply_prime hp'
 461
 462/-! ### Additional totient values -/
 463
 464/-- φ(2) = 1. -/
 465theorem totient_two : totient 2 = 1 := by
 466  simp [totient]
 467
 468/-- φ(3) = 2. -/
 469theorem totient_three : totient 3 = 2 := by
 470  native_decide
 471
 472/-- φ(4) = 2. -/
 473theorem totient_four : totient 4 = 2 := by
 474  native_decide
 475
 476/-- φ(5) = 4. -/
 477theorem totient_five : totient 5 = 4 := by
 478  native_decide
 479
 480/-- φ(6) = 2. -/
 481theorem totient_six : totient 6 = 2 := by
 482  native_decide
 483
 484/-- φ(8) = 4. -/
 485theorem totient_eight : totient 8 = 4 := by
 486  native_decide
 487
 488/-- φ(45) = 24. -/
 489theorem totient_fortyfive : totient 45 = 24 := by
 490  native_decide
 491
 492/-- φ(360) = 96. -/
 493theorem totient_threehundredsixty : totient 360 = 96 := by
 494  native_decide
 495
 496/-! ### Ω and ω at prime powers -/
 497
 498/-- Ω(p^k) = k for prime p. -/
 499theorem bigOmega_prime_pow {p k : ℕ} (hp : Prime p) : bigOmega (p ^ k) = k := by
 500  have hp' : Nat.Prime p := (prime_iff p).1 hp
 501  cases k with
 502  | zero => simp [bigOmega_apply]
 503  | succ k => exact ArithmeticFunction.cardFactors_apply_prime_pow hp'
 504
 505/-- ω(p^k) = 1 for prime p and k ≥ 1. -/
 506theorem omega_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) : omega (p ^ k) = 1 := by
 507  have hp' : Nat.Prime p := (prime_iff p).1 hp
 508  have hk' : k ≠ 0 := Nat.pos_iff_ne_zero.mp hk
 509  simp only [omega]
 510  exact ArithmeticFunction.cardDistinctFactors_apply_prime_pow hp' hk'
 511
 512/-! ### Sigma at prime powers -/
 513
 514/-- σ_0(p^k) = k + 1 for prime p (number of divisors of p^k). -/
 515theorem sigma_zero_prime_pow {p k : ℕ} (hp : Prime p) : sigma 0 (p ^ k) = k + 1 := by
 516  have hp' : Nat.Prime p := (prime_iff p).1 hp
 517  simp only [sigma_zero_apply]
 518  rw [Nat.divisors_prime_pow hp' k]
 519  simp
 520
 521/-- Concrete sigma values at small prime powers. -/
 522theorem sigma_one_two_pow_one : sigma 1 (2 ^ 1) = 3 := by native_decide
 523theorem sigma_one_two_pow_two : sigma 1 (2 ^ 2) = 7 := by native_decide
 524theorem sigma_one_two_pow_three : sigma 1 (2 ^ 3) = 15 := by native_decide
 525theorem sigma_one_three_pow_one : sigma 1 (3 ^ 1) = 4 := by native_decide
 526theorem sigma_one_three_pow_two : sigma 1 (3 ^ 2) = 13 := by native_decide
 527theorem sigma_one_five_pow_one : sigma 1 (5 ^ 1) = 6 := by native_decide
 528
 529/-! ### Totient multiplicativity -/
 530
 531/-- Euler's totient function is multiplicative. -/
 532theorem totient_isMultiplicative :
 533    ∀ {m n : ℕ}, Nat.Coprime m n → totient (m * n) = totient m * totient n := by
 534  intro m n h
 535  exact totient_mul_of_coprime h
 536
 537/-! ### Divisors of prime powers -/
 538
 539/-- The divisors of p^k are exactly {p^0, p^1, ..., p^k}. -/
 540theorem divisors_prime_pow {p k : ℕ} (hp : Prime p) :
 541    (p ^ k).divisors = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective hp.one_lt⟩ := by
 542  have hp' : Nat.Prime p := (prime_iff p).1 hp
 543  exact Nat.divisors_prime_pow hp' k
 544
 545/-- The number of divisors of p^k is k + 1. -/
 546theorem card_divisors_prime_pow {p k : ℕ} (hp : Prime p) : (p ^ k).divisors.card = k + 1 := by
 547  rw [divisors_prime_pow hp]
 548  simp
 549
 550/-! ### Additional small prime facts -/
 551
 552theorem prime_twentythree : Prime 23 := by decide
 553theorem prime_twentynine : Prime 29 := by decide
 554theorem prime_thirtyone : Prime 31 := by decide
 555theorem prime_fortyone : Prime 41 := by decide
 556theorem prime_fortythree : Prime 43 := by decide
 557theorem prime_fortyseven : Prime 47 := by decide
 558theorem prime_fiftythree : Prime 53 := by decide
 559theorem prime_fiftynine : Prime 59 := by decide
 560theorem prime_sixtyone : Prime 61 := by decide
 561theorem prime_sixtyseven : Prime 67 := by decide
 562theorem prime_seventyone : Prime 71 := by decide
 563theorem prime_seventythree : Prime 73 := by decide
 564theorem prime_seventynine : Prime 79 := by decide
 565theorem prime_eightythree : Prime 83 := by decide
 566theorem prime_eightynine : Prime 89 := by decide
 567theorem prime_ninetyseven : Prime 97 := by decide
 568
 569/-! ### Factorial valuations (decidable facts) -/
 570
 571/-- vp 2 (4!) = 3. -/
 572theorem vp_factorial_four_two : vp 2 (Nat.factorial 4) = 3 := by native_decide
 573
 574/-- vp 2 (5!) = 3. -/
 575theorem vp_factorial_five_two : vp 2 (Nat.factorial 5) = 3 := by native_decide
 576
 577/-- vp 2 (6!) = 4. -/
 578theorem vp_factorial_six_two : vp 2 (Nat.factorial 6) = 4 := by native_decide
 579
 580/-- vp 2 (8!) = 7. -/
 581theorem vp_factorial_eight_two : vp 2 (Nat.factorial 8) = 7 := by native_decide
 582
 583/-- vp 3 (6!) = 2. -/
 584theorem vp_factorial_six_three : vp 3 (Nat.factorial 6) = 2 := by native_decide
 585
 586/-- vp 3 (9!) = 4. -/
 587theorem vp_factorial_nine_three : vp 3 (Nat.factorial 9) = 4 := by native_decide
 588
 589/-- vp 5 (10!) = 2. -/
 590theorem vp_factorial_ten_five : vp 5 (Nat.factorial 10) = 2 := by native_decide
 591
 592/-! ### Product lemmas for Ω and ω -/
 593
 594/-- Ω(n!) for small factorials.
 595- 2! = 2 → Ω = 1
 596- 3! = 6 = 2*3 → Ω = 2
 597- 4! = 24 = 2³*3 → Ω = 4
 598- 5! = 120 = 2³*3*5 → Ω = 5
 599-/
 600theorem bigOmega_factorial_two : bigOmega (Nat.factorial 2) = 1 := by native_decide
 601theorem bigOmega_factorial_three : bigOmega (Nat.factorial 3) = 2 := by native_decide
 602theorem bigOmega_factorial_four : bigOmega (Nat.factorial 4) = 4 := by native_decide
 603theorem bigOmega_factorial_five : bigOmega (Nat.factorial 5) = 5 := by native_decide
 604
 605/-! ### Perfect numbers -/
 606
 607/-- A number n is perfect if σ_1(n) = 2n.
 608We make this decidable for concrete values. -/
 609def isPerfect (n : ℕ) : Prop := sigma 1 n = 2 * n
 610
 611instance : DecidablePred isPerfect := fun n => inferInstanceAs (Decidable (sigma 1 n = 2 * n))
 612
 613/-- 6 is perfect. -/
 614theorem isPerfect_six : isPerfect 6 := by native_decide
 615
 616/-- 28 is perfect. -/
 617theorem isPerfect_twentyeight : isPerfect 28 := by native_decide
 618
 619/-- 496 is perfect. -/
 620theorem isPerfect_fourhundredninetysix : isPerfect 496 := by native_decide
 621
 622/-! ### More primeCounting values -/
 623
 624/-- π(30) = 10. -/
 625theorem primeCounting_thirty : primeCounting 30 = 10 := by native_decide
 626
 627/-- π(50) = 15. -/
 628theorem primeCounting_fifty : primeCounting 50 = 15 := by native_decide
 629
 630/-- π(200) = 46. -/
 631theorem primeCounting_twohundred : primeCounting 200 = 46 := by native_decide
 632
 633/-- π(1000) = 168. -/
 634theorem primeCounting_thousand : primeCounting 1000 = 168 := by native_decide
 635
 636/-! ### Ω and ω for RS constants -/
 637
 638/-- Ω(8) = 3 (since 8 = 2³). -/
 639theorem bigOmega_eight : bigOmega 8 = 3 := by native_decide
 640
 641/-- Ω(45) = 3 (since 45 = 3² × 5). -/
 642theorem bigOmega_fortyfive : bigOmega 45 = 3 := by native_decide
 643
 644/-- Ω(360) = 6 (since 360 = 2³ × 3² × 5). -/
 645theorem bigOmega_threehundredsixty : bigOmega 360 = 6 := by native_decide
 646
 647/-- Ω(840) = 6 (since 840 = 2³ × 3 × 5 × 7, with 3+1+1+1 = 6 factors). -/
 648theorem bigOmega_eighthundredforty : bigOmega 840 = 6 := by native_decide
 649
 650/-- ω(8) = 1 (only prime factor is 2). -/
 651theorem omega_eight : omega 8 = 1 := by native_decide
 652
 653/-- ω(45) = 2 (prime factors are 3 and 5). -/
 654theorem omega_fortyfive : omega 45 = 2 := by native_decide
 655
 656/-- ω(360) = 3 (prime factors are 2, 3, 5). -/
 657theorem omega_threehundredsixty : omega 360 = 3 := by native_decide
 658
 659/-- ω(840) = 4 (prime factors are 2, 3, 5, 7). -/
 660theorem omega_eighthundredforty : omega 840 = 4 := by native_decide
 661
 662/-! ### Radical (product of distinct prime factors) -/
 663
 664/-- The radical of n is the product of its distinct prime factors. -/
 665def radical (n : ℕ) : ℕ := n.primeFactors.prod id
 666
 667/-- rad(1) = 1. -/
 668theorem radical_one' : radical 1 = 1 := by native_decide
 669
 670/-- rad(2) = 2. -/
 671theorem radical_two' : radical 2 = 2 := by native_decide
 672
 673/-- rad(6) = 6 (squarefree). -/
 674theorem radical_six' : radical 6 = 6 := by native_decide
 675
 676/-- rad(12) = 6. -/
 677theorem radical_twelve' : radical 12 = 6 := by native_decide
 678
 679/-- rad(p) = p for prime p. -/
 680theorem radical_prime' {p : ℕ} (hp : Prime p) : radical p = p := by
 681  have hp' : Nat.Prime p := (prime_iff p).1 hp
 682  simp only [radical]
 683  rw [Nat.Prime.primeFactors hp']
 684  simp
 685
 686/-! ### Totient as cardinality -/
 687
 688/-- φ(n) = |{a ∈ [0,n) : gcd(n,a) = 1}|. -/
 689theorem totient_eq_card_filter {n : ℕ} :
 690    totient n = (Finset.filter (fun a => n.Coprime a) (Finset.range n)).card := by
 691  simp only [totient]
 692  exact Nat.totient_eq_card_coprime n
 693
 694/-! ### Additional coprimality facts for RS constants -/
 695
 696/-- gcd(8, 360) = 8. -/
 697theorem gcd_eight_threehundredsixty : Nat.gcd 8 360 = 8 := by native_decide
 698
 699/-- gcd(45, 360) = 45. -/
 700theorem gcd_fortyfive_threehundredsixty : Nat.gcd 45 360 = 45 := by native_decide
 701
 702/-- gcd(8, 840) = 8. -/
 703theorem gcd_eight_eighthundredforty : Nat.gcd 8 840 = 8 := by native_decide
 704
 705/-- gcd(45, 840) = 15. -/
 706theorem gcd_fortyfive_eighthundredforty : Nat.gcd 45 840 = 15 := by native_decide
 707
 708/-- gcd(360, 840) = 120. -/
 709theorem gcd_threehundredsixty_eighthundredforty : Nat.gcd 360 840 = 120 := by native_decide
 710
 711/-- lcm(8, 840) = 840. -/
 712theorem lcm_eight_eighthundredforty : Nat.lcm 8 840 = 840 := by native_decide
 713
 714/-- lcm(45, 840) = 2520. -/
 715theorem lcm_fortyfive_eighthundredforty : Nat.lcm 45 840 = 2520 := by native_decide
 716
 717/-- lcm(360, 840) = 2520. -/
 718theorem lcm_threehundredsixty_eighthundredforty : Nat.lcm 360 840 = 2520 := by native_decide
 719
 720/-! ### Sigma values at RS constants -/
 721
 722/-- σ_0(8) = 4. -/
 723theorem sigma_zero_eight : sigma 0 8 = 4 := by native_decide
 724
 725/-- σ_0(45) = 6. -/
 726theorem sigma_zero_fortyfive : sigma 0 45 = 6 := by native_decide
 727
 728/-- σ_0(360) = 24. -/
 729theorem sigma_zero_threehundredsixty : sigma 0 360 = 24 := by native_decide
 730
 731/-- σ_1(8) = 15. -/
 732theorem sigma_one_eight : sigma 1 8 = 15 := by native_decide
 733
 734/-- σ_1(45) = 78. -/
 735theorem sigma_one_fortyfive : sigma 1 45 = 78 := by native_decide
 736
 737/-- σ_1(360) = 1170. -/
 738theorem sigma_one_threehundredsixty : sigma 1 360 = 1170 := by native_decide
 739
 740/-! ### Prime factors of primes and prime powers -/
 741
 742/-- The prime factors of a prime p is just {p}. -/
 743theorem primeFactors_prime {p : ℕ} (hp : Prime p) : p.primeFactors = {p} := by
 744  have hp' : Nat.Prime p := (prime_iff p).1 hp
 745  exact Nat.Prime.primeFactors hp'
 746
 747/-- The prime factors of p^k (k ≥ 1) is just {p}. -/
 748theorem primeFactors_prime_pow {p k : ℕ} (hp : Prime p) (hk : k ≠ 0) :
 749    (p ^ k).primeFactors = {p} := by
 750  have hp' : Nat.Prime p := (prime_iff p).1 hp
 751  exact Nat.primeFactors_prime_pow hk hp'
 752
 753/-- rad(p^k) = p for prime p and k ≥ 1. -/
 754theorem radical_prime_pow {p k : ℕ} (hp : Prime p) (hk : k ≠ 0) : radical (p ^ k) = p := by
 755  simp only [radical, primeFactors_prime_pow hp hk, Finset.prod_singleton, id]
 756
 757/-! ### Von Mangoldt sum identity -/
 758
 759/-- The sum of von Mangoldt over divisors: ∑_{d|n} Λ(d) = log(n).
 760    This connects Λ to the logarithm. -/
 761theorem vonMangoldt_sum_divisors {n : ℕ} :
 762    ∑ d ∈ n.divisors, vonMangoldt d = Real.log n := by
 763  simp only [vonMangoldt]
 764  exact ArithmeticFunction.vonMangoldt_sum
 765
 766/-! ### Sigma multiplicativity helpers -/
 767
 768/-- σ_k(mn) = σ_k(m) × σ_k(n) for coprime m, n. -/
 769theorem sigma_mul_of_coprime {k m n : ℕ} (h : Nat.Coprime m n) :
 770    sigma k (m * n) = sigma k m * sigma k n := by
 771  simp only [sigma]
 772  exact ArithmeticFunction.isMultiplicative_sigma.map_mul_of_coprime h
 773
 774/-- σ_0(mn) = σ_0(m) × σ_0(n) for coprime m, n. -/
 775theorem sigma_zero_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 776    sigma 0 (m * n) = sigma 0 m * sigma 0 n :=
 777  sigma_mul_of_coprime h
 778
 779/-- σ_1(mn) = σ_1(m) × σ_1(n) for coprime m, n. -/
 780theorem sigma_one_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 781    sigma 1 (m * n) = sigma 1 m * sigma 1 n :=
 782  sigma_mul_of_coprime h
 783
 784/-! ### Totient product formula helpers -/
 785
 786/-- φ(n) > 0 for n > 0 (strengthened). -/
 787theorem totient_pos {n : ℕ} (hn : 0 < n) : 0 < totient n := by
 788  simp only [totient]
 789  exact Nat.totient_pos.mpr hn
 790
 791/-- φ(2^k) = 2^k - 2^(k-1) = 2^(k-1) for k ≥ 1 (concrete). -/
 792theorem totient_two_pow_one : totient (2 ^ 1) = 1 := by native_decide
 793theorem totient_two_pow_two : totient (2 ^ 2) = 2 := by native_decide
 794theorem totient_two_pow_three : totient (2 ^ 3) = 4 := by native_decide
 795theorem totient_two_pow_four : totient (2 ^ 4) = 8 := by native_decide
 796
 797/-- φ(3^k) values. -/
 798theorem totient_three_pow_one : totient (3 ^ 1) = 2 := by native_decide
 799theorem totient_three_pow_two : totient (3 ^ 2) = 6 := by native_decide
 800
 801/-- φ(5^k) values. -/
 802theorem totient_five_pow_one : totient (5 ^ 1) = 4 := by native_decide
 803theorem totient_five_pow_two : totient (5 ^ 2) = 20 := by native_decide
 804
 805/-! ### More concrete arithmetic function values -/
 806
 807/-- Ω(6) = 2 (since 6 = 2 × 3). -/
 808theorem bigOmega_six : bigOmega 6 = 2 := by native_decide
 809
 810/-- ω(6) = 2 (distinct prime factors: 2, 3). -/
 811theorem omega_six : omega 6 = 2 := by native_decide
 812
 813/-- Ω(12) = 3 (since 12 = 2² × 3). -/
 814theorem bigOmega_twelve : bigOmega 12 = 3 := by native_decide
 815
 816/-- ω(12) = 2 (distinct prime factors: 2, 3). -/
 817theorem omega_twelve : omega 12 = 2 := by native_decide
 818
 819/-- Ω(30) = 3 (since 30 = 2 × 3 × 5). -/
 820theorem bigOmega_thirty : bigOmega 30 = 3 := by native_decide
 821
 822/-- ω(30) = 3 (distinct prime factors: 2, 3, 5). -/
 823theorem omega_thirty : omega 30 = 3 := by native_decide
 824
 825/-- μ(6) = 1 (squarefree with 2 prime factors). -/
 826theorem mobius_six : mobius 6 = 1 := by native_decide
 827
 828/-- μ(30) = -1 (squarefree with 3 prime factors). -/
 829theorem mobius_thirty : mobius 30 = -1 := by native_decide
 830
 831/-- μ(12) = 0 (not squarefree, since 4 | 12). -/
 832theorem mobius_twelve : mobius 12 = 0 := by native_decide
 833
 834/-- rad(30) = 30 (squarefree). -/
 835theorem radical_thirty : radical 30 = 30 := by native_decide
 836
 837/-- rad(60) = 30. -/
 838theorem radical_sixty : radical 60 = 30 := by native_decide
 839
 840/-- rad(360) = 30. -/
 841theorem radical_threehundredsixty : radical 360 = 30 := by native_decide
 842
 843/-- rad(840) = 210 = 2 × 3 × 5 × 7. -/
 844theorem radical_eighthundredforty : radical 840 = 210 := by native_decide
 845
 846/-! ### Radical algebra -/
 847
 848/-- rad(n) ≤ n for all n ≠ 0. -/
 849theorem radical_le {n : ℕ} (hn : n ≠ 0) : radical n ≤ n := by
 850  simp only [radical]
 851  have h := Nat.prod_primeFactors_dvd n
 852  exact Nat.le_of_dvd (Nat.pos_of_ne_zero hn) h
 853
 854/-- rad(1) = 1 (using the general definition). -/
 855theorem radical_one_eq : radical 1 = 1 := by native_decide
 856
 857/-- rad(n) > 0 for n > 0. -/
 858theorem radical_pos {n : ℕ} (_hn : 0 < n) : 0 < radical n := by
 859  simp only [radical]
 860  exact Finset.prod_pos (fun p hp => Nat.Prime.pos (Nat.prime_of_mem_primeFactors hp))
 861
 862/-! ### Coprimality power lemmas -/
 863
 864/-- Coprimality is preserved by powers on the left. -/
 865theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
 866    Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b := by
 867  exact Nat.coprime_pow_left_iff hn a b
 868
 869/-- Coprimality is preserved by powers on the right. -/
 870theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
 871    Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b := by
 872  exact Nat.coprime_pow_right_iff hn a b
 873
 874/-- If p is prime and doesn't divide a, then a is coprime to p^m. -/
 875theorem coprime_pow_of_prime_not_dvd {p m a : ℕ} (hp : Prime p) (h : ¬p ∣ a) :
 876    Nat.Coprime a (p ^ m) := by
 877  have hp' : Nat.Prime p := (prime_iff p).1 hp
 878  exact hp'.coprime_pow_of_not_dvd h
 879
 880/-- Two distinct primes raised to powers are coprime. -/
 881theorem coprime_prime_pow {p q n m : ℕ} (hp : Prime p) (hq : Prime q) (hne : p ≠ q) :
 882    Nat.Coprime (p ^ n) (q ^ m) := by
 883  have hp' : Nat.Prime p := (prime_iff p).1 hp
 884  have hq' : Nat.Prime q := (prime_iff q).1 hq
 885  exact Nat.coprime_pow_primes n m hp' hq' hne
 886
 887/-! ### More primeCounting values -/
 888
 889/-- π(150) = 35. -/
 890theorem primeCounting_onehundredfifty : primeCounting 150 = 35 := by native_decide
 891
 892/-- π(250) = 53. -/
 893theorem primeCounting_twohundredfifty : primeCounting 250 = 53 := by native_decide
 894
 895/-- π(500) = 95. -/
 896theorem primeCounting_fivehundred : primeCounting 500 = 95 := by native_decide
 897
 898/-- π(750) = 132. -/
 899theorem primeCounting_sevenhundredfifty : primeCounting 750 = 132 := by native_decide
 900
 901/-! ### Legendre formula concrete values -/
 902
 903/-- vp 2 (10!) = 8. -/
 904theorem vp_factorial_ten_two : vp 2 (Nat.factorial 10) = 8 := by native_decide
 905
 906/-- vp 2 (12!) = 10. -/
 907theorem vp_factorial_twelve_two : vp 2 (Nat.factorial 12) = 10 := by native_decide
 908
 909/-- vp 3 (10!) = 4. -/
 910theorem vp_factorial_ten_three : vp 3 (Nat.factorial 10) = 4 := by native_decide
 911
 912/-- vp 3 (12!) = 5. -/
 913theorem vp_factorial_twelve_three : vp 3 (Nat.factorial 12) = 5 := by native_decide
 914
 915/-- vp 5 (25!) = 6. -/
 916theorem vp_factorial_twentyfive_five : vp 5 (Nat.factorial 25) = 6 := by native_decide
 917
 918/-- vp 7 (50!) = 8. -/
 919theorem vp_factorial_fifty_seven : vp 7 (Nat.factorial 50) = 8 := by native_decide
 920
 921/-! ### More squarefree concrete values -/
 922
 923/-- 30 is squarefree. -/
 924theorem squarefree_thirty : Squarefree 30 := by native_decide
 925
 926/-- 6 is squarefree. -/
 927theorem squarefree_six : Squarefree 6 := by native_decide
 928
 929/-- 10 is squarefree. -/
 930theorem squarefree_ten : Squarefree 10 := by native_decide
 931
 932/-- 15 is squarefree. -/
 933theorem squarefree_fifteen : Squarefree 15 := by native_decide
 934
 935/-- 210 = 2×3×5×7 is squarefree. -/
 936theorem squarefree_twohundredten : Squarefree 210 := by native_decide
 937
 938/-! ### Divisor count for RS constants -/
 939
 940/-- The number of divisors of 8 is 4. -/
 941theorem divisors_card_eight : (8 : ℕ).divisors.card = 4 := by native_decide
 942
 943/-- The number of divisors of 45 is 6. -/
 944theorem divisors_card_fortyfive : (45 : ℕ).divisors.card = 6 := by native_decide
 945
 946/-- The number of divisors of 360 is 24. -/
 947theorem divisors_card_threehundredsixty : (360 : ℕ).divisors.card = 24 := by native_decide
 948
 949/-- The number of divisors of 840 is 32. -/
 950theorem divisors_card_eighthundredforty : (840 : ℕ).divisors.card = 32 := by native_decide
 951
 952/-! ### More small primes (101-199) -/
 953
 954theorem prime_onehundredone : Prime 101 := by native_decide
 955theorem prime_onehundredseven : Prime 107 := by native_decide
 956theorem prime_onehundrednine : Prime 109 := by native_decide
 957theorem prime_onehundredthirteen : Prime 113 := by native_decide
 958theorem prime_onehundredtwentyseven : Prime 127 := by native_decide
 959theorem prime_onehundredthirtyone : Prime 131 := by native_decide
 960theorem prime_onehundredthirtynine : Prime 139 := by native_decide
 961theorem prime_onehundredfortynine : Prime 149 := by native_decide
 962theorem prime_onehundredfiftyone : Prime 151 := by native_decide
 963theorem prime_onehundredfiftyseven : Prime 157 := by native_decide
 964theorem prime_onehundredsixtythree : Prime 163 := by native_decide
 965theorem prime_onehundredsixtyseven : Prime 167 := by native_decide
 966theorem prime_onehundredseventythree : Prime 173 := by native_decide
 967theorem prime_onehundredseventynine : Prime 179 := by native_decide
 968theorem prime_onehundredeightyone : Prime 181 := by native_decide
 969theorem prime_onehundredninetyone : Prime 191 := by native_decide
 970theorem prime_onehundredninetythree : Prime 193 := by native_decide
 971theorem prime_onehundredninetyseven : Prime 197 := by native_decide
 972theorem prime_onehundredninetynine : Prime 199 := by native_decide
 973
 974/-! ### Sigma values at small composites -/
 975
 976/-- σ_0(6) = 4 (divisors: 1, 2, 3, 6). -/
 977theorem sigma_zero_six : sigma 0 6 = 4 := by native_decide
 978
 979/-- σ_1(6) = 12 (sum: 1 + 2 + 3 + 6 = 12). -/
 980theorem sigma_one_six : sigma 1 6 = 12 := by native_decide
 981
 982/-- σ_0(10) = 4 (divisors: 1, 2, 5, 10). -/
 983theorem sigma_zero_ten : sigma 0 10 = 4 := by native_decide
 984
 985/-- σ_1(10) = 18 (sum: 1 + 2 + 5 + 10 = 18). -/
 986theorem sigma_one_ten : sigma 1 10 = 18 := by native_decide
 987
 988/-- σ_0(12) = 6 (divisors: 1, 2, 3, 4, 6, 12). -/
 989theorem sigma_zero_twelve : sigma 0 12 = 6 := by native_decide
 990
 991/-- σ_1(12) = 28 (sum: 1 + 2 + 3 + 4 + 6 + 12 = 28). -/
 992theorem sigma_one_twelve : sigma 1 12 = 28 := by native_decide
 993
 994/-- σ_0(30) = 8. -/
 995theorem sigma_zero_thirty : sigma 0 30 = 8 := by native_decide
 996
 997/-- σ_1(30) = 72. -/
 998theorem sigma_one_thirty : sigma 1 30 = 72 := by native_decide
 999
1000/-! ### Totient at small composites -/
1001
1002/-- φ(10) = 4. -/
1003theorem totient_ten : totient 10 = 4 := by native_decide
1004
1005/-- φ(12) = 4. -/
1006theorem totient_twelve : totient 12 = 4 := by native_decide
1007
1008/-- φ(30) = 8. -/
1009theorem totient_thirty : totient 30 = 8 := by native_decide
1010
1011/-- φ(24) = 8. -/
1012theorem totient_twentyfour : totient 24 = 8 := by native_decide
1013
1014/-- φ(36) = 12. -/
1015theorem totient_thirtysix : totient 36 = 12 := by native_decide
1016
1017/-- φ(48) = 16. -/
1018theorem totient_fortyeight : totient 48 = 16 := by native_decide
1019
1020/-- φ(60) = 16. -/
1021theorem totient_sixty : totient 60 = 16 := by native_decide
1022
1023/-- φ(72) = 24. -/
1024theorem totient_seventytwo : totient 72 = 24 := by native_decide
1025
1026/-- φ(120) = 32. -/
1027theorem totient_onehundredtwenty : totient 120 = 32 := by native_decide
1028
1029/-! ### Liouville at small composites -/
1030
1031/-- λ(6) = 1 (6 = 2 × 3, Ω(6) = 2, even). -/
1032theorem liouville_six : liouville 6 = 1 := by native_decide
1033
1034/-- λ(10) = 1 (10 = 2 × 5, Ω(10) = 2, even). -/
1035theorem liouville_ten : liouville 10 = 1 := by native_decide
1036
1037/-- λ(12) = -1 (12 = 2² × 3, Ω(12) = 3, odd). -/
1038theorem liouville_twelve : liouville 12 = -1 := by native_decide
1039
1040/-- λ(30) = -1 (30 = 2 × 3 × 5, Ω(30) = 3, odd). -/
1041theorem liouville_thirty : liouville 30 = -1 := by native_decide
1042
1043/-- λ(8) = -1 (8 = 2³, Ω(8) = 3, odd). -/
1044theorem liouville_eight : liouville 8 = -1 := by native_decide
1045
1046/-- λ(45) = -1 (45 = 3² × 5, Ω(45) = 3, odd). -/
1047theorem liouville_fortyfive : liouville 45 = -1 := by native_decide
1048
1049/-- λ(360) = 1 (360 = 2³ × 3² × 5, Ω(360) = 6, even). -/
1050theorem liouville_threehundredsixty : liouville 360 = 1 := by native_decide
1051
1052/-- λ(840) = 1 (840 = 2³ × 3 × 5 × 7, Ω(840) = 6, even). -/
1053theorem liouville_eighthundredforty : liouville 840 = 1 := by native_decide
1054
1055/-! ### Coprimality of RS constants -/
1056
1057/-- gcd(8, 45) = 1 (already in RSConstants, aliased here for visibility). -/
1058theorem gcd_eight_fortyfive : Nat.gcd 8 45 = 1 := by native_decide
1059
1060/-- 8 and 45 are coprime. -/
1061theorem coprime_eight_fortyfive : Nat.Coprime 8 45 := by native_decide
1062
1063/-- 360 and 37 are coprime. -/
1064theorem coprime_threehundredsixty_thirtyseven : Nat.Coprime 360 37 := by native_decide
1065
1066/-- 8 and 37 are coprime. -/
1067theorem coprime_eight_thirtyseven : Nat.Coprime 8 37 := by native_decide
1068
1069/-- 45 and 37 are coprime. -/
1070theorem coprime_fortyfive_thirtyseven : Nat.Coprime 45 37 := by native_decide
1071
1072/-- gcd(360, 7) = 1 (7 does not divide 360). -/
1073theorem gcd_threehundredsixty_seven : Nat.gcd 360 7 = 1 := by native_decide
1074
1075/-- gcd(45, 8) = 1 (symmetric). -/
1076theorem gcd_fortyfive_eight : Nat.gcd 45 8 = 1 := by native_decide
1077
1078/-! ### More divisor counts -/
1079
1080/-- The number of divisors of 6 is 4. -/
1081theorem divisors_card_six : (6 : ℕ).divisors.card = 4 := by native_decide
1082
1083/-- The number of divisors of 10 is 4. -/
1084theorem divisors_card_ten : (10 : ℕ).divisors.card = 4 := by native_decide
1085
1086/-- The number of divisors of 12 is 6. -/
1087theorem divisors_card_twelve : (12 : ℕ).divisors.card = 6 := by native_decide
1088
1089/-- The number of divisors of 30 is 8. -/
1090theorem divisors_card_thirty : (30 : ℕ).divisors.card = 8 := by native_decide
1091
1092/-- The number of divisors of 60 is 12. -/
1093theorem divisors_card_sixty : (60 : ℕ).divisors.card = 12 := by native_decide
1094
1095/-- The number of divisors of 120 is 16. -/
1096theorem divisors_card_onehundredtwenty : (120 : ℕ).divisors.card = 16 := by native_decide
1097
1098/-! ### More Möbius values -/
1099
1100/-- μ(10) = 1 (squarefree with 2 prime factors). -/
1101theorem mobius_ten : mobius 10 = 1 := by native_decide
1102
1103/-- μ(15) = 1 (squarefree with 2 prime factors). -/
1104theorem mobius_fifteen : mobius 15 = 1 := by native_decide
1105
1106/-- μ(21) = 1 (squarefree with 2 prime factors). -/
1107theorem mobius_twentyone : mobius 21 = 1 := by native_decide
1108
1109/-- μ(35) = 1 (squarefree with 2 prime factors). -/
1110theorem mobius_thirtyfive : mobius 35 = 1 := by native_decide
1111
1112/-- μ(42) = -1 (squarefree with 3 prime factors). -/
1113theorem mobius_fortytwo : mobius 42 = -1 := by native_decide
1114
1115/-- μ(70) = -1 (squarefree with 3 prime factors). -/
1116theorem mobius_seventy : mobius 70 = -1 := by native_decide
1117
1118/-- μ(105) = -1 (squarefree with 3 prime factors). -/
1119theorem mobius_onehundredfive : mobius 105 = -1 := by native_decide
1120
1121/-- μ(210) = 1 (squarefree with 4 prime factors). -/
1122theorem mobius_twohundredten : mobius 210 = 1 := by native_decide
1123
1124/-- μ(18) = 0 (not squarefree, 9 | 18). -/
1125theorem mobius_eighteen : mobius 18 = 0 := by native_decide
1126
1127/-- μ(20) = 0 (not squarefree, 4 | 20). -/
1128theorem mobius_twenty : mobius 20 = 0 := by native_decide
1129
1130/-! ### More squarefree values -/
1131
1132/-- 42 = 2×3×7 is squarefree. -/
1133theorem squarefree_fortytwo : Squarefree 42 := by native_decide
1134
1135/-- 70 = 2×5×7 is squarefree. -/
1136theorem squarefree_seventy : Squarefree 70 := by native_decide
1137
1138/-- 105 = 3×5×7 is squarefree. -/
1139theorem squarefree_onehundredfive : Squarefree 105 := by native_decide
1140
1141/-- 77 = 7×11 is squarefree. -/
1142theorem squarefree_seventyseven : Squarefree 77 := by native_decide
1143
1144/-- 91 = 7×13 is squarefree. -/
1145theorem squarefree_ninetyone : Squarefree 91 := by native_decide
1146
1147/-- 35 = 5×7 is squarefree. -/
1148theorem squarefree_thirtyfive : Squarefree 35 := by native_decide
1149
1150/-- 21 = 3×7 is squarefree. -/
1151theorem squarefree_twentyone : Squarefree 21 := by native_decide
1152
1153/-- 33 = 3×11 is squarefree. -/
1154theorem squarefree_thirtythree : Squarefree 33 := by native_decide
1155
1156/-- 18 is NOT squarefree (9 | 18). -/
1157theorem not_squarefree_eighteen : ¬Squarefree 18 := by native_decide
1158
1159/-- 20 is NOT squarefree (4 | 20). -/
1160theorem not_squarefree_twenty : ¬Squarefree 20 := by native_decide
1161
1162/-- 50 is NOT squarefree (25 | 50). -/
1163theorem not_squarefree_fifty : ¬Squarefree 50 := by native_decide
1164
1165/-! ### Twin prime pairs (decidable) -/
1166
1167/-- 3 and 5 are twin primes. -/
1168theorem twin_prime_three_five : Prime 3 ∧ Prime 5 ∧ 5 = 3 + 2 := by native_decide
1169
1170/-- 5 and 7 are twin primes. -/
1171theorem twin_prime_five_seven : Prime 5 ∧ Prime 7 ∧ 7 = 5 + 2 := by native_decide
1172
1173/-- 11 and 13 are twin primes. -/
1174theorem twin_prime_eleven_thirteen : Prime 11 ∧ Prime 13 ∧ 13 = 11 + 2 := by native_decide
1175
1176/-- 17 and 19 are twin primes. -/
1177theorem twin_prime_seventeen_nineteen : Prime 17 ∧ Prime 19 ∧ 19 = 17 + 2 := by native_decide
1178
1179/-- 29 and 31 are twin primes. -/
1180theorem twin_prime_twentynine_thirtyone : Prime 29 ∧ Prime 31 ∧ 31 = 29 + 2 := by native_decide
1181
1182/-- 41 and 43 are twin primes. -/
1183theorem twin_prime_fortyone_fortythree : Prime 41 ∧ Prime 43 ∧ 43 = 41 + 2 := by native_decide
1184
1185/-- 59 and 61 are twin primes. -/
1186theorem twin_prime_fiftynine_sixtyone : Prime 59 ∧ Prime 61 ∧ 61 = 59 + 2 := by native_decide
1187
1188/-- 71 and 73 are twin primes. -/
1189theorem twin_prime_seventyone_seventythree : Prime 71 ∧ Prime 73 ∧ 73 = 71 + 2 := by native_decide
1190
1191/-! ### More arithmetic function values at RS-related numbers -/
1192
1193/-- ω(120) = 3 (distinct prime factors: 2, 3, 5). -/
1194theorem omega_onehundredtwenty : omega 120 = 3 := by native_decide
1195
1196/-- Ω(120) = 5 (120 = 2³ × 3 × 5). -/
1197theorem bigOmega_onehundredtwenty : bigOmega 120 = 5 := by native_decide
1198
1199/-- σ_1(120) = 360. -/
1200theorem sigma_one_onehundredtwenty : sigma 1 120 = 360 := by native_decide
1201
1202/-- σ_0(120) = 16. -/
1203theorem sigma_zero_onehundredtwenty : sigma 0 120 = 16 := by native_decide
1204
1205/-- σ_1(840) = 2880. -/
1206theorem sigma_one_eighthundredforty : sigma 1 840 = 2880 := by native_decide
1207
1208/-- σ_0(840) = 32. -/
1209theorem sigma_zero_eighthundredforty : sigma 0 840 = 32 := by native_decide
1210
1211-- Note: ω(840) = 4 already exists as omega_eighthundredforty
1212
1213/-- rad(120) = 30 = 2×3×5. -/
1214theorem radical_onehundredtwenty : radical 120 = 30 := by native_decide
1215
1216/-- φ(840) = 192. -/
1217theorem totient_eighthundredforty : totient 840 = 192 := by native_decide
1218
1219/-! ### Sophie Germain primes (p and 2p+1 both prime) -/
1220
1221/-- 2 is a Sophie Germain prime (2 and 5 are both prime). -/
1222theorem sophie_germain_two : Prime 2 ∧ Prime (2 * 2 + 1) := by native_decide
1223
1224/-- 3 is a Sophie Germain prime (3 and 7 are both prime). -/
1225theorem sophie_germain_three : Prime 3 ∧ Prime (2 * 3 + 1) := by native_decide
1226
1227/-- 5 is a Sophie Germain prime (5 and 11 are both prime). -/
1228theorem sophie_germain_five : Prime 5 ∧ Prime (2 * 5 + 1) := by native_decide
1229
1230/-- 11 is a Sophie Germain prime (11 and 23 are both prime). -/
1231theorem sophie_germain_eleven : Prime 11 ∧ Prime (2 * 11 + 1) := by native_decide
1232
1233/-- 23 is a Sophie Germain prime (23 and 47 are both prime). -/
1234theorem sophie_germain_twentythree : Prime 23 ∧ Prime (2 * 23 + 1) := by native_decide
1235
1236/-- 29 is a Sophie Germain prime (29 and 59 are both prime). -/
1237theorem sophie_germain_twentynine : Prime 29 ∧ Prime (2 * 29 + 1) := by native_decide
1238
1239/-! ### Mersenne prime exponents (small) -/
1240
1241/-- 2^2 - 1 = 3 is a Mersenne prime. -/
1242theorem mersenne_two : Prime (2 ^ 2 - 1) := by native_decide
1243
1244/-- 2^3 - 1 = 7 is a Mersenne prime. -/
1245theorem mersenne_three : Prime (2 ^ 3 - 1) := by native_decide
1246
1247/-- 2^5 - 1 = 31 is a Mersenne prime. -/
1248theorem mersenne_five : Prime (2 ^ 5 - 1) := by native_decide
1249
1250/-- 2^7 - 1 = 127 is a Mersenne prime. -/
1251theorem mersenne_seven : Prime (2 ^ 7 - 1) := by native_decide
1252
1253/-! ### Fermat primes (2^(2^n) + 1) -/
1254
1255/-- F_0 = 2^(2^0) + 1 = 3 is a Fermat prime. -/
1256theorem fermat_zero : Prime (2 ^ (2 ^ 0) + 1) := by native_decide
1257
1258/-- F_1 = 2^(2^1) + 1 = 5 is a Fermat prime. -/
1259theorem fermat_one : Prime (2 ^ (2 ^ 1) + 1) := by native_decide
1260
1261/-- F_2 = 2^(2^2) + 1 = 17 is a Fermat prime. -/
1262theorem fermat_two : Prime (2 ^ (2 ^ 2) + 1) := by native_decide
1263
1264/-- F_3 = 2^(2^3) + 1 = 257 is a Fermat prime. -/
1265theorem fermat_three : Prime (2 ^ (2 ^ 3) + 1) := by native_decide
1266
1267/-- F_4 = 2^(2^4) + 1 = 65537 is a Fermat prime. -/
1268theorem fermat_four : Prime (2 ^ (2 ^ 4) + 1) := by native_decide
1269
1270/-! ### Cousin primes (differ by 4) -/
1271
1272/-- 3 and 7 are cousin primes. -/
1273theorem cousin_prime_three_seven : Prime 3 ∧ Prime 7 ∧ 7 = 3 + 4 := by native_decide
1274
1275/-- 7 and 11 are cousin primes. -/
1276theorem cousin_prime_seven_eleven : Prime 7 ∧ Prime 11 ∧ 11 = 7 + 4 := by native_decide
1277
1278/-- 13 and 17 are cousin primes. -/
1279theorem cousin_prime_thirteen_seventeen : Prime 13 ∧ Prime 17 ∧ 17 = 13 + 4 := by native_decide
1280
1281/-- 19 and 23 are cousin primes. -/
1282theorem cousin_prime_nineteen_twentythree : Prime 19 ∧ Prime 23 ∧ 23 = 19 + 4 := by native_decide
1283
1284/-- 37 and 41 are cousin primes. -/
1285theorem cousin_prime_thirtyseven_fortyone : Prime 37 ∧ Prime 41 ∧ 41 = 37 + 4 := by native_decide
1286
1287/-- 43 and 47 are cousin primes. -/
1288theorem cousin_prime_fortythree_fortyseven : Prime 43 ∧ Prime 47 ∧ 47 = 43 + 4 := by native_decide
1289
1290/-- 67 and 71 are cousin primes. -/
1291theorem cousin_prime_sixtyseven_seventyone : Prime 67 ∧ Prime 71 ∧ 71 = 67 + 4 := by native_decide
1292
1293/-! ### Sexy primes (differ by 6) -/
1294
1295/-- 5 and 11 are sexy primes. -/
1296theorem sexy_prime_five_eleven : Prime 5 ∧ Prime 11 ∧ 11 = 5 + 6 := by native_decide
1297
1298/-- 7 and 13 are sexy primes. -/
1299theorem sexy_prime_seven_thirteen : Prime 7 ∧ Prime 13 ∧ 13 = 7 + 6 := by native_decide
1300
1301/-- 11 and 17 are sexy primes. -/
1302theorem sexy_prime_eleven_seventeen : Prime 11 ∧ Prime 17 ∧ 17 = 11 + 6 := by native_decide
1303
1304/-- 13 and 19 are sexy primes. -/
1305theorem sexy_prime_thirteen_nineteen : Prime 13 ∧ Prime 19 ∧ 19 = 13 + 6 := by native_decide
1306
1307/-- 17 and 23 are sexy primes. -/
1308theorem sexy_prime_seventeen_twentythree : Prime 17 ∧ Prime 23 ∧ 23 = 17 + 6 := by native_decide
1309
1310/-- 23 and 29 are sexy primes. -/
1311theorem sexy_prime_twentythree_twentynine : Prime 23 ∧ Prime 29 ∧ 29 = 23 + 6 := by native_decide
1312
1313/-- 31 and 37 are sexy primes. -/
1314theorem sexy_prime_thirtyone_thirtyseven : Prime 31 ∧ Prime 37 ∧ 37 = 31 + 6 := by native_decide
1315
1316/-- 37 and 43 are sexy primes. -/
1317theorem sexy_prime_thirtyseven_fortythree : Prime 37 ∧ Prime 43 ∧ 43 = 37 + 6 := by native_decide
1318
1319/-! ### 210-related arithmetic functions (210 = 2×3×5×7 = primorial(4)) -/
1320
1321/-- 210 = 2 × 3 × 5 × 7 is the product of first 4 primes. -/
1322theorem twohundredten_eq_primorial_four : (210 : ℕ) = 2 * 3 * 5 * 7 := by native_decide
1323
1324/-- φ(210) = 48. -/
1325theorem totient_twohundredten : totient 210 = 48 := by native_decide
1326
1327/-- σ_0(210) = 16 (number of divisors). -/
1328theorem sigma_zero_twohundredten : sigma 0 210 = 16 := by native_decide
1329
1330/-- σ_1(210) = 576 (sum of divisors). -/
1331theorem sigma_one_twohundredten : sigma 1 210 = 576 := by native_decide
1332
1333/-- Ω(210) = 4 (since 210 = 2¹×3¹×5¹×7¹). -/
1334theorem bigOmega_twohundredten : bigOmega 210 = 4 := by native_decide
1335
1336/-- ω(210) = 4 (distinct prime factors: 2, 3, 5, 7). -/
1337theorem omega_twohundredten : omega 210 = 4 := by native_decide
1338
1339/-- rad(210) = 210 (squarefree). -/
1340theorem radical_twohundredten : radical 210 = 210 := by native_decide
1341
1342/-- λ(210) = 1 (Liouville, Ω = 4 is even). -/
1343theorem liouville_twohundredten : liouville 210 = 1 := by native_decide
1344
1345-- Note: μ(210) = 1 already exists as mobius_twohundredten
1346
1347/-! ### Additional small primes -/
1348
1349/-- 19 is prime. -/
1350theorem prime_nineteen : Prime 19 := by native_decide
1351
1352/-! ### Primorial values (product of first n primes) -/
1353
1354/-- primorial(1) = 2. -/
1355theorem primorial_one : (2 : ℕ) = 2 := rfl
1356
1357/-- primorial(2) = 2 × 3 = 6. -/
1358theorem primorial_two_eq : (6 : ℕ) = 2 * 3 := by native_decide
1359
1360/-- primorial(3) = 2 × 3 × 5 = 30. -/
1361theorem primorial_three_eq : (30 : ℕ) = 2 * 3 * 5 := by native_decide
1362
1363/-- primorial(4) = 2 × 3 × 5 × 7 = 210. -/
1364theorem primorial_four_eq : (210 : ℕ) = 2 * 3 * 5 * 7 := by native_decide
1365
1366/-- primorial(5) = 2 × 3 × 5 × 7 × 11 = 2310. -/
1367theorem primorial_five_eq : (2310 : ℕ) = 2 * 3 * 5 * 7 * 11 := by native_decide
1368
1369/-! ### More 2310-related (primorial(5)) -/
1370
1371/-- φ(2310) = 480. -/
1372theorem totient_twothousandthreehundredten : totient 2310 = 480 := by native_decide
1373
1374/-- ω(2310) = 5 (distinct prime factors: 2, 3, 5, 7, 11). -/
1375theorem omega_twothousandthreehundredten : omega 2310 = 5 := by native_decide
1376
1377/-- Ω(2310) = 5. -/
1378theorem bigOmega_twothousandthreehundredten : bigOmega 2310 = 5 := by native_decide
1379
1380/-- 2310 is squarefree. -/
1381theorem squarefree_twothousandthreehundredten : Squarefree 2310 := by native_decide
1382
1383/-- μ(2310) = -1 (squarefree with 5 prime factors). -/
1384theorem mobius_twothousandthreehundredten : mobius 2310 = -1 := by native_decide
1385
1386/-! ### Highly composite numbers -/
1387
1388/-- 12 is highly composite (has more divisors than any smaller positive integer). -/
1389theorem divisors_card_twelve_gt : ∀ n, 0 < n → n < 12 → (n : ℕ).divisors.card < (12 : ℕ).divisors.card := by
1390  intro n hn hlt
1391  interval_cases n <;> native_decide
1392
1393/-! ### More highly composite numbers -/
1394
1395/-- 60 is highly composite (has more divisors than any smaller positive integer). -/
1396theorem divisors_card_sixty_gt : ∀ n, 0 < n → n < 60 → (n : ℕ).divisors.card < (60 : ℕ).divisors.card := by
1397  intro n hn hlt
1398  interval_cases n <;> native_decide
1399
1400/-- 120 is highly composite (has more divisors than any smaller positive integer). -/
1401theorem divisors_card_onehundredtwenty_gt : ∀ n, 0 < n → n < 120 → (n : ℕ).divisors.card < (120 : ℕ).divisors.card := by
1402  intro n hn hlt
1403  interval_cases n <;> native_decide
1404
1405/-! ### Safe primes (p such that (p-1)/2 is also prime) -/
1406
1407/-- 5 is a safe prime: (5-1)/2 = 2 is prime. -/
1408theorem safe_prime_five : Prime 5 ∧ Prime ((5 - 1) / 2) := by native_decide
1409
1410/-- 7 is a safe prime: (7-1)/2 = 3 is prime. -/
1411theorem safe_prime_seven : Prime 7 ∧ Prime ((7 - 1) / 2) := by native_decide
1412
1413/-- 11 is a safe prime: (11-1)/2 = 5 is prime. -/
1414theorem safe_prime_eleven : Prime 11 ∧ Prime ((11 - 1) / 2) := by native_decide
1415
1416/-- 23 is a safe prime: (23-1)/2 = 11 is prime. -/
1417theorem safe_prime_twentythree : Prime 23 ∧ Prime ((23 - 1) / 2) := by native_decide
1418
1419/-- 47 is a safe prime: (47-1)/2 = 23 is prime. -/
1420theorem safe_prime_fortyseven : Prime 47 ∧ Prime ((47 - 1) / 2) := by native_decide
1421
1422/-- 59 is a safe prime: (59-1)/2 = 29 is prime. -/
1423theorem safe_prime_fiftynine : Prime 59 ∧ Prime ((59 - 1) / 2) := by native_decide
1424
1425/-- 83 is a safe prime: (83-1)/2 = 41 is prime. -/
1426theorem safe_prime_eightythree : Prime 83 ∧ Prime ((83 - 1) / 2) := by native_decide
1427
1428-- Note: 89 is NOT a safe prime since (89-1)/2 = 44 = 4×11 is composite
1429
1430/-- 107 is a safe prime: (107-1)/2 = 53 is prime. -/
1431theorem safe_prime_onehundredseven : Prime 107 ∧ Prime ((107 - 1) / 2) := by native_decide
1432
1433/-! ### Abundant numbers (σ_1(n) > 2n) -/
1434
1435/-- 12 is abundant: σ_1(12) = 28 > 24. -/
1436theorem abundant_twelve : sigma 1 12 > 2 * 12 := by native_decide
1437
1438/-- 18 is abundant: σ_1(18) = 39 > 36. -/
1439theorem abundant_eighteen : sigma 1 18 > 2 * 18 := by native_decide
1440
1441/-- 20 is abundant: σ_1(20) = 42 > 40. -/
1442theorem abundant_twenty : sigma 1 20 > 2 * 20 := by native_decide
1443
1444/-- 24 is abundant: σ_1(24) = 60 > 48. -/
1445theorem abundant_twentyfour : sigma 1 24 > 2 * 24 := by native_decide
1446
1447/-- 30 is abundant: σ_1(30) = 72 > 60. -/
1448theorem abundant_thirty : sigma 1 30 > 2 * 30 := by native_decide
1449
1450/-- 36 is abundant: σ_1(36) = 91 > 72. -/
1451theorem abundant_thirtysix : sigma 1 36 > 2 * 36 := by native_decide
1452
1453/-! ### Deficient numbers (σ_1(n) < 2n) -/
1454
1455/-- 1 is deficient: σ_1(1) = 1 < 2. -/
1456theorem deficient_one : sigma 1 1 < 2 * 1 := by native_decide
1457
1458/-- 2 is deficient: σ_1(2) = 3 < 4. -/
1459theorem deficient_two : sigma 1 2 < 2 * 2 := by native_decide
1460
1461/-- 3 is deficient: σ_1(3) = 4 < 6. -/
1462theorem deficient_three : sigma 1 3 < 2 * 3 := by native_decide
1463
1464/-- 4 is deficient: σ_1(4) = 7 < 8. -/
1465theorem deficient_four : sigma 1 4 < 2 * 4 := by native_decide
1466
1467/-- 5 is deficient: σ_1(5) = 6 < 10. -/
1468theorem deficient_five : sigma 1 5 < 2 * 5 := by native_decide
1469
1470/-- 7 is deficient: σ_1(7) = 8 < 14. -/
1471theorem deficient_seven : sigma 1 7 < 2 * 7 := by native_decide
1472
1473/-- 8 is deficient: σ_1(8) = 15 < 16. -/
1474theorem deficient_eight : sigma 1 8 < 2 * 8 := by native_decide
1475
1476/-- 9 is deficient: σ_1(9) = 13 < 18. -/
1477theorem deficient_nine : sigma 1 9 < 2 * 9 := by native_decide
1478
1479/-- 10 is deficient: σ_1(10) = 18 < 20. -/
1480theorem deficient_ten : sigma 1 10 < 2 * 10 := by native_decide
1481
1482/-- 11 is deficient (all primes are deficient). -/
1483theorem deficient_eleven : sigma 1 11 < 2 * 11 := by native_decide
1484
1485/-! ### Pythagorean primes (p ≡ 1 mod 4) — can be expressed as sum of two squares -/
1486
1487/-- 5 ≡ 1 (mod 4) is a Pythagorean prime. -/
1488theorem pythagorean_prime_five : Prime 5 ∧ 5 % 4 = 1 := by native_decide
1489
1490/-- 13 ≡ 1 (mod 4) is a Pythagorean prime. -/
1491theorem pythagorean_prime_thirteen : Prime 13 ∧ 13 % 4 = 1 := by native_decide
1492
1493/-- 17 ≡ 1 (mod 4) is a Pythagorean prime. -/
1494theorem pythagorean_prime_seventeen : Prime 17 ∧ 17 % 4 = 1 := by native_decide
1495
1496/-- 29 ≡ 1 (mod 4) is a Pythagorean prime. -/
1497theorem pythagorean_prime_twentynine : Prime 29 ∧ 29 % 4 = 1 := by native_decide
1498
1499/-- 37 ≡ 1 (mod 4) is a Pythagorean prime. -/
1500theorem pythagorean_prime_thirtyseven : Prime 37 ∧ 37 % 4 = 1 := by native_decide
1501
1502/-- 41 ≡ 1 (mod 4) is a Pythagorean prime. -/
1503theorem pythagorean_prime_fortyone : Prime 41 ∧ 41 % 4 = 1 := by native_decide
1504
1505/-- 53 ≡ 1 (mod 4) is a Pythagorean prime. -/
1506theorem pythagorean_prime_fiftythree : Prime 53 ∧ 53 % 4 = 1 := by native_decide
1507
1508/-- 61 ≡ 1 (mod 4) is a Pythagorean prime. -/
1509theorem pythagorean_prime_sixtyone : Prime 61 ∧ 61 % 4 = 1 := by native_decide
1510
1511/-- 73 ≡ 1 (mod 4) is a Pythagorean prime. -/
1512theorem pythagorean_prime_seventythree : Prime 73 ∧ 73 % 4 = 1 := by native_decide
1513
1514/-- 89 ≡ 1 (mod 4) is a Pythagorean prime. -/
1515theorem pythagorean_prime_eightynine : Prime 89 ∧ 89 % 4 = 1 := by native_decide
1516
1517/-- 97 ≡ 1 (mod 4) is a Pythagorean prime. -/
1518theorem pythagorean_prime_ninetyseven : Prime 97 ∧ 97 % 4 = 1 := by native_decide
1519
1520/-- 101 ≡ 1 (mod 4) is a Pythagorean prime. -/
1521theorem pythagorean_prime_onehundredone : Prime 101 ∧ 101 % 4 = 1 := by native_decide
1522
1523/-- 109 ≡ 1 (mod 4) is a Pythagorean prime. -/
1524theorem pythagorean_prime_onehundrednine : Prime 109 ∧ 109 % 4 = 1 := by native_decide
1525
1526/-- 113 ≡ 1 (mod 4) is a Pythagorean prime. -/
1527theorem pythagorean_prime_onehundredthirteen : Prime 113 ∧ 113 % 4 = 1 := by native_decide
1528
1529/-- 137 ≡ 1 (mod 4) is a Pythagorean prime (RS-relevant). -/
1530theorem pythagorean_prime_onehundredthirtyseven : Prime 137 ∧ 137 % 4 = 1 := by native_decide
1531
1532/-! ### Prime triplets (three primes with gaps ≤ 6) -/
1533
1534/-- (3, 5, 7) is a prime triplet. -/
1535theorem prime_triplet_three_five_seven : Prime 3 ∧ Prime 5 ∧ Prime 7 := by native_decide
1536
1537/-- (5, 7, 11) are three primes with gap (2, 4). -/
1538theorem prime_triplet_five_seven_eleven : Prime 5 ∧ Prime 7 ∧ Prime 11 := by native_decide
1539
1540/-- (7, 11, 13) are three primes with gap (4, 2). -/
1541theorem prime_triplet_seven_eleven_thirteen : Prime 7 ∧ Prime 11 ∧ Prime 13 := by native_decide
1542
1543/-- (11, 13, 17) are three primes with gap (2, 4). -/
1544theorem prime_triplet_eleven_thirteen_seventeen : Prime 11 ∧ Prime 13 ∧ Prime 17 := by native_decide
1545
1546/-- (13, 17, 19) are three primes with gap (4, 2). -/
1547theorem prime_triplet_thirteen_seventeen_nineteen : Prime 13 ∧ Prime 17 ∧ Prime 19 := by native_decide
1548
1549/-- (17, 19, 23) are three primes with gap (2, 4). -/
1550theorem prime_triplet_seventeen_nineteen_twentythree : Prime 17 ∧ Prime 19 ∧ Prime 23 := by native_decide
1551
1552/-- (37, 41, 43) are three primes with gap (4, 2). RS-relevant (37 is the beat numerator). -/
1553theorem prime_triplet_thirtyseven_fortyone_fortythree : Prime 37 ∧ Prime 41 ∧ Prime 43 := by native_decide
1554
1555/-! ### Sum of two squares representations for Pythagorean primes -/
1556
1557/-- 5 = 1² + 2². -/
1558theorem sum_of_squares_five : (5 : ℕ) = 1^2 + 2^2 := by native_decide
1559
1560/-- 13 = 2² + 3². -/
1561theorem sum_of_squares_thirteen : (13 : ℕ) = 2^2 + 3^2 := by native_decide
1562
1563/-- 17 = 1² + 4². -/
1564theorem sum_of_squares_seventeen : (17 : ℕ) = 1^2 + 4^2 := by native_decide
1565
1566/-- 29 = 2² + 5². -/
1567theorem sum_of_squares_twentynine : (29 : ℕ) = 2^2 + 5^2 := by native_decide
1568
1569/-- 37 = 1² + 6². -/
1570theorem sum_of_squares_thirtyseven : (37 : ℕ) = 1^2 + 6^2 := by native_decide
1571
1572/-- 41 = 4² + 5². -/
1573theorem sum_of_squares_fortyone : (41 : ℕ) = 4^2 + 5^2 := by native_decide
1574
1575/-- 53 = 2² + 7². -/
1576theorem sum_of_squares_fiftythree : (53 : ℕ) = 2^2 + 7^2 := by native_decide
1577
1578/-- 137 = 4² + 11² (RS-relevant). -/
1579theorem sum_of_squares_onehundredthirtyseven : (137 : ℕ) = 4^2 + 11^2 := by native_decide
1580
1581/-! ### Prime quadruplets (four primes in close cluster p, p+2, p+6, p+8) -/
1582
1583/-- (5, 7, 11, 13) is a prime quadruplet (gaps: 2, 4, 2). -/
1584theorem prime_quadruplet_five : Prime 5 ∧ Prime 7 ∧ Prime 11 ∧ Prime 13 := by native_decide
1585
1586/-- (11, 13, 17, 19) is a prime quadruplet (gaps: 2, 4, 2). -/
1587theorem prime_quadruplet_eleven : Prime 11 ∧ Prime 13 ∧ Prime 17 ∧ Prime 19 := by native_decide
1588
1589/-- (101, 103, 107, 109) is a prime quadruplet (gaps: 2, 4, 2). -/
1590theorem prime_quadruplet_onehundredone : Prime 101 ∧ Prime 103 ∧ Prime 107 ∧ Prime 109 := by native_decide
1591
1592/-- (191, 193, 197, 199) is a prime quadruplet (gaps: 2, 4, 2). -/
1593theorem prime_quadruplet_onehundredninetyone : Prime 191 ∧ Prime 193 ∧ Prime 197 ∧ Prime 199 := by native_decide
1594
1595/-! ### Primes p ≡ 3 (mod 4) — not expressible as sum of two squares -/
1596
1597/-- 3 ≡ 3 (mod 4). -/
1598theorem mod4_three_prime : Prime 3 ∧ 3 % 4 = 3 := by native_decide
1599
1600/-- 7 ≡ 3 (mod 4). -/
1601theorem mod4_seven_prime : Prime 7 ∧ 7 % 4 = 3 := by native_decide
1602
1603/-- 11 ≡ 3 (mod 4). -/
1604theorem mod4_eleven_prime : Prime 11 ∧ 11 % 4 = 3 := by native_decide
1605
1606/-- 19 ≡ 3 (mod 4). -/
1607theorem mod4_nineteen_prime : Prime 19 ∧ 19 % 4 = 3 := by native_decide
1608
1609/-- 23 ≡ 3 (mod 4). -/
1610theorem mod4_twentythree_prime : Prime 23 ∧ 23 % 4 = 3 := by native_decide
1611
1612/-- 31 ≡ 3 (mod 4). -/
1613theorem mod4_thirtyone_prime : Prime 31 ∧ 31 % 4 = 3 := by native_decide
1614
1615/-- 43 ≡ 3 (mod 4). -/
1616theorem mod4_fortythree_prime : Prime 43 ∧ 43 % 4 = 3 := by native_decide
1617
1618/-- 47 ≡ 3 (mod 4). -/
1619theorem mod4_fortyseven_prime : Prime 47 ∧ 47 % 4 = 3 := by native_decide
1620
1621/-- 59 ≡ 3 (mod 4). -/
1622theorem mod4_fiftynine_prime : Prime 59 ∧ 59 % 4 = 3 := by native_decide
1623
1624/-- 67 ≡ 3 (mod 4). -/
1625theorem mod4_sixtyseven_prime : Prime 67 ∧ 67 % 4 = 3 := by native_decide
1626
1627/-- 71 ≡ 3 (mod 4). -/
1628theorem mod4_seventyone_prime : Prime 71 ∧ 71 % 4 = 3 := by native_decide
1629
1630/-- 79 ≡ 3 (mod 4). -/
1631theorem mod4_seventynine_prime : Prime 79 ∧ 79 % 4 = 3 := by native_decide
1632
1633/-- 83 ≡ 3 (mod 4). -/
1634theorem mod4_eightythree_prime : Prime 83 ∧ 83 % 4 = 3 := by native_decide
1635
1636/-- 103 ≡ 3 (mod 4) (RS-relevant). -/
1637theorem mod4_onehundredthree_prime : Prime 103 ∧ 103 % 4 = 3 := by native_decide
1638
1639/-! ### σ_2 values (sum of squares of divisors) -/
1640
1641/-- σ_2(1) = 1. -/
1642theorem sigma_two_one : sigma 2 1 = 1 := by native_decide
1643
1644/-- σ_2(2) = 1 + 4 = 5. -/
1645theorem sigma_two_two : sigma 2 2 = 5 := by native_decide
1646
1647/-- σ_2(3) = 1 + 9 = 10. -/
1648theorem sigma_two_three : sigma 2 3 = 10 := by native_decide
1649
1650/-- σ_2(4) = 1 + 4 + 16 = 21. -/
1651theorem sigma_two_four : sigma 2 4 = 21 := by native_decide
1652
1653/-- σ_2(5) = 1 + 25 = 26. -/
1654theorem sigma_two_five : sigma 2 5 = 26 := by native_decide
1655
1656/-- σ_2(6) = 1 + 4 + 9 + 36 = 50. -/
1657theorem sigma_two_six : sigma 2 6 = 50 := by native_decide
1658
1659/-- σ_2(8) = 1 + 4 + 16 + 64 = 85. -/
1660theorem sigma_two_eight : sigma 2 8 = 85 := by native_decide
1661
1662/-- σ_2(10) = 1 + 4 + 25 + 100 = 130. -/
1663theorem sigma_two_ten : sigma 2 10 = 130 := by native_decide
1664
1665/-- σ_2(12) = 1 + 4 + 9 + 16 + 36 + 144 = 210. -/
1666theorem sigma_two_twelve : sigma 2 12 = 210 := by native_decide
1667
1668/-- σ_2(30) = 1300 (divisors: 1+4+9+25+36+100+225+900). -/
1669theorem sigma_two_thirty : sigma 2 30 = 1300 := by native_decide
1670
1671/-! ### More primeCounting values at round numbers -/
1672
1673/-- π(400) = 78. -/
1674theorem primeCounting_fourhundred : primeCounting 400 = 78 := by native_decide
1675
1676/-- π(600) = 109. -/
1677theorem primeCounting_sixhundred : primeCounting 600 = 109 := by native_decide
1678
1679/-- π(800) = 139. -/
1680theorem primeCounting_eighthundred : primeCounting 800 = 139 := by native_decide
1681
1682/-- π(900) = 154. -/
1683theorem primeCounting_ninehundred : primeCounting 900 = 154 := by native_decide
1684
1685/-! ### More sum of squares representations -/
1686
1687/-- 61 = 5² + 6². -/
1688theorem sum_of_squares_sixtyone : (61 : ℕ) = 5^2 + 6^2 := by native_decide
1689
1690/-- 73 = 3² + 8². -/
1691theorem sum_of_squares_seventythree : (73 : ℕ) = 3^2 + 8^2 := by native_decide
1692
1693/-- 89 = 5² + 8². -/
1694theorem sum_of_squares_eightynine : (89 : ℕ) = 5^2 + 8^2 := by native_decide
1695
1696/-- 97 = 4² + 9². -/
1697theorem sum_of_squares_ninetyseven : (97 : ℕ) = 4^2 + 9^2 := by native_decide
1698
1699/-- 101 = 1² + 10². -/
1700theorem sum_of_squares_onehundredone : (101 : ℕ) = 1^2 + 10^2 := by native_decide
1701
1702/-- 109 = 3² + 10². -/
1703theorem sum_of_squares_onehundrednine : (109 : ℕ) = 3^2 + 10^2 := by native_decide
1704
1705/-- 113 = 7² + 8². -/
1706theorem sum_of_squares_onehundredthirteen : (113 : ℕ) = 7^2 + 8^2 := by native_decide
1707
1708/-! ### Semiprimes (product of exactly two primes, counting multiplicity) -/
1709
1710/-- A number is semiprime if Ω(n) = 2. -/
1711def isSemiprime (n : ℕ) : Bool := bigOmega n = 2
1712
1713/-- 4 = 2² is semiprime. -/
1714theorem semiprime_four : isSemiprime 4 = true := by native_decide
1715
1716/-- 6 = 2 × 3 is semiprime. -/
1717theorem semiprime_six : isSemiprime 6 = true := by native_decide
1718
1719/-- 9 = 3² is semiprime. -/
1720theorem semiprime_nine : isSemiprime 9 = true := by native_decide
1721
1722/-- 10 = 2 × 5 is semiprime. -/
1723theorem semiprime_ten : isSemiprime 10 = true := by native_decide
1724
1725/-- 14 = 2 × 7 is semiprime. -/
1726theorem semiprime_fourteen : isSemiprime 14 = true := by native_decide
1727
1728/-- 15 = 3 × 5 is semiprime. -/
1729theorem semiprime_fifteen : isSemiprime 15 = true := by native_decide
1730
1731/-- 21 = 3 × 7 is semiprime. -/
1732theorem semiprime_twentyone : isSemiprime 21 = true := by native_decide
1733
1734/-- 22 = 2 × 11 is semiprime. -/
1735theorem semiprime_twentytwo : isSemiprime 22 = true := by native_decide
1736
1737/-- 25 = 5² is semiprime. -/
1738theorem semiprime_twentyfive : isSemiprime 25 = true := by native_decide
1739
1740/-- 26 = 2 × 13 is semiprime. -/
1741theorem semiprime_twentysix : isSemiprime 26 = true := by native_decide
1742
1743/-- 33 = 3 × 11 is semiprime. -/
1744theorem semiprime_thirtythree : isSemiprime 33 = true := by native_decide
1745
1746/-- 34 = 2 × 17 is semiprime. -/
1747theorem semiprime_thirtyfour : isSemiprime 34 = true := by native_decide
1748
1749/-- 35 = 5 × 7 is semiprime. -/
1750theorem semiprime_thirtyfive : isSemiprime 35 = true := by native_decide
1751
1752/-- 38 = 2 × 19 is semiprime. -/
1753theorem semiprime_thirtyeight : isSemiprime 38 = true := by native_decide
1754
1755/-- 39 = 3 × 13 is semiprime. -/
1756theorem semiprime_thirtynine : isSemiprime 39 = true := by native_decide
1757
1758/-- 49 = 7² is semiprime. -/
1759theorem semiprime_fortynine : isSemiprime 49 = true := by native_decide
1760
1761/-- 51 = 3 × 17 is semiprime. -/
1762theorem semiprime_fiftyone : isSemiprime 51 = true := by native_decide
1763
1764/-- 55 = 5 × 11 is semiprime. -/
1765theorem semiprime_fiftyfive : isSemiprime 55 = true := by native_decide
1766
1767/-- 57 = 3 × 19 is semiprime. -/
1768theorem semiprime_fiftyseven : isSemiprime 57 = true := by native_decide
1769
1770/-- 58 = 2 × 29 is semiprime. -/
1771theorem semiprime_fiftyeight : isSemiprime 58 = true := by native_decide
1772
1773/-- 62 = 2 × 31 is semiprime. -/
1774theorem semiprime_sixtytwo : isSemiprime 62 = true := by native_decide
1775
1776/-- 65 = 5 × 13 is semiprime. -/
1777theorem semiprime_sixtyfive : isSemiprime 65 = true := by native_decide
1778
1779/-- 74 = 2 × 37 is semiprime (RS-relevant: 37). -/
1780theorem semiprime_seventyfour : isSemiprime 74 = true := by native_decide
1781
1782/-- 77 = 7 × 11 is semiprime. -/
1783theorem semiprime_seventyseven : isSemiprime 77 = true := by native_decide
1784
1785/-- 85 = 5 × 17 is semiprime (RS-relevant: 17). -/
1786theorem semiprime_eightyfive : isSemiprime 85 = true := by native_decide
1787
1788/-- 91 = 7 × 13 is semiprime. -/
1789theorem semiprime_ninetyone : isSemiprime 91 = true := by native_decide
1790
1791/-- 95 = 5 × 19 is semiprime. -/
1792theorem semiprime_ninetyfive : isSemiprime 95 = true := by native_decide
1793
1794/-! ### Powers of 2 -/
1795
1796/-- 2^10 = 1024. -/
1797theorem two_pow_ten : (2 : ℕ) ^ 10 = 1024 := by native_decide
1798
1799/-- 2^12 = 4096. -/
1800theorem two_pow_twelve : (2 : ℕ) ^ 12 = 4096 := by native_decide
1801
1802/-- 2^16 = 65536. -/
1803theorem two_pow_sixteen : (2 : ℕ) ^ 16 = 65536 := by native_decide
1804
1805/-- 2^20 = 1048576. -/
1806theorem two_pow_twenty : (2 : ℕ) ^ 20 = 1048576 := by native_decide
1807
1808/-- 2^4 = 16. -/
1809theorem two_pow_four : (2 : ℕ) ^ 4 = 16 := by native_decide
1810
1811/-- 2^5 = 32. -/
1812theorem two_pow_five : (2 : ℕ) ^ 5 = 32 := by native_decide
1813
1814/-- 2^6 = 64. -/
1815theorem two_pow_six : (2 : ℕ) ^ 6 = 64 := by native_decide
1816
1817/-- 2^7 = 128. -/
1818theorem two_pow_seven : (2 : ℕ) ^ 7 = 128 := by native_decide
1819
1820/-- 2^8 = 256. -/
1821theorem two_pow_eight : (2 : ℕ) ^ 8 = 256 := by native_decide
1822
1823/-- 2^9 = 512. -/
1824theorem two_pow_nine : (2 : ℕ) ^ 9 = 512 := by native_decide
1825
1826/-! ### σ_3 values (sum of cubes of divisors) -/
1827
1828/-- σ_3(1) = 1. -/
1829theorem sigma_three_one : sigma 3 1 = 1 := by native_decide
1830
1831/-- σ_3(2) = 1 + 8 = 9. -/
1832theorem sigma_three_two : sigma 3 2 = 9 := by native_decide
1833
1834/-- σ_3(3) = 1 + 27 = 28. -/
1835theorem sigma_three_three : sigma 3 3 = 28 := by native_decide
1836
1837/-- σ_3(4) = 1 + 8 + 64 = 73. -/
1838theorem sigma_three_four : sigma 3 4 = 73 := by native_decide
1839
1840/-- σ_3(5) = 1 + 125 = 126. -/
1841theorem sigma_three_five : sigma 3 5 = 126 := by native_decide
1842
1843/-- σ_3(6) = 1 + 8 + 27 + 216 = 252. -/
1844theorem sigma_three_six : sigma 3 6 = 252 := by native_decide
1845
1846/-- σ_3(8) = 1 + 8 + 64 + 512 = 585. -/
1847theorem sigma_three_eight : sigma 3 8 = 585 := by native_decide
1848
1849/-- σ_3(10) = 1 + 8 + 125 + 1000 = 1134. -/
1850theorem sigma_three_ten : sigma 3 10 = 1134 := by native_decide
1851
1852/-- σ_3(12) = 2044. -/
1853theorem sigma_three_twelve : sigma 3 12 = 2044 := by native_decide
1854
1855/-! ### Mod 6 prime classification (all primes > 3 are ≡ 1 or 5 mod 6) -/
1856
1857/-- 7 ≡ 1 (mod 6). -/
1858theorem mod6_seven_prime : Prime 7 ∧ 7 % 6 = 1 := by native_decide
1859
1860/-- 13 ≡ 1 (mod 6). -/
1861theorem mod6_thirteen_prime : Prime 13 ∧ 13 % 6 = 1 := by native_decide
1862
1863/-- 19 ≡ 1 (mod 6). -/
1864theorem mod6_nineteen_prime : Prime 19 ∧ 19 % 6 = 1 := by native_decide
1865
1866/-- 31 ≡ 1 (mod 6). -/
1867theorem mod6_thirtyone_prime : Prime 31 ∧ 31 % 6 = 1 := by native_decide
1868
1869/-- 37 ≡ 1 (mod 6) (RS-relevant). -/
1870theorem mod6_thirtyseven_prime : Prime 37 ∧ 37 % 6 = 1 := by native_decide
1871
1872/-- 43 ≡ 1 (mod 6). -/
1873theorem mod6_fortythree_prime : Prime 43 ∧ 43 % 6 = 1 := by native_decide
1874
1875/-- 61 ≡ 1 (mod 6). -/
1876theorem mod6_sixtyone_prime : Prime 61 ∧ 61 % 6 = 1 := by native_decide
1877
1878/-- 67 ≡ 1 (mod 6). -/
1879theorem mod6_sixtyseven_prime : Prime 67 ∧ 67 % 6 = 1 := by native_decide
1880
1881/-- 73 ≡ 1 (mod 6). -/
1882theorem mod6_seventythree_prime : Prime 73 ∧ 73 % 6 = 1 := by native_decide
1883
1884/-- 79 ≡ 1 (mod 6). -/
1885theorem mod6_seventynine_prime : Prime 79 ∧ 79 % 6 = 1 := by native_decide
1886
1887/-- 97 ≡ 1 (mod 6). -/
1888theorem mod6_ninetyseven_prime : Prime 97 ∧ 97 % 6 = 1 := by native_decide
1889
1890/-- 103 ≡ 1 (mod 6) (RS-relevant). -/
1891theorem mod6_onehundredthree_prime : Prime 103 ∧ 103 % 6 = 1 := by native_decide
1892
1893/-- 5 ≡ 5 (mod 6). -/
1894theorem mod6_five_prime : Prime 5 ∧ 5 % 6 = 5 := by native_decide
1895
1896/-- 11 ≡ 5 (mod 6) (RS-relevant). -/
1897theorem mod6_eleven_prime : Prime 11 ∧ 11 % 6 = 5 := by native_decide
1898
1899/-- 17 ≡ 5 (mod 6) (RS-relevant). -/
1900theorem mod6_seventeen_prime : Prime 17 ∧ 17 % 6 = 5 := by native_decide
1901
1902/-- 23 ≡ 5 (mod 6). -/
1903theorem mod6_twentythree_prime : Prime 23 ∧ 23 % 6 = 5 := by native_decide
1904
1905/-- 29 ≡ 5 (mod 6). -/
1906theorem mod6_twentynine_prime : Prime 29 ∧ 29 % 6 = 5 := by native_decide
1907
1908/-- 41 ≡ 5 (mod 6). -/
1909theorem mod6_fortyone_prime : Prime 41 ∧ 41 % 6 = 5 := by native_decide
1910
1911/-- 47 ≡ 5 (mod 6). -/
1912theorem mod6_fortyseven_prime : Prime 47 ∧ 47 % 6 = 5 := by native_decide
1913
1914/-- 53 ≡ 5 (mod 6). -/
1915theorem mod6_fiftythree_prime : Prime 53 ∧ 53 % 6 = 5 := by native_decide
1916
1917/-- 59 ≡ 5 (mod 6). -/
1918theorem mod6_fiftynine_prime : Prime 59 ∧ 59 % 6 = 5 := by native_decide
1919
1920/-- 71 ≡ 5 (mod 6). -/
1921theorem mod6_seventyone_prime : Prime 71 ∧ 71 % 6 = 5 := by native_decide
1922
1923/-- 83 ≡ 5 (mod 6). -/
1924theorem mod6_eightythree_prime : Prime 83 ∧ 83 % 6 = 5 := by native_decide
1925
1926/-- 89 ≡ 5 (mod 6). -/
1927theorem mod6_eightynine_prime : Prime 89 ∧ 89 % 6 = 5 := by native_decide
1928
1929/-- 137 ≡ 5 (mod 6) (RS-relevant). -/
1930theorem mod6_onehundredthirtyseven_prime : Prime 137 ∧ 137 % 6 = 5 := by native_decide
1931
1932/-! ### Primes in the 200s -/
1933
1934/-- 211 is prime. -/
1935theorem prime_twohundredeleven : Prime 211 := by native_decide
1936
1937/-- 223 is prime. -/
1938theorem prime_twohundredtwentythree : Prime 223 := by native_decide
1939
1940/-- 227 is prime. -/
1941theorem prime_twohundredtwentyseven : Prime 227 := by native_decide
1942
1943/-- 229 is prime. -/
1944theorem prime_twohundredtwentynine : Prime 229 := by native_decide
1945
1946/-- 233 is prime. -/
1947theorem prime_twohundredthirtythree : Prime 233 := by native_decide
1948
1949/-- 239 is prime. -/
1950theorem prime_twohundredthirtynine : Prime 239 := by native_decide
1951
1952/-- 241 is prime. -/
1953theorem prime_twohundredfortyone : Prime 241 := by native_decide
1954
1955/-- 251 is prime. -/
1956theorem prime_twohundredfiftyone : Prime 251 := by native_decide
1957
1958/-- 257 is prime (Fermat prime F_3 = 2^8 + 1). -/
1959theorem prime_twohundredfiftyseven : Prime 257 := by native_decide
1960
1961/-- 263 is prime. -/
1962theorem prime_twohundredsixtythree : Prime 263 := by native_decide
1963
1964/-- 269 is prime. -/
1965theorem prime_twohundredsixtynine : Prime 269 := by native_decide
1966
1967/-- 271 is prime. -/
1968theorem prime_twohundredseventyone : Prime 271 := by native_decide
1969
1970/-- 277 is prime. -/
1971theorem prime_twohundredseventyseven : Prime 277 := by native_decide
1972
1973/-- 281 is prime. -/
1974theorem prime_twohundredeightyone : Prime 281 := by native_decide
1975
1976/-- 283 is prime. -/
1977theorem prime_twohundredeightythree : Prime 283 := by native_decide
1978
1979/-- 293 is prime. -/
1980theorem prime_twohundredninetythree : Prime 293 := by native_decide
1981
1982/-! ### Primes in the 300s -/
1983
1984/-- 307 is prime. -/
1985theorem prime_threehundredseven : Prime 307 := by native_decide
1986
1987/-- 311 is prime. -/
1988theorem prime_threehundredeleven : Prime 311 := by native_decide
1989
1990/-- 313 is prime. -/
1991theorem prime_threehundredthirteen : Prime 313 := by native_decide
1992
1993/-- 317 is prime. -/
1994theorem prime_threehundredseventeen : Prime 317 := by native_decide
1995
1996/-- 331 is prime. -/
1997theorem prime_threehundredthirtyone : Prime 331 := by native_decide
1998
1999/-- 337 is prime. -/
2000theorem prime_threehundredthirtyseven : Prime 337 := by native_decide
2001
2002/-- 347 is prime. -/
2003theorem prime_threehundredfortyseven : Prime 347 := by native_decide
2004
2005/-- 349 is prime. -/
2006theorem prime_threehundredfortynine : Prime 349 := by native_decide
2007
2008/-- 353 is prime. -/
2009theorem prime_threehundredfiftythree : Prime 353 := by native_decide
2010
2011/-- 359 is prime. -/
2012theorem prime_threehundredfiftynine : Prime 359 := by native_decide
2013
2014/-- 367 is prime. -/
2015theorem prime_threehundredsixtyseven : Prime 367 := by native_decide
2016
2017/-- 373 is prime. -/
2018theorem prime_threehundredseventythree : Prime 373 := by native_decide
2019
2020/-- 379 is prime. -/
2021theorem prime_threehundredseventynine : Prime 379 := by native_decide
2022
2023/-- 383 is prime. -/
2024theorem prime_threehundredeightythree : Prime 383 := by native_decide
2025
2026/-- 389 is prime. -/
2027theorem prime_threehundredeightynine : Prime 389 := by native_decide
2028
2029/-- 397 is prime. -/
2030theorem prime_threehundredninetyseven : Prime 397 := by native_decide
2031
2032/-! ### 3-almost primes (Ω(n) = 3) -/
2033
2034/-- A number is 3-almost prime if Ω(n) = 3. -/
2035def isThreeAlmostPrime (n : ℕ) : Bool := bigOmega n = 3
2036
2037/-- 8 = 2³ is 3-almost prime. -/
2038theorem three_almost_prime_eight : isThreeAlmostPrime 8 = true := by native_decide
2039
2040/-- 12 = 2² × 3 is 3-almost prime. -/
2041theorem three_almost_prime_twelve : isThreeAlmostPrime 12 = true := by native_decide
2042
2043/-- 18 = 2 × 3² is 3-almost prime. -/
2044theorem three_almost_prime_eighteen : isThreeAlmostPrime 18 = true := by native_decide
2045
2046/-- 20 = 2² × 5 is 3-almost prime. -/
2047theorem three_almost_prime_twenty : isThreeAlmostPrime 20 = true := by native_decide
2048
2049/-- 27 = 3³ is 3-almost prime. -/
2050theorem three_almost_prime_twentyseven : isThreeAlmostPrime 27 = true := by native_decide
2051
2052/-- 28 = 2² × 7 is 3-almost prime. -/
2053theorem three_almost_prime_twentyeight : isThreeAlmostPrime 28 = true := by native_decide
2054
2055/-- 30 = 2 × 3 × 5 is 3-almost prime. -/
2056theorem three_almost_prime_thirty : isThreeAlmostPrime 30 = true := by native_decide
2057
2058/-- 42 = 2 × 3 × 7 is 3-almost prime. -/
2059theorem three_almost_prime_fortytwo : isThreeAlmostPrime 42 = true := by native_decide
2060
2061/-- 44 = 2² × 11 is 3-almost prime. -/
2062theorem three_almost_prime_fortyfour : isThreeAlmostPrime 44 = true := by native_decide
2063
2064/-- 45 = 3² × 5 is 3-almost prime (RS constant). -/
2065theorem three_almost_prime_fortyfive : isThreeAlmostPrime 45 = true := by native_decide
2066
2067/-- 50 = 2 × 5² is 3-almost prime. -/
2068theorem three_almost_prime_fifty : isThreeAlmostPrime 50 = true := by native_decide
2069
2070/-- 52 = 2² × 13 is 3-almost prime. -/
2071theorem three_almost_prime_fiftytwo : isThreeAlmostPrime 52 = true := by native_decide
2072
2073/-- 63 = 3² × 7 is 3-almost prime. -/
2074theorem three_almost_prime_sixtythree : isThreeAlmostPrime 63 = true := by native_decide
2075
2076/-- 66 = 2 × 3 × 11 is 3-almost prime (RS-relevant: 11). -/
2077theorem three_almost_prime_sixtysix : isThreeAlmostPrime 66 = true := by native_decide
2078
2079/-- 68 = 2² × 17 is 3-almost prime (RS-relevant: 17). -/
2080theorem three_almost_prime_sixtyeight : isThreeAlmostPrime 68 = true := by native_decide
2081
2082/-- 70 = 2 × 5 × 7 is 3-almost prime. -/
2083theorem three_almost_prime_seventy : isThreeAlmostPrime 70 = true := by native_decide
2084
2085/-- 75 = 3 × 5² is 3-almost prime. -/
2086theorem three_almost_prime_seventyfive : isThreeAlmostPrime 75 = true := by native_decide
2087
2088/-- 76 = 2² × 19 is 3-almost prime. -/
2089theorem three_almost_prime_seventysix : isThreeAlmostPrime 76 = true := by native_decide
2090
2091/-! ### σ_2 and σ_3 for RS constants -/
2092
2093/-- σ_2(45) (RS constant). -/
2094theorem sigma_two_fortyfive : sigma 2 45 = 2366 := by native_decide
2095
2096-- Note: σ_2(360) and σ_3 values for large numbers require careful computation
2097-- Leaving those for future sessions when we can verify the exact values
2098
2099/-! ### Balanced primes ((p_{n-1} + p_{n+1})/2 = p_n) -/
2100
2101/-- 5 is a balanced prime: (3 + 7)/2 = 5. -/
2102theorem balanced_prime_five : Prime 5 ∧ Prime 3 ∧ Prime 7 ∧ (3 + 7) / 2 = 5 := by native_decide
2103
2104/-- 53 is a balanced prime: (47 + 59)/2 = 53. -/
2105theorem balanced_prime_fiftythree : Prime 53 ∧ Prime 47 ∧ Prime 59 ∧ (47 + 59) / 2 = 53 := by native_decide
2106
2107/-- 157 is a balanced prime: (151 + 163)/2 = 157. -/
2108theorem balanced_prime_onehundredfiftyseven : Prime 157 ∧ Prime 151 ∧ Prime 163 ∧ (151 + 163) / 2 = 157 := by native_decide
2109
2110/-- 173 is a balanced prime: (167 + 179)/2 = 173. -/
2111theorem balanced_prime_onehundredseventythree : Prime 173 ∧ Prime 167 ∧ Prime 179 ∧ (167 + 179) / 2 = 173 := by native_decide
2112
2113/-- 211 is a balanced prime: (199 + 223)/2 = 211. -/
2114theorem balanced_prime_twohundredeleven : Prime 211 ∧ Prime 199 ∧ Prime 223 ∧ (199 + 223) / 2 = 211 := by native_decide
2115
2116/-- 257 is a balanced prime: (251 + 263)/2 = 257 (Fermat prime F_3). -/
2117theorem balanced_prime_twohundredfiftyseven : Prime 257 ∧ Prime 251 ∧ Prime 263 ∧ (251 + 263) / 2 = 257 := by native_decide
2118
2119/-! ### Practical numbers (every m ≤ n is a sum of distinct divisors of n) -/
2120
2121/-- σ_1(1) = 1 ≥ 1, so 1 is practical. -/
2122theorem practical_one : sigma 1 1 ≥ 1 := by native_decide
2123
2124/-- σ_1(2) = 3 ≥ 2, so 2 is practical. -/
2125theorem practical_two : sigma 1 2 ≥ 2 := by native_decide
2126
2127/-- σ_1(4) = 7 ≥ 4, so 4 is practical. -/
2128theorem practical_four : sigma 1 4 ≥ 4 := by native_decide
2129
2130/-- σ_1(6) = 12 ≥ 6, so 6 is practical. -/
2131theorem practical_six : sigma 1 6 ≥ 6 := by native_decide
2132
2133/-- σ_1(8) = 15 ≥ 8, so 8 is practical. -/
2134theorem practical_eight : sigma 1 8 ≥ 8 := by native_decide
2135
2136/-- σ_1(12) = 28 ≥ 12, so 12 is practical. -/
2137theorem practical_twelve : sigma 1 12 ≥ 12 := by native_decide
2138
2139/-- σ_1(16) = 31 ≥ 16, so 16 is practical. -/
2140theorem practical_sixteen : sigma 1 16 ≥ 16 := by native_decide
2141
2142/-- σ_1(18) = 39 ≥ 18, so 18 is practical. -/
2143theorem practical_eighteen : sigma 1 18 ≥ 18 := by native_decide
2144
2145/-- σ_1(20) = 42 ≥ 20, so 20 is practical. -/
2146theorem practical_twenty : sigma 1 20 ≥ 20 := by native_decide
2147
2148/-- σ_1(24) = 60 ≥ 24, so 24 is practical. -/
2149theorem practical_twentyfour : sigma 1 24 ≥ 24 := by native_decide
2150
2151/-- σ_1(28) = 56 ≥ 28, so 28 is practical. -/
2152theorem practical_twentyeight : sigma 1 28 ≥ 28 := by native_decide
2153
2154/-- σ_1(30) = 72 ≥ 30, so 30 is practical. -/
2155theorem practical_thirty : sigma 1 30 ≥ 30 := by native_decide
2156
2157/-- σ_1(32) = 63 ≥ 32, so 32 is practical. -/
2158theorem practical_thirtytwo : sigma 1 32 ≥ 32 := by native_decide
2159
2160/-- σ_1(36) = 91 ≥ 36, so 36 is practical. -/
2161theorem practical_thirtysix : sigma 1 36 ≥ 36 := by native_decide
2162
2163/-! ### Primes in the 400s -/
2164
2165/-- 401 is prime. -/
2166theorem prime_fourhundredone : Prime 401 := by native_decide
2167
2168/-- 409 is prime. -/
2169theorem prime_fourhundrednine : Prime 409 := by native_decide
2170
2171/-- 419 is prime. -/
2172theorem prime_fourhundrednineteen : Prime 419 := by native_decide
2173
2174/-- 421 is prime. -/
2175theorem prime_fourhundredtwentyone : Prime 421 := by native_decide
2176
2177/-- 431 is prime. -/
2178theorem prime_fourhundredthirtyone : Prime 431 := by native_decide
2179
2180/-- 433 is prime. -/
2181theorem prime_fourhundredthirtythree : Prime 433 := by native_decide
2182
2183/-- 439 is prime. -/
2184theorem prime_fourhundredthirtynine : Prime 439 := by native_decide
2185
2186/-- 443 is prime. -/
2187theorem prime_fourhundredfortythree : Prime 443 := by native_decide
2188
2189/-- 449 is prime. -/
2190theorem prime_fourhundredfortynine : Prime 449 := by native_decide
2191
2192/-- 457 is prime. -/
2193theorem prime_fourhundredfiftyseven : Prime 457 := by native_decide
2194
2195/-- 461 is prime. -/
2196theorem prime_fourhundredsixtyone : Prime 461 := by native_decide
2197
2198/-- 463 is prime. -/
2199theorem prime_fourhundredsixtythree : Prime 463 := by native_decide
2200
2201/-- 467 is prime. -/
2202theorem prime_fourhundredsixtyseven : Prime 467 := by native_decide
2203
2204/-- 479 is prime. -/
2205theorem prime_fourhundredseventynine : Prime 479 := by native_decide
2206
2207/-- 487 is prime. -/
2208theorem prime_fourhundredeightyseven : Prime 487 := by native_decide
2209
2210/-- 491 is prime. -/
2211theorem prime_fourhundredninetyone : Prime 491 := by native_decide
2212
2213/-- 499 is prime. -/
2214theorem prime_fourhundredninetynine : Prime 499 := by native_decide
2215
2216/-! ### 4-almost primes (Ω(n) = 4) -/
2217
2218/-- A number is 4-almost prime if Ω(n) = 4. -/
2219def isFourAlmostPrime (n : ℕ) : Bool := bigOmega n = 4
2220
2221/-- 16 = 2⁴ is 4-almost prime. -/
2222theorem four_almost_prime_sixteen : isFourAlmostPrime 16 = true := by native_decide
2223
2224/-- 24 = 2³ × 3 is 4-almost prime. -/
2225theorem four_almost_prime_twentyfour : isFourAlmostPrime 24 = true := by native_decide
2226
2227/-- 36 = 2² × 3² is 4-almost prime. -/
2228theorem four_almost_prime_thirtysix : isFourAlmostPrime 36 = true := by native_decide
2229
2230/-- 40 = 2³ × 5 is 4-almost prime. -/
2231theorem four_almost_prime_forty : isFourAlmostPrime 40 = true := by native_decide
2232
2233/-- 54 = 2 × 3³ is 4-almost prime. -/
2234theorem four_almost_prime_fiftyfour : isFourAlmostPrime 54 = true := by native_decide
2235
2236/-- 56 = 2³ × 7 is 4-almost prime. -/
2237theorem four_almost_prime_fiftysix : isFourAlmostPrime 56 = true := by native_decide
2238
2239/-- 60 = 2² × 3 × 5 is 4-almost prime. -/
2240theorem four_almost_prime_sixty : isFourAlmostPrime 60 = true := by native_decide
2241
2242/-- 81 = 3⁴ is 4-almost prime. -/
2243theorem four_almost_prime_eightyone : isFourAlmostPrime 81 = true := by native_decide
2244
2245/-- 84 = 2² × 3 × 7 is 4-almost prime. -/
2246theorem four_almost_prime_eightyfour : isFourAlmostPrime 84 = true := by native_decide
2247
2248/-- 88 = 2³ × 11 is 4-almost prime (RS-relevant: 11). -/
2249theorem four_almost_prime_eightyeight : isFourAlmostPrime 88 = true := by native_decide
2250
2251/-- 90 = 2 × 3² × 5 is 4-almost prime. -/
2252theorem four_almost_prime_ninety : isFourAlmostPrime 90 = true := by native_decide
2253
2254/-- 100 = 2² × 5² is 4-almost prime. -/
2255theorem four_almost_prime_onehundred : isFourAlmostPrime 100 = true := by native_decide
2256
2257/-- 104 = 2³ × 13 is 4-almost prime. -/
2258theorem four_almost_prime_onehundredfour : isFourAlmostPrime 104 = true := by native_decide
2259
2260-- Note: 120 = 2³ × 3 × 5, Ω = 3 + 1 + 1 = 5, so 120 is 5-almost prime, not 4-almost prime
2261
2262/-- 126 = 2 × 3² × 7 is 4-almost prime. -/
2263theorem four_almost_prime_onehundredtwentysix : isFourAlmostPrime 126 = true := by native_decide
2264
2265/-- 132 = 2² × 3 × 11 is 4-almost prime (RS-relevant: 11). -/
2266theorem four_almost_prime_onehundredthirtytwo : isFourAlmostPrime 132 = true := by native_decide
2267
2268/-- 136 = 2³ × 17 is 4-almost prime (RS-relevant: 17). -/
2269theorem four_almost_prime_onehundredthirtysix : isFourAlmostPrime 136 = true := by native_decide
2270
2271/-- 140 = 2² × 5 × 7 is 4-almost prime. -/
2272theorem four_almost_prime_onehundredforty : isFourAlmostPrime 140 = true := by native_decide
2273
2274/-! ### Chen primes (p is prime and p+2 is prime or semiprime) -/
2275
2276/-- 2 is a Chen prime: 2+2 = 4 = 2² is semiprime. -/
2277theorem chen_prime_two : Prime 2 ∧ isSemiprime 4 = true := by native_decide
2278
2279/-- 3 is a Chen prime: 3+2 = 5 is prime. -/
2280theorem chen_prime_three : Prime 3 ∧ Prime 5 := by native_decide
2281
2282/-- 5 is a Chen prime: 5+2 = 7 is prime. -/
2283theorem chen_prime_five : Prime 5 ∧ Prime 7 := by native_decide
2284
2285/-- 7 is a Chen prime: 7+2 = 9 = 3² is semiprime. -/
2286theorem chen_prime_seven : Prime 7 ∧ isSemiprime 9 = true := by native_decide
2287
2288/-- 11 is a Chen prime: 11+2 = 13 is prime (RS-relevant). -/
2289theorem chen_prime_eleven : Prime 11 ∧ Prime 13 := by native_decide
2290
2291/-- 13 is a Chen prime: 13+2 = 15 = 3×5 is semiprime. -/
2292theorem chen_prime_thirteen : Prime 13 ∧ isSemiprime 15 = true := by native_decide
2293
2294/-- 17 is a Chen prime: 17+2 = 19 is prime (RS-relevant). -/
2295theorem chen_prime_seventeen : Prime 17 ∧ Prime 19 := by native_decide
2296
2297/-- 19 is a Chen prime: 19+2 = 21 = 3×7 is semiprime. -/
2298theorem chen_prime_nineteen : Prime 19 ∧ isSemiprime 21 = true := by native_decide
2299
2300/-- 23 is a Chen prime: 23+2 = 25 = 5² is semiprime. -/
2301theorem chen_prime_twentythree : Prime 23 ∧ isSemiprime 25 = true := by native_decide
2302
2303/-- 29 is a Chen prime: 29+2 = 31 is prime. -/
2304theorem chen_prime_twentynine : Prime 29 ∧ Prime 31 := by native_decide
2305
2306/-- 31 is a Chen prime: 31+2 = 33 = 3×11 is semiprime. -/
2307theorem chen_prime_thirtyone : Prime 31 ∧ isSemiprime 33 = true := by native_decide
2308
2309/-- 37 is a Chen prime: 37+2 = 39 = 3×13 is semiprime (RS-relevant). -/
2310theorem chen_prime_thirtyseven : Prime 37 ∧ isSemiprime 39 = true := by native_decide
2311
2312/-- 41 is a Chen prime: 41+2 = 43 is prime. -/
2313theorem chen_prime_fortyone : Prime 41 ∧ Prime 43 := by native_decide
2314
2315/-- 47 is a Chen prime: 47+2 = 49 = 7² is semiprime. -/
2316theorem chen_prime_fortyseven : Prime 47 ∧ isSemiprime 49 = true := by native_decide
2317
2318/-! ### Emirps (primes that form different primes when reversed) -/
2319
2320/-- 13 reversed is 31, both prime (13 is an emirp). -/
2321theorem emirp_thirteen : Prime 13 ∧ Prime 31 ∧ 13 ≠ 31 := by native_decide
2322
2323/-- 17 reversed is 71, both prime (17 is an emirp, RS-relevant). -/
2324theorem emirp_seventeen : Prime 17 ∧ Prime 71 ∧ 17 ≠ 71 := by native_decide
2325
2326/-- 31 reversed is 13, both prime (31 is an emirp). -/
2327theorem emirp_thirtyone : Prime 31 ∧ Prime 13 ∧ 31 ≠ 13 := by native_decide
2328
2329/-- 37 reversed is 73, both prime (37 is an emirp, RS-relevant). -/
2330theorem emirp_thirtyseven : Prime 37 ∧ Prime 73 ∧ 37 ≠ 73 := by native_decide
2331
2332/-- 71 reversed is 17, both prime (71 is an emirp). -/
2333theorem emirp_seventyone : Prime 71 ∧ Prime 17 ∧ 71 ≠ 17 := by native_decide
2334
2335/-- 73 reversed is 37, both prime (73 is an emirp). -/
2336theorem emirp_seventythree : Prime 73 ∧ Prime 37 ∧ 73 ≠ 37 := by native_decide
2337
2338/-- 79 reversed is 97, both prime (79 is an emirp). -/
2339theorem emirp_seventynine : Prime 79 ∧ Prime 97 ∧ 79 ≠ 97 := by native_decide
2340
2341/-- 97 reversed is 79, both prime (97 is an emirp). -/
2342theorem emirp_ninetyseven : Prime 97 ∧ Prime 79 ∧ 97 ≠ 79 := by native_decide
2343
2344/-- 107 reversed is 701, both prime (107 is an emirp). -/
2345theorem emirp_onehundredseven : Prime 107 ∧ Prime 701 ∧ 107 ≠ 701 := by native_decide
2346
2347/-- 113 reversed is 311, both prime (113 is an emirp). -/
2348theorem emirp_onehundredthirteen : Prime 113 ∧ Prime 311 ∧ 113 ≠ 311 := by native_decide
2349
2350/-- 149 reversed is 941, both prime (149 is an emirp). -/
2351theorem emirp_onehundredfortynine : Prime 149 ∧ Prime 941 ∧ 149 ≠ 941 := by native_decide
2352
2353/-- 157 reversed is 751, both prime (157 is an emirp). -/
2354theorem emirp_onehundredfiftyseven : Prime 157 ∧ Prime 751 ∧ 157 ≠ 751 := by native_decide
2355
2356/-! ### Repunit-related primes -/
2357
2358/-- R_2 = 11 is a repunit prime. -/
2359theorem repunit_prime_two : Prime 11 ∧ 11 = (10^2 - 1) / 9 := by native_decide
2360
2361/-- R_19 component: 19 is prime (indexes repunit R_19 which is also prime). -/
2362theorem repunit_index_nineteen : Prime 19 := by native_decide
2363
2364/-- R_23 component: 23 is prime (indexes repunit R_23 which is also prime). -/
2365theorem repunit_index_twentythree : Prime 23 := by native_decide
2366
2367/-- 111 = 3 × 37 is not prime (R_3 factors as 3 × 37, RS-relevant: 37). -/
2368theorem repunit_three_composite : ¬ Prime 111 ∧ 111 = 3 * 37 := by native_decide
2369
2370/-- 1111 = 11 × 101 is not prime (R_4 factors). -/
2371theorem repunit_four_composite : ¬ Prime 1111 ∧ 1111 = 11 * 101 := by native_decide
2372
2373/-- 11111 = 41 × 271 is not prime (R_5 factors). -/
2374theorem repunit_five_composite : ¬ Prime 11111 ∧ 11111 = 41 * 271 := by native_decide
2375
2376/-! ### Wieferich prime candidates -/
2377
2378/-- 1093 is prime (first Wieferich prime). -/
2379theorem prime_onethousandninetythree : Prime 1093 := by native_decide
2380
2381/-- 3511 is prime (second known Wieferich prime). -/
2382theorem prime_threethousandfiveeleven : Prime 3511 := by native_decide
2383
2384-- Note: primeCounting for values > 1000 requires careful verification
2385-- Leaving larger primeCounting values for future sessions
2386
2387/-! ### Primes in the 500s -/
2388
2389/-- 503 is prime. -/
2390theorem prime_fivehundredthree : Prime 503 := by native_decide
2391
2392/-- 509 is prime. -/
2393theorem prime_fivehundrednine : Prime 509 := by native_decide
2394
2395/-- 521 is prime. -/
2396theorem prime_fivehundredtwentyone : Prime 521 := by native_decide
2397
2398/-- 523 is prime. -/
2399theorem prime_fivehundredtwentythree : Prime 523 := by native_decide
2400
2401/-- 541 is prime. -/
2402theorem prime_fivehundredfortyone : Prime 541 := by native_decide
2403
2404/-- 547 is prime. -/
2405theorem prime_fivehundredfortyseven : Prime 547 := by native_decide
2406
2407/-- 557 is prime. -/
2408theorem prime_fivehundredfiftyseven : Prime 557 := by native_decide
2409
2410/-- 563 is prime (Wilson prime). -/
2411theorem prime_fivehundredsixtythree : Prime 563 := by native_decide
2412
2413/-- 569 is prime. -/
2414theorem prime_fivehundredsixtynine : Prime 569 := by native_decide
2415
2416/-- 571 is prime. -/
2417theorem prime_fivehundredseventyone : Prime 571 := by native_decide
2418
2419/-- 577 is prime. -/
2420theorem prime_fivehundredseventyseven : Prime 577 := by native_decide
2421
2422/-- 587 is prime. -/
2423theorem prime_fivehundredeightyseven : Prime 587 := by native_decide
2424
2425/-- 593 is prime. -/
2426theorem prime_fivehundredninetythree : Prime 593 := by native_decide
2427
2428/-- 599 is prime. -/
2429theorem prime_fivehundredninetynine : Prime 599 := by native_decide
2430
2431/-! ### 5-almost primes (Ω(n) = 5) -/
2432
2433/-- A number is 5-almost prime if Ω(n) = 5. -/
2434def isFiveAlmostPrime (n : ℕ) : Bool := bigOmega n = 5
2435
2436/-- 32 = 2⁵ is 5-almost prime. -/
2437theorem five_almost_prime_thirtytwo : isFiveAlmostPrime 32 = true := by native_decide
2438
2439/-- 48 = 2⁴ × 3 is 5-almost prime. -/
2440theorem five_almost_prime_fortyeight : isFiveAlmostPrime 48 = true := by native_decide
2441
2442/-- 72 = 2³ × 3² is 5-almost prime. -/
2443theorem five_almost_prime_seventytwo : isFiveAlmostPrime 72 = true := by native_decide
2444
2445/-- 80 = 2⁴ × 5 is 5-almost prime. -/
2446theorem five_almost_prime_eighty : isFiveAlmostPrime 80 = true := by native_decide
2447
2448/-- 108 = 2² × 3³ is 5-almost prime. -/
2449theorem five_almost_prime_onehundredeight : isFiveAlmostPrime 108 = true := by native_decide
2450
2451/-- 112 = 2⁴ × 7 is 5-almost prime. -/
2452theorem five_almost_prime_onehundredtwelve : isFiveAlmostPrime 112 = true := by native_decide
2453
2454/-- 120 = 2³ × 3 × 5 is 5-almost prime (RS-relevant). -/
2455theorem five_almost_prime_onehundredtwenty : isFiveAlmostPrime 120 = true := by native_decide
2456
2457/-- 162 = 2 × 3⁴ is 5-almost prime. -/
2458theorem five_almost_prime_onehundredsixtytwo : isFiveAlmostPrime 162 = true := by native_decide
2459
2460/-- 176 = 2⁴ × 11 is 5-almost prime (RS-relevant: 11). -/
2461theorem five_almost_prime_onehundredseventysix : isFiveAlmostPrime 176 = true := by native_decide
2462
2463/-- 180 = 2² × 3² × 5 is 5-almost prime. -/
2464theorem five_almost_prime_onehundredeighty : isFiveAlmostPrime 180 = true := by native_decide
2465
2466/-- 200 = 2³ × 5² is 5-almost prime. -/
2467theorem five_almost_prime_twohundred : isFiveAlmostPrime 200 = true := by native_decide
2468
2469/-- 208 = 2⁴ × 13 is 5-almost prime. -/
2470theorem five_almost_prime_twohundredeight : isFiveAlmostPrime 208 = true := by native_decide
2471
2472-- Note: 240 = 2⁴ × 3 × 5, Ω = 4 + 1 + 1 = 6, so 240 is 6-almost prime, not 5-almost prime
2473
2474/-- 243 = 3⁵ is 5-almost prime. -/
2475theorem five_almost_prime_twohundredfortythree : isFiveAlmostPrime 243 = true := by native_decide
2476
2477/-- 272 = 2⁴ × 17 is 5-almost prime (RS-relevant: 17). -/
2478theorem five_almost_prime_twohundredseventytwo : isFiveAlmostPrime 272 = true := by native_decide
2479
2480/-! ### Palindromic primes -/
2481
2482/-- 2 is a palindromic prime (single digit). -/
2483theorem palindromic_prime_two : Prime 2 := by native_decide
2484
2485/-- 3 is a palindromic prime (single digit). -/
2486theorem palindromic_prime_three : Prime 3 := by native_decide
2487
2488/-- 5 is a palindromic prime (single digit). -/
2489theorem palindromic_prime_five : Prime 5 := by native_decide
2490
2491/-- 7 is a palindromic prime (single digit). -/
2492theorem palindromic_prime_seven : Prime 7 := by native_decide
2493
2494/-- 11 is a palindromic prime (RS-relevant). -/
2495theorem palindromic_prime_eleven : Prime 11 := by native_decide
2496
2497/-- 101 is a palindromic prime. -/
2498theorem palindromic_prime_onehundredone : Prime 101 := by native_decide
2499
2500/-- 131 is a palindromic prime. -/
2501theorem palindromic_prime_onehundredthirtyone : Prime 131 := by native_decide
2502
2503/-- 151 is a palindromic prime. -/
2504theorem palindromic_prime_onehundredfiftyone : Prime 151 := by native_decide
2505
2506/-- 181 is a palindromic prime. -/
2507theorem palindromic_prime_onehundredeightyone : Prime 181 := by native_decide
2508
2509/-- 191 is a palindromic prime. -/
2510theorem palindromic_prime_onehundredninetyone : Prime 191 := by native_decide
2511
2512/-- 313 is a palindromic prime. -/
2513theorem palindromic_prime_threehundredthirteen : Prime 313 := by native_decide
2514
2515/-- 353 is a palindromic prime. -/
2516theorem palindromic_prime_threehundredfiftythree : Prime 353 := by native_decide
2517
2518/-- 373 is a palindromic prime. -/
2519theorem palindromic_prime_threehundredseventythree : Prime 373 := by native_decide
2520
2521/-- 383 is a palindromic prime. -/
2522theorem palindromic_prime_threehundredeightythree : Prime 383 := by native_decide
2523
2524/-- 727 is a palindromic prime. -/
2525theorem palindromic_prime_sevenhundredtwentyseven : Prime 727 := by native_decide
2526
2527/-- 757 is a palindromic prime. -/
2528theorem palindromic_prime_sevenhundredfiftyseven : Prime 757 := by native_decide
2529
2530/-- 787 is a palindromic prime. -/
2531theorem palindromic_prime_sevenhundredeightyseven : Prime 787 := by native_decide
2532
2533/-- 797 is a palindromic prime. -/
2534theorem palindromic_prime_sevenhundredninetyseven : Prime 797 := by native_decide
2535
2536/-! ### Strong primes (p > (p_prev + p_next)/2) -/
2537
2538/-- 11 is a strong prime: 11 > (7 + 13)/2 = 10. -/
2539theorem strong_prime_eleven : Prime 11 ∧ Prime 7 ∧ Prime 13 ∧ 11 > (7 + 13) / 2 := by native_decide
2540
2541/-- 17 is a strong prime: 17 > (13 + 19)/2 = 16 (RS-relevant). -/
2542theorem strong_prime_seventeen : Prime 17 ∧ Prime 13 ∧ Prime 19 ∧ 17 > (13 + 19) / 2 := by native_decide
2543
2544/-- 29 is a strong prime: 29 > (23 + 31)/2 = 27. -/
2545theorem strong_prime_twentynine : Prime 29 ∧ Prime 23 ∧ Prime 31 ∧ 29 > (23 + 31) / 2 := by native_decide
2546
2547/-- 37 is a strong prime: 37 > (31 + 41)/2 = 36 (RS-relevant). -/
2548theorem strong_prime_thirtyseven : Prime 37 ∧ Prime 31 ∧ Prime 41 ∧ 37 > (31 + 41) / 2 := by native_decide
2549
2550/-- 41 is a strong prime: 41 > (37 + 43)/2 = 40. -/
2551theorem strong_prime_fortyone : Prime 41 ∧ Prime 37 ∧ Prime 43 ∧ 41 > (37 + 43) / 2 := by native_decide
2552
2553/-- 59 is a strong prime: 59 > (53 + 61)/2 = 57. -/
2554theorem strong_prime_fiftynine : Prime 59 ∧ Prime 53 ∧ Prime 61 ∧ 59 > (53 + 61) / 2 := by native_decide
2555
2556/-- 67 is a strong prime: 67 > (61 + 71)/2 = 66. -/
2557theorem strong_prime_sixtyseven : Prime 67 ∧ Prime 61 ∧ Prime 71 ∧ 67 > (61 + 71) / 2 := by native_decide
2558
2559/-- 71 is a strong prime: 71 > (67 + 73)/2 = 70. -/
2560theorem strong_prime_seventyone : Prime 71 ∧ Prime 67 ∧ Prime 73 ∧ 71 > (67 + 73) / 2 := by native_decide
2561
2562/-- 79 is a strong prime: 79 > (73 + 83)/2 = 78. -/
2563theorem strong_prime_seventynine : Prime 79 ∧ Prime 73 ∧ Prime 83 ∧ 79 > (73 + 83) / 2 := by native_decide
2564
2565/-- 97 is a strong prime: 97 > (89 + 101)/2 = 95. -/
2566theorem strong_prime_ninetyseven : Prime 97 ∧ Prime 89 ∧ Prime 101 ∧ 97 > (89 + 101) / 2 := by native_decide
2567
2568/-- 101 is a strong prime: 101 > (97 + 103)/2 = 100. -/
2569theorem strong_prime_onehundredone : Prime 101 ∧ Prime 97 ∧ Prime 103 ∧ 101 > (97 + 103) / 2 := by native_decide
2570
2571/-- 107 is a strong prime: 107 > (103 + 109)/2 = 106. -/
2572theorem strong_prime_onehundredseven : Prime 107 ∧ Prime 103 ∧ Prime 109 ∧ 107 > (103 + 109) / 2 := by native_decide
2573
2574/-! ### More twin prime pairs -/
2575
2576/-- (101, 103) is a twin prime pair. -/
2577theorem twin_prime_onehundredone_onehundredthree : Prime 101 ∧ Prime 103 ∧ 103 = 101 + 2 := by native_decide
2578
2579/-- (107, 109) is a twin prime pair. -/
2580theorem twin_prime_onehundredseven_onehundrednine : Prime 107 ∧ Prime 109 ∧ 109 = 107 + 2 := by native_decide
2581
2582/-- (137, 139) is a twin prime pair (RS-relevant: 137). -/
2583theorem twin_prime_onehundredthirtyseven_onehundredthirtynine : Prime 137 ∧ Prime 139 ∧ 139 = 137 + 2 := by native_decide
2584
2585/-- (149, 151) is a twin prime pair. -/
2586theorem twin_prime_onehundredfortynine_onehundredfiftyone : Prime 149 ∧ Prime 151 ∧ 151 = 149 + 2 := by native_decide
2587
2588/-- (179, 181) is a twin prime pair. -/
2589theorem twin_prime_onehundredseventynine_onehundredeightyone : Prime 179 ∧ Prime 181 ∧ 181 = 179 + 2 := by native_decide
2590
2591/-- (191, 193) is a twin prime pair. -/
2592theorem twin_prime_onehundredninetyone_onehundredninetythree : Prime 191 ∧ Prime 193 ∧ 193 = 191 + 2 := by native_decide
2593
2594/-- (197, 199) is a twin prime pair. -/
2595theorem twin_prime_onehundredninetyseven_onehundredninetynine : Prime 197 ∧ Prime 199 ∧ 199 = 197 + 2 := by native_decide
2596
2597/-- (227, 229) is a twin prime pair. -/
2598theorem twin_prime_twohundredtwentyseven_twohundredtwentynine : Prime 227 ∧ Prime 229 ∧ 229 = 227 + 2 := by native_decide
2599
2600/-- (239, 241) is a twin prime pair. -/
2601theorem twin_prime_twohundredthirtynine_twohundredfortyone : Prime 239 ∧ Prime 241 ∧ 241 = 239 + 2 := by native_decide
2602
2603/-- (269, 271) is a twin prime pair. -/
2604theorem twin_prime_twohundredsixtynine_twohundredseventyone : Prime 269 ∧ Prime 271 ∧ 271 = 269 + 2 := by native_decide
2605
2606/-- (281, 283) is a twin prime pair. -/
2607theorem twin_prime_twohundredeightyone_twohundredeightythree : Prime 281 ∧ Prime 283 ∧ 283 = 281 + 2 := by native_decide
2608
2609/-- (311, 313) is a twin prime pair. -/
2610theorem twin_prime_threehundredeleven_threehundredthirteen : Prime 311 ∧ Prime 313 ∧ 313 = 311 + 2 := by native_decide
2611
2612/-- (347, 349) is a twin prime pair. -/
2613theorem twin_prime_threehundredfortyseven_threehundredfortynine : Prime 347 ∧ Prime 349 ∧ 349 = 347 + 2 := by native_decide
2614
2615/-- (419, 421) is a twin prime pair. -/
2616theorem twin_prime_fourhundrednineteen_fourhundredtwentyone : Prime 419 ∧ Prime 421 ∧ 421 = 419 + 2 := by native_decide
2617
2618/-- (431, 433) is a twin prime pair. -/
2619theorem twin_prime_fourhundredthirtyone_fourhundredthirtythree : Prime 431 ∧ Prime 433 ∧ 433 = 431 + 2 := by native_decide
2620
2621/-- (461, 463) is a twin prime pair. -/
2622theorem twin_prime_fourhundredsixtyone_fourhundredsixtythree : Prime 461 ∧ Prime 463 ∧ 463 = 461 + 2 := by native_decide
2623
2624/-! ### Primes in the 600s -/
2625
2626/-- 601 is prime. -/
2627theorem prime_sixhundredone : Prime 601 := by native_decide
2628
2629/-- 607 is prime. -/
2630theorem prime_sixhundredseven : Prime 607 := by native_decide
2631
2632/-- 613 is prime. -/
2633theorem prime_sixhundredthirteen : Prime 613 := by native_decide
2634
2635/-- 617 is prime. -/
2636theorem prime_sixhundredseventeen : Prime 617 := by native_decide
2637
2638/-- 619 is prime. -/
2639theorem prime_sixhundrednineteen : Prime 619 := by native_decide
2640
2641/-- 631 is prime. -/
2642theorem prime_sixhundredthirtyone : Prime 631 := by native_decide
2643
2644/-- 641 is prime (Fermat prime related: divides F₅). -/
2645theorem prime_sixhundredfortyone : Prime 641 := by native_decide
2646
2647/-- 643 is prime. -/
2648theorem prime_sixhundredfortythree : Prime 643 := by native_decide
2649
2650/-- 647 is prime. -/
2651theorem prime_sixhundredfortyseven : Prime 647 := by native_decide
2652
2653/-- 653 is prime. -/
2654theorem prime_sixhundredfiftythree : Prime 653 := by native_decide
2655
2656/-- 659 is prime. -/
2657theorem prime_sixhundredfiftynine : Prime 659 := by native_decide
2658
2659/-- 661 is prime. -/
2660theorem prime_sixhundredsixtyone : Prime 661 := by native_decide
2661
2662/-- 673 is prime. -/
2663theorem prime_sixhundredseventythree : Prime 673 := by native_decide
2664
2665/-- 677 is prime. -/
2666theorem prime_sixhundredseventyseven : Prime 677 := by native_decide
2667
2668/-- 683 is prime. -/
2669theorem prime_sixhundredeightythree : Prime 683 := by native_decide
2670
2671/-- 691 is prime. -/
2672theorem prime_sixhundredninetyone : Prime 691 := by native_decide
2673
2674/-! ### 6-almost primes (Ω(n) = 6) -/
2675
2676/-- A number is 6-almost prime if Ω(n) = 6. -/
2677def isSixAlmostPrime (n : ℕ) : Bool := bigOmega n = 6
2678
2679/-- 64 = 2⁶ is 6-almost prime. -/
2680theorem six_almost_prime_sixtyfour : isSixAlmostPrime 64 = true := by native_decide
2681
2682/-- 96 = 2⁵ × 3 is 6-almost prime. -/
2683theorem six_almost_prime_ninetysix : isSixAlmostPrime 96 = true := by native_decide
2684
2685/-- 144 = 2⁴ × 3² is 6-almost prime. -/
2686theorem six_almost_prime_onehundredfortyfour : isSixAlmostPrime 144 = true := by native_decide
2687
2688/-- 160 = 2⁵ × 5 is 6-almost prime. -/
2689theorem six_almost_prime_onehundredsixty : isSixAlmostPrime 160 = true := by native_decide
2690
2691/-- 216 = 2³ × 3³ is 6-almost prime. -/
2692theorem six_almost_prime_twohundredsixteen : isSixAlmostPrime 216 = true := by native_decide
2693
2694/-- 224 = 2⁵ × 7 is 6-almost prime. -/
2695theorem six_almost_prime_twohundredtwentyfour : isSixAlmostPrime 224 = true := by native_decide
2696
2697/-- 240 = 2⁴ × 3 × 5 is 6-almost prime (RS-relevant). -/
2698theorem six_almost_prime_twohundredforty : isSixAlmostPrime 240 = true := by native_decide
2699
2700-- Note: 288 = 2⁵ × 3², Ω = 5 + 2 = 7, so not 6-almost prime.
2701
2702/-- 324 = 2² × 3⁴ is 6-almost prime. -/
2703theorem six_almost_prime_threehundredtwentyfour : isSixAlmostPrime 324 = true := by native_decide
2704
2705/-- 352 = 2⁵ × 11 is 6-almost prime (RS-relevant: 11). -/
2706theorem six_almost_prime_threehundredfiftytwo : isSixAlmostPrime 352 = true := by native_decide
2707
2708/-- 360 = 2³ × 3² × 5 is 6-almost prime (RS-relevant: main superperiod). -/
2709theorem six_almost_prime_threehundredsixty : isSixAlmostPrime 360 = true := by native_decide
2710
2711-- Note: 384 = 2⁷ × 3, Ω = 7 + 1 = 8, so not 6-almost prime.
2712
2713/-- 400 = 2⁴ × 5² is 6-almost prime. -/
2714theorem six_almost_prime_fourhundred : isSixAlmostPrime 400 = true := by native_decide
2715
2716/-- 416 = 2⁵ × 13 is 6-almost prime. -/
2717theorem six_almost_prime_fourhundredsixteen : isSixAlmostPrime 416 = true := by native_decide
2718
2719-- Note: 432 = 2⁴ × 3³, Ω = 4 + 3 = 7, so not 6-almost prime.
2720
2721-- Note: 448 = 2⁶ × 7, Ω = 6 + 1 = 7, so not 6-almost prime.
2722
2723/-- 486 = 2 × 3⁵ is 6-almost prime. -/
2724theorem six_almost_prime_fourhundredeightysix : isSixAlmostPrime 486 = true := by native_decide
2725
2726-- Note: 500 = 2² × 5³, Ω = 2 + 3 = 5, so not 6-almost prime.
2727
2728/-- 528 = 2⁴ × 3 × 11 is 6-almost prime (RS-relevant: 11). -/
2729theorem six_almost_prime_fivehundredtwentyeight : isSixAlmostPrime 528 = true := by native_decide
2730
2731/-- 544 = 2⁵ × 17 is 6-almost prime (RS-relevant: 17). -/
2732theorem six_almost_prime_fivehundredfortyfour : isSixAlmostPrime 544 = true := by native_decide
2733
2734/-- 560 = 2⁴ × 5 × 7 is 6-almost prime. -/
2735theorem six_almost_prime_fivehundredsixty : isSixAlmostPrime 560 = true := by native_decide
2736
2737-- Note: 576 = 2⁶ × 3², Ω = 6 + 2 = 8, so not 6-almost prime.
2738
2739/-- 624 = 2⁴ × 3 × 13 is 6-almost prime. -/
2740theorem six_almost_prime_sixhundredtwentyfour : isSixAlmostPrime 624 = true := by native_decide
2741
2742/-- 729 = 3⁶ is 6-almost prime. -/
2743theorem six_almost_prime_sevenhundredtwentynine : isSixAlmostPrime 729 = true := by native_decide
2744
2745/-! ### Weak primes (p < (p_prev + p_next)/2) -/
2746
2747-- Note: 3 < (2 + 5)/2 = 3.5, but in ℕ, (2+5)/2 = 3, so 3 < 3 is false. 3 is balanced.
2748
2749/-- 7 is a weak prime: 7 < (5 + 11)/2 = 8. -/
2750theorem weak_prime_seven : Prime 7 ∧ Prime 5 ∧ Prime 11 ∧ 7 < (5 + 11) / 2 := by native_decide
2751
2752/-- 13 is a weak prime: 13 < (11 + 17)/2 = 14. -/
2753theorem weak_prime_thirteen : Prime 13 ∧ Prime 11 ∧ Prime 17 ∧ 13 < (11 + 17) / 2 := by native_decide
2754
2755/-- 19 is a weak prime: 19 < (17 + 23)/2 = 20. -/
2756theorem weak_prime_nineteen : Prime 19 ∧ Prime 17 ∧ Prime 23 ∧ 19 < (17 + 23) / 2 := by native_decide
2757
2758/-- 23 is a weak prime: 23 < (19 + 29)/2 = 24. -/
2759theorem weak_prime_twentythree : Prime 23 ∧ Prime 19 ∧ Prime 29 ∧ 23 < (19 + 29) / 2 := by native_decide
2760
2761/-- 31 is a weak prime: 31 < (29 + 37)/2 = 33. -/
2762theorem weak_prime_thirtyone : Prime 31 ∧ Prime 29 ∧ Prime 37 ∧ 31 < (29 + 37) / 2 := by native_decide
2763
2764/-- 43 is a weak prime: 43 < (41 + 47)/2 = 44. -/
2765theorem weak_prime_fortythree : Prime 43 ∧ Prime 41 ∧ Prime 47 ∧ 43 < (41 + 47) / 2 := by native_decide
2766
2767/-- 47 is a weak prime: 47 < (43 + 53)/2 = 48. -/
2768theorem weak_prime_fortyseven : Prime 47 ∧ Prime 43 ∧ Prime 53 ∧ 47 < (43 + 53) / 2 := by native_decide
2769
2770/-- 61 is a weak prime: 61 < (59 + 67)/2 = 63. -/
2771theorem weak_prime_sixtyone : Prime 61 ∧ Prime 59 ∧ Prime 67 ∧ 61 < (59 + 67) / 2 := by native_decide
2772
2773/-- 73 is a weak prime: 73 < (71 + 79)/2 = 75. -/
2774theorem weak_prime_seventythree : Prime 73 ∧ Prime 71 ∧ Prime 79 ∧ 73 < (71 + 79) / 2 := by native_decide
2775
2776/-- 83 is a weak prime: 83 < (79 + 89)/2 = 84. -/
2777theorem weak_prime_eightythree : Prime 83 ∧ Prime 79 ∧ Prime 89 ∧ 83 < (79 + 89) / 2 := by native_decide
2778
2779/-- 89 is a weak prime: 89 < (83 + 97)/2 = 90. -/
2780theorem weak_prime_eightynine : Prime 89 ∧ Prime 83 ∧ Prime 97 ∧ 89 < (83 + 97) / 2 := by native_decide
2781
2782/-- 103 is a weak prime: 103 < (101 + 107)/2 = 104 (RS-relevant). -/
2783theorem weak_prime_onehundredthree : Prime 103 ∧ Prime 101 ∧ Prime 107 ∧ 103 < (101 + 107) / 2 := by native_decide
2784
2785/-! ### Superprimes (prime-indexed primes: p_n where n is also prime) -/
2786
2787/-- p_2 = 3 is a superprime. -/
2788theorem superprime_three : Prime 3 ∧ Prime 2 := by native_decide
2789
2790/-- p_3 = 5 is a superprime. -/
2791theorem superprime_five : Prime 5 ∧ Prime 3 := by native_decide
2792
2793/-- p_5 = 11 is a superprime (RS-relevant). -/
2794theorem superprime_eleven : Prime 11 ∧ Prime 5 := by native_decide
2795
2796/-- p_7 = 17 is a superprime (RS-relevant). -/
2797theorem superprime_seventeen : Prime 17 ∧ Prime 7 := by native_decide
2798
2799/-- p_11 = 31 is a superprime. -/
2800theorem superprime_thirtyone : Prime 31 ∧ Prime 11 := by native_decide
2801
2802/-- p_13 = 41 is a superprime. -/
2803theorem superprime_fortyone : Prime 41 ∧ Prime 13 := by native_decide
2804
2805/-- p_17 = 59 is a superprime. -/
2806theorem superprime_fiftynine : Prime 59 ∧ Prime 17 := by native_decide
2807
2808/-- p_19 = 67 is a superprime. -/
2809theorem superprime_sixtyseven : Prime 67 ∧ Prime 19 := by native_decide
2810
2811/-- p_23 = 83 is a superprime. -/
2812theorem superprime_eightythree : Prime 83 ∧ Prime 23 := by native_decide
2813
2814/-- p_29 = 109 is a superprime. -/
2815theorem superprime_onehundrednine : Prime 109 ∧ Prime 29 := by native_decide
2816
2817/-- p_31 = 127 is a superprime (also Mersenne prime 2^7 - 1). -/
2818theorem superprime_onehundredtwentyseven : Prime 127 ∧ Prime 31 := by native_decide
2819
2820/-- p_37 = 157 is a superprime (RS-relevant: 37). -/
2821theorem superprime_onehundredfiftyseven : Prime 157 ∧ Prime 37 := by native_decide
2822
2823/-- p_41 = 179 is a superprime. -/
2824theorem superprime_onehundredseventynine : Prime 179 ∧ Prime 41 := by native_decide
2825
2826/-- p_43 = 191 is a superprime. -/
2827theorem superprime_onehundredninetyone : Prime 191 ∧ Prime 43 := by native_decide
2828
2829/-- p_47 = 211 is a superprime. -/
2830theorem superprime_twohundredeleven : Prime 211 ∧ Prime 47 := by native_decide
2831
2832/-! ### Isolated primes (no twin: p-2 and p+2 both composite) -/
2833
2834/-- 23 is an isolated prime: 21 = 3 × 7, 25 = 5². -/
2835theorem isolated_prime_twentythree : Prime 23 ∧ ¬Prime 21 ∧ ¬Prime 25 := by native_decide
2836
2837/-- 37 is an isolated prime: 35 = 5 × 7, 39 = 3 × 13 (RS-relevant). -/
2838theorem isolated_prime_thirtyseven : Prime 37 ∧ ¬Prime 35 ∧ ¬Prime 39 := by native_decide
2839
2840/-- 47 is an isolated prime: 45 = 3² × 5, 49 = 7². -/
2841theorem isolated_prime_fortyseven : Prime 47 ∧ ¬Prime 45 ∧ ¬Prime 49 := by native_decide
2842
2843/-- 53 is an isolated prime: 51 = 3 × 17, 55 = 5 × 11. -/
2844theorem isolated_prime_fiftythree : Prime 53 ∧ ¬Prime 51 ∧ ¬Prime 55 := by native_decide
2845
2846/-- 67 is an isolated prime: 65 = 5 × 13, 69 = 3 × 23. -/
2847theorem isolated_prime_sixtyseven : Prime 67 ∧ ¬Prime 65 ∧ ¬Prime 69 := by native_decide
2848
2849/-- 79 is an isolated prime: 77 = 7 × 11, 81 = 3⁴. -/
2850theorem isolated_prime_seventynine : Prime 79 ∧ ¬Prime 77 ∧ ¬Prime 81 := by native_decide
2851
2852/-- 83 is an isolated prime: 81 = 3⁴, 85 = 5 × 17. -/
2853theorem isolated_prime_eightythree : Prime 83 ∧ ¬Prime 81 ∧ ¬Prime 85 := by native_decide
2854
2855/-- 89 is an isolated prime: 87 = 3 × 29, 91 = 7 × 13. -/
2856theorem isolated_prime_eightynine : Prime 89 ∧ ¬Prime 87 ∧ ¬Prime 91 := by native_decide
2857
2858/-- 97 is an isolated prime: 95 = 5 × 19, 99 = 3² × 11. -/
2859theorem isolated_prime_ninetyseven : Prime 97 ∧ ¬Prime 95 ∧ ¬Prime 99 := by native_decide
2860
2861-- Note: 103 is NOT isolated since 103 - 2 = 101 is prime.
2862
2863/-- 113 is an isolated prime: 111 = 3 × 37, 115 = 5 × 23. -/
2864theorem isolated_prime_onehundredthirteen : Prime 113 ∧ ¬Prime 111 ∧ ¬Prime 115 := by native_decide
2865
2866/-- 127 is an isolated prime: 125 = 5³, 129 = 3 × 43. -/
2867theorem isolated_prime_onehundredtwentyseven : Prime 127 ∧ ¬Prime 125 ∧ ¬Prime 129 := by native_decide
2868
2869/-- 131 is NOT isolated: 131 - 2 = 129 (composite), but 131 + 2 = 133 = 7 × 19 (composite). -/
2870-- Check: 129 = 3 × 43, 133 = 7 × 19, so 131 IS isolated.
2871theorem isolated_prime_onehundredthirtyone : Prime 131 ∧ ¬Prime 129 ∧ ¬Prime 133 := by native_decide
2872
2873/-- 157 is an isolated prime: 155 = 5 × 31, 159 = 3 × 53. -/
2874theorem isolated_prime_onehundredfiftyseven : Prime 157 ∧ ¬Prime 155 ∧ ¬Prime 159 := by native_decide
2875
2876/-- 173 is an isolated prime: 171 = 3² × 19, 175 = 5² × 7. -/
2877theorem isolated_prime_onehundredseventythree : Prime 173 ∧ ¬Prime 171 ∧ ¬Prime 175 := by native_decide
2878
2879end Primes
2880end NumberTheory
2881end IndisputableMonolith
2882