IndisputableMonolith.NumberTheory.Primes.RSConstants

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3import IndisputableMonolith.NumberTheory.Primes.Factorization
   4
   5/-!
   6# RS constants (prime facts and factorizations)
   7
   8This file collects small, **decidable** arithmetic facts about integers that appear repeatedly in
   9the `reality` repo (e.g. `8`, `45`, `360`, `840`, and prime markers like `11`, `17`, `37`, `103`,
  10`137`).
  11
  12These are intentionally “boring but stable” anchors: they keep later bridge lemmas readable and
  13avoid re-proving the same arithmetic in many places.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace Primes
  19
  20/-! ### Prime facts (small constants) -/
  21
  22theorem prime_five : Prime 5 := by
  23  decide
  24
  25theorem prime_eleven : Prime 11 := by
  26  decide
  27
  28theorem prime_seventeen : Prime 17 := by
  29  decide
  30
  31theorem prime_thirtyseven : Prime 37 := by
  32  decide
  33
  34theorem prime_onehundredthree : Prime 103 := by
  35  decide
  36
  37theorem prime_onehundredthirtyseven : Prime 137 := by
  38  decide
  39
  40/-! ### GCD/LCM and factorizations (RS cycle integers) -/
  41
  42theorem eight_eq_two_pow_three : (8 : ℕ) = 2^3 := by
  43  native_decide
  44
  45theorem fortyfive_eq_three_sq_mul_five : (45 : ℕ) = 3^2 * 5 := by
  46  native_decide
  47
  48theorem gcd_eight_fortyfive_eq_one : Nat.gcd 8 45 = 1 := by
  49  native_decide
  50
  51theorem lcm_eight_fortyfive_eq_360 : Nat.lcm 8 45 = 360 := by
  52  native_decide
  53
  54theorem threehundredsixty_factorization : (360 : ℕ) = 2^3 * 3^2 * 5 := by
  55  native_decide
  56
  57theorem wheel840_factorization : (840 : ℕ) = 2^3 * 3 * 5 * 7 := by
  58  native_decide
  59
  60/-! ### Rational identities (beat-frequency arithmetic) -/
  61
  62theorem one_div_eight_sub_one_div_fortyfive :
  63    (1 : ℚ) / 8 - (1 : ℚ) / 45 = (37 : ℚ) / 360 := by
  64  norm_num
  65
  66theorem aliasing_ratio : (37 : ℚ) / 45 < 1 := by
  67  norm_num
  68
  69/-! ### Integer identities (beat numerator as a difference) -/
  70
  71/-- The RS beat numerator arises as a simple difference: \(45 - 8 = 37\). -/
  72theorem fortyfive_sub_eight_eq_thirtyseven : (45 : ℕ) - 8 = 37 := by
  73  native_decide
  74
  75/-- Convenience wrapper: 8 and 45 are coprime. -/
  76theorem coprime_eight_fortyfive : Nat.Coprime 8 45 := by
  77  native_decide
  78
  79/-! ### vp-based characterizations of RS constants -/
  80
  81/-- The prime spectrum of 8: only has 2-content, with exponent 3. -/
  82theorem vp_eight_two : vp 2 8 = 3 := by native_decide
  83theorem vp_eight_three : vp 3 8 = 0 := by native_decide
  84theorem vp_eight_five : vp 5 8 = 0 := by native_decide
  85
  86/-- The prime spectrum of 45: has 3-content (exponent 2) and 5-content (exponent 1). -/
  87theorem vp_fortyfive_two : vp 2 45 = 0 := by native_decide
  88theorem vp_fortyfive_three : vp 3 45 = 2 := by native_decide
  89theorem vp_fortyfive_five : vp 5 45 = 1 := by native_decide
  90
  91/-- The prime spectrum of 360: the full LCM uses all three primes {2, 3, 5}. -/
  92theorem vp_360_two : vp 2 360 = 3 := by native_decide
  93theorem vp_360_three : vp 3 360 = 2 := by native_decide
  94theorem vp_360_five : vp 5 360 = 1 := by native_decide
  95theorem vp_360_seven : vp 7 360 = 0 := by native_decide
  96
  97/-- The prime spectrum of 840 (wheel modulus): uses {2, 3, 5, 7}. -/
  98theorem vp_840_two : vp 2 840 = 3 := by native_decide
  99theorem vp_840_three : vp 3 840 = 1 := by native_decide
 100theorem vp_840_five : vp 5 840 = 1 := by native_decide
 101theorem vp_840_seven : vp 7 840 = 1 := by native_decide
 102
 103/-- 360 = lcm(8, 45) via the vp characterization: max at each prime. -/
 104theorem lcm_eight_fortyfive_vp_characterization (p : ℕ) :
 105    vp p 360 = max (vp p 8) (vp p 45) := by
 106  have h360 : (360 : ℕ) ≠ 0 := by decide
 107  have h8 : (8 : ℕ) ≠ 0 := by decide
 108  have h45 : (45 : ℕ) ≠ 0 := by decide
 109  rw [← lcm_eight_fortyfive_eq_360]
 110  exact vp_lcm h8 h45 p
 111
 112/-- 8 and 45 are coprime: their gcd has vp = 0 everywhere. -/
 113theorem coprime_eight_fortyfive_vp (p : ℕ) : vp p (Nat.gcd 8 45) = 0 := by
 114  rw [gcd_eight_fortyfive_eq_one]
 115  simp
 116
 117/-- The beat frequency numerator 37 is prime. -/
 118theorem prime_beat_numerator : Prime 37 := prime_thirtyseven
 119
 120/-- 37 does not divide 360 (since gcd(37, 360) = 1). -/
 121theorem coprime_thirtyseven_360 : Nat.Coprime 37 360 := by native_decide
 122
 123/-! ### Additional RS primes and constants -/
 124
 125/-- The number 13 is prime (cicada cycle). -/
 126theorem prime_thirteen : Prime 13 := by decide
 127
 128/-- The number 7 is prime (wheel factor). -/
 129theorem prime_seven : Prime 7 := by decide
 130
 131/-- The cycle-45 gap is squarefree: 45 = 3² · 5, but wait—45 is NOT squarefree because 3² divides it.
 132We record the correct statement: 45 is not squarefree. -/
 133theorem not_squarefree_fortyfive : ¬Squarefree 45 := by
 134  intro hsq
 135  have h := hsq 3 ⟨5, by norm_num⟩
 136  simp at h
 137
 138/-- 360 is not squarefree (since 4 = 2² divides it). -/
 139theorem not_squarefree_360 : ¬Squarefree 360 := by
 140  intro hsq
 141  have h := hsq 2 ⟨90, by norm_num⟩
 142  simp at h
 143
 144/-- 8 is not squarefree (since 4 = 2² divides it). -/
 145theorem not_squarefree_eight : ¬Squarefree 8 := by
 146  intro hsq
 147  have h := hsq 2 ⟨2, by norm_num⟩
 148  simp at h
 149
 150/-- 840 is not squarefree (since 4 = 2² divides it). -/
 151theorem not_squarefree_840 : ¬Squarefree 840 := by
 152  intro hsq
 153  have h := hsq 2 ⟨210, by norm_num⟩
 154  simp at h
 155
 156/-- The radical of 360 (product of distinct prime factors) is 30 = 2·3·5. -/
 157theorem radical_360 : (360 : ℕ).primeFactors.prod id = 30 := by native_decide
 158
 159/-- The radical of 8 is 2. -/
 160theorem radical_eight : (8 : ℕ).primeFactors.prod id = 2 := by native_decide
 161
 162/-- The radical of 45 is 15 = 3·5. -/
 163theorem radical_fortyfive : (45 : ℕ).primeFactors.prod id = 15 := by native_decide
 164
 165/-! ### Divisibility facts for RS constants -/
 166
 167/-- 8 divides 360. -/
 168theorem eight_dvd_360 : 8 ∣ 360 := by decide
 169
 170/-- 45 divides 360. -/
 171theorem fortyfive_dvd_360 : 45 ∣ 360 := by decide
 172
 173/-- 360 / 8 = 45. -/
 174theorem threehundredsixty_div_eight : 360 / 8 = 45 := by native_decide
 175
 176/-- 360 / 45 = 8. -/
 177theorem threehundredsixty_div_fortyfive : 360 / 45 = 8 := by native_decide
 178
 179end Primes
 180end NumberTheory
 181end IndisputableMonolith
 182