IndisputableMonolith.NumberTheory.PrimeCostSpectrum

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.NumberTheory.PrimeLedgerStructure
   4
   5/-!
   6# The Prime Cost Spectrum
   7
   8This module extends the Recognition Science cost function `J` from the
   9positive reals to a complete arithmetic function on ℕ via the prime
  10factorization.  For each `n ≥ 1` we define
  11
  12  `c(n) := Σ_{p^k ‖ n} k · J(p) = Σ_p v_p(n) · J(p)`
  13
  14where `v_p(n)` is the `p`-adic valuation.  This makes `c` a
  15*completely additive* arithmetic function: `c(m·n) = c(m) + c(n)` for
  16positive `m, n`.
  17
  18The cost spectrum `{J(p) : p prime}` is the set of irreducible cost
  19quanta out of which every integer's cost is built.  Classical
  20prime-counting machinery (Chebyshev `θ`, `ψ`, prime counting `π`)
  21admits clean reformulations in terms of `c`.
  22
  23## Main definitions
  24
  25* `primeCost p`           : `J p` viewed as a real, restricted to primes.
  26* `costSpectrumValue n`   : the cost `c(n)` of an integer, defined via
  27                            `Nat.factorization`.
  28
  29## Main theorems (all 0 sorry, 0 axiom)
  30
  31* `primeCost_pos`         : `0 < J(p)` for every prime `p ≥ 2`.
  32* `primeCost_strictMono`  : `J` is strictly increasing on primes.
  33* `costSpectrumValue_one` : `c(1) = 0`.
  34* `costSpectrumValue_prime`: `c(p) = J(p)` for prime `p`.
  35* `costSpectrumValue_mul` : `c(m·n) = c(m) + c(n)` for `m, n > 0`.
  36* `costSpectrumValue_pow` : `c(p^k) = k · J(p)` for prime `p`.
  37* `costSpectrumValue_nonneg` : `c(n) ≥ 0`.
  38
  39## Lean status: 0 sorry
  40-/
  41
  42namespace IndisputableMonolith
  43namespace NumberTheory
  44namespace PrimeCostSpectrum
  45
  46open Cost
  47
  48noncomputable section
  49
  50/-! ## Prime cost: the irreducible quanta -/
  51
  52/-- The cost of a prime number.  This is just `J` evaluated on `p`,
  53    but isolated here because primes are the ledger's irreducible
  54    transactions and their costs are the spectrum's basis. -/
  55def primeCost (p : ℕ) : ℝ := Jcost (p : ℝ)
  56
  57/-- For any prime `p`, the prime cost is strictly positive. -/
  58theorem primeCost_pos {p : ℕ} (hp : Nat.Prime p) : 0 < primeCost p := by
  59  unfold primeCost
  60  have hp_pos : 0 < (p : ℝ) := by exact_mod_cast hp.pos
  61  have hp_ne_one : (p : ℝ) ≠ 1 := by
  62    have : p ≠ 1 := hp.one_lt.ne'
  63    exact_mod_cast this
  64  exact Jcost_pos_of_ne_one (p : ℝ) hp_pos hp_ne_one
  65
  66/-- The prime cost is nonnegative for any natural number `n` (treating
  67    `n = 0` as the boundary case `J(0) = -1` which we avoid by working
  68    only with positive `n`). -/
  69theorem primeCost_nonneg {n : ℕ} (hn : 0 < n) : 0 ≤ primeCost n := by
  70  unfold primeCost
  71  have : 0 < (n : ℝ) := by exact_mod_cast hn
  72  exact Jcost_nonneg this
  73
  74/-- `J` is strictly monotonic on the positive reals at and above 1.
  75    This is the key analytic input for showing that distinct primes
  76    have distinct cost values.
  77
  78    Algebraic proof: writing J(x) = (x-1)²/(2x), we need to show
  79    (x-1)²·y < (y-1)²·x when 1 ≤ x < y.  This rearranges to
  80    (y-x)·(xy-1) > 0, which holds since y-x > 0 and xy ≥ x ≥ 1
  81    with strict inequality whenever x > 1; the boundary case x = 1
  82    gives (x-1)² = 0 < (y-1)²·x. -/
  83private lemma jcost_strictMono_on_one_le :
  84    StrictMonoOn Jcost (Set.Ici (1 : ℝ)) := by
  85  intro x hx y hy hxy
  86  have hx1 : (1 : ℝ) ≤ x := hx
  87  have hy1 : (1 : ℝ) ≤ y := hy
  88  have hx_pos : 0 < x := by linarith
  89  have hy_pos : 0 < y := by linarith
  90  rw [Jcost_eq_sq (ne_of_gt hx_pos), Jcost_eq_sq (ne_of_gt hy_pos)]
  91  have h2x_pos : 0 < 2 * x := by linarith
  92  have h2y_pos : 0 < 2 * y := by linarith
  93  rw [div_lt_div_iff₀ h2x_pos h2y_pos]
  94  -- Goal: (x-1)² · 2y < (y-1)² · 2x.
  95  -- Identity: (y-1)²·x - (x-1)²·y = (y-x)·(xy - 1).
  96  have key : (y - 1)^2 * x - (x - 1)^2 * y = (y - x) * (x * y - 1) := by ring
  97  have hyx_pos : 0 < y - x := by linarith
  98  have hy_pos_strict : 1 < y := lt_of_le_of_lt hx1 hxy
  99  rcases lt_or_eq_of_le hx1 with hx_gt | hx_eq
 100  · -- x > 1: then x*y > 1, so (y-x)·(xy-1) > 0.
 101    have hxy_gt : 1 < x * y := by
 102      have h1 : 1 * 1 ≤ x * y := mul_le_mul hx1 hy1 (by norm_num) (le_of_lt hx_pos)
 103      have h2 : 1 < x * y := by
 104        have := mul_lt_mul_of_pos_right hx_gt hy_pos
 105        linarith
 106      exact h2
 107    nlinarith [mul_pos hyx_pos (by linarith : (0 : ℝ) < x * y - 1), key]
 108  · -- x = 1: LHS is 0, RHS is positive.
 109    rw [← hx_eq]
 110    have h_lhs : (1 - 1 : ℝ)^2 * (2 * y) = 0 := by ring
 111    rw [h_lhs]
 112    have hy_sub_pos : 0 < y - 1 := by linarith
 113    have hy_sq_pos : 0 < (y - 1)^2 := by positivity
 114    have h_two_pos : (0 : ℝ) < 2 * 1 := by norm_num
 115    exact mul_pos hy_sq_pos h_two_pos
 116
 117/-- Prime cost is strictly increasing in the prime: `p < q` ⟹ `J(p) < J(q)`. -/
 118theorem primeCost_strictMono {p q : ℕ}
 119    (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) :
 120    primeCost p < primeCost q := by
 121  unfold primeCost
 122  have hp_ge : (1 : ℝ) ≤ (p : ℝ) := by exact_mod_cast hp.one_lt.le
 123  have hq_ge : (1 : ℝ) ≤ (q : ℝ) := by exact_mod_cast hq.one_lt.le
 124  have : (p : ℝ) < (q : ℝ) := by exact_mod_cast hpq
 125  exact jcost_strictMono_on_one_le hp_ge hq_ge this
 126
 127/-! ## Cost spectrum value: extending J to all of ℕ via factorization -/
 128
 129/-- The total cost of an integer `n`, defined via its prime factorization:
 130    `c(n) = Σ_{p^k ‖ n} k · J(p)`.
 131    By convention `c(0) = 0`. -/
 132def costSpectrumValue (n : ℕ) : ℝ :=
 133  n.factorization.sum fun p k => (k : ℝ) * primeCost p
 134
 135@[simp]
 136theorem costSpectrumValue_one : costSpectrumValue 1 = 0 := by
 137  unfold costSpectrumValue
 138  simp [Nat.factorization_one]
 139
 140@[simp]
 141theorem costSpectrumValue_zero : costSpectrumValue 0 = 0 := by
 142  unfold costSpectrumValue
 143  simp [Nat.factorization_zero]
 144
 145/-- For a prime `p`, `c(p) = J(p)`. -/
 146theorem costSpectrumValue_prime {p : ℕ} (hp : Nat.Prime p) :
 147    costSpectrumValue p = primeCost p := by
 148  unfold costSpectrumValue
 149  rw [Nat.Prime.factorization hp]
 150  simp [Finsupp.sum_single_index]
 151
 152/-- For a prime power `p^k`, `c(p^k) = k · J(p)`. -/
 153theorem costSpectrumValue_pow {p k : ℕ} (hp : Nat.Prime p) :
 154    costSpectrumValue (p ^ k) = (k : ℝ) * primeCost p := by
 155  unfold costSpectrumValue
 156  rw [Nat.Prime.factorization_pow hp]
 157  simp [Finsupp.sum_single_index]
 158
 159/-- The cost is completely additive over coprime products.
 160    For arbitrary products with positive factors, the same identity holds
 161    because `Nat.factorization` is additive on positive multiplications. -/
 162theorem costSpectrumValue_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 163    costSpectrumValue (m * n) = costSpectrumValue m + costSpectrumValue n := by
 164  unfold costSpectrumValue
 165  rw [Nat.factorization_mul hm hn]
 166  rw [Finsupp.sum_add_index']
 167  · intro p
 168    simp
 169  · intro p i j
 170    push_cast
 171    ring
 172
 173/-- The cost is nonnegative for any positive `n`.
 174    Each summand `k · J(p) ≥ 0` by primality of `p`, so the sum is ≥ 0. -/
 175theorem costSpectrumValue_nonneg (n : ℕ) :
 176    0 ≤ costSpectrumValue n := by
 177  unfold costSpectrumValue
 178  apply Finsupp.sum_nonneg
 179  intro p hp_mem
 180  have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
 181    (Nat.support_factorization n ▸ hp_mem)
 182  have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
 183    exact_mod_cast Nat.zero_le _
 184  have hJ_nonneg : 0 ≤ primeCost p := le_of_lt (primeCost_pos hp_prime)
 185  exact mul_nonneg hk_nonneg hJ_nonneg
 186
 187/-- Cost is monotonic under multiplication by positive integers
 188    (a direct consequence of additivity and nonnegativity of prime costs). -/
 189theorem costSpectrumValue_le_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 190    costSpectrumValue m ≤ costSpectrumValue (m * n) := by
 191  rw [costSpectrumValue_mul hm hn]
 192  have := costSpectrumValue_nonneg n
 193  linarith
 194
 195/-- The cost is strictly positive for any integer `n ≥ 2`. -/
 196theorem costSpectrumValue_pos {n : ℕ} (hn : 2 ≤ n) :
 197    0 < costSpectrumValue n := by
 198  have hn_ne_zero : n ≠ 0 := by omega
 199  have hn_ne_one : n ≠ 1 := by omega
 200  obtain ⟨p, hp_prime, hp_dvd⟩ := Nat.exists_prime_and_dvd hn_ne_one
 201  have hp_mem : p ∈ n.factorization.support := by
 202    rw [Nat.support_factorization]
 203    exact Nat.mem_primeFactors.mpr ⟨hp_prime, hp_dvd, hn_ne_zero⟩
 204  have hk_pos : 0 < n.factorization p := by
 205    have := Finsupp.mem_support_iff.mp hp_mem
 206    exact Nat.pos_of_ne_zero this
 207  have hJ_pos : 0 < primeCost p := primeCost_pos hp_prime
 208  have hsummand_pos : 0 < (n.factorization p : ℝ) * primeCost p := by
 209    have hk_real_pos : (0 : ℝ) < (n.factorization p : ℝ) := by
 210      exact_mod_cast hk_pos
 211    exact mul_pos hk_real_pos hJ_pos
 212  unfold costSpectrumValue
 213  -- Split the Finsupp sum into the p-summand plus the rest, both nonneg.
 214  rw [Finsupp.sum, ← Finset.sum_erase_add _ _ hp_mem]
 215  apply add_pos_of_nonneg_of_pos
 216  · apply Finset.sum_nonneg
 217    intro q hq_mem
 218    have hq_in_support : q ∈ n.factorization.support :=
 219      (Finset.mem_erase.mp hq_mem).2
 220    have hq_prime : Nat.Prime q := Nat.prime_of_mem_primeFactors
 221      (Nat.support_factorization n ▸ hq_in_support)
 222    have hk_nonneg : (0 : ℝ) ≤ (n.factorization q : ℝ) := by
 223      exact_mod_cast Nat.zero_le _
 224    exact mul_nonneg hk_nonneg (le_of_lt (primeCost_pos hq_prime))
 225  · exact hsummand_pos
 226
 227/-! ## Auxiliary arithmetic functions -/
 228
 229/-- The total prime factor count (with multiplicity) of `n`, written `Ω(n)`. -/
 230def Omega (n : ℕ) : ℕ := n.factorization.sum fun _ k => k
 231
 232/-- The total prime factor count (without multiplicity) of `n`, written `ω(n)`. -/
 233def omega (n : ℕ) : ℕ := n.factorization.support.card
 234
 235/-- The "sum of prime factors with multiplicity" function `sopfr(n) = Σ k·p`. -/
 236def sopfr (n : ℕ) : ℕ := n.factorization.sum fun p k => k * p
 237
 238/-- The reciprocal-sum-of-prime-factors `Σ k/p` as a real number. -/
 239noncomputable def reciprocalPrimeSum (n : ℕ) : ℝ :=
 240  n.factorization.sum fun p k => (k : ℝ) / (p : ℝ)
 241
 242/-- Per-summand identity: each prime-power contribution to `c(n)` decomposes
 243    into half of `k·p`, half of `k/p`, minus `k`.  Used to derive the
 244    closed-form decomposition below. -/
 245private lemma summand_decomposition (p k : ℕ) (hp : Nat.Prime p) :
 246    (k : ℝ) * primeCost p =
 247      (1/2) * ((k : ℝ) * (p : ℝ))
 248      + (1/2) * ((k : ℝ) / (p : ℝ)) - (k : ℝ) := by
 249  unfold primeCost Jcost
 250  have hp_pos : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
 251  have hp_ne : (p : ℝ) ≠ 0 := ne_of_gt hp_pos
 252  field_simp
 253
 254/-! ## Power formula and Omega bound -/
 255
 256/-- For any positive integer `n` and any natural `k`,
 257    `c(n^k) = k · c(n)`.  This is the complete-additivity of `c`
 258    extended to repeated multiplication. -/
 259theorem costSpectrumValue_pow_general {n : ℕ} (hn : n ≠ 0) (k : ℕ) :
 260    costSpectrumValue (n ^ k) = (k : ℝ) * costSpectrumValue n := by
 261  induction k with
 262  | zero => simp [costSpectrumValue_one]
 263  | succ k ih =>
 264    have hnk : n ^ k ≠ 0 := pow_ne_zero k hn
 265    rw [pow_succ, costSpectrumValue_mul hnk hn, ih]
 266    push_cast
 267    ring
 268
 269/-- The cost spectrum value is bounded by `Ω(n) · J(p_max)` where
 270    `p_max` is the largest prime factor of `n`.  Specialized to the
 271    weaker bound `c(n) ≤ Ω(n) · J(n)` using monotonicity of `J` on
 272    `[1, ∞)`.  Useful for asymptotic upper bounds. -/
 273theorem costSpectrumValue_le_omega_mul_jcost {n : ℕ} (hn : 2 ≤ n) :
 274    costSpectrumValue n ≤ (Omega n : ℝ) * Jcost (n : ℝ) := by
 275  have hn_pos : 0 < n := by omega
 276  have hn_ge_one : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn_pos
 277  -- Bound each summand: k · J(p) ≤ k · J(n) for prime p dividing n,
 278  -- since p ≤ n and J is monotonic on [1, ∞).
 279  have h_per_summand : ∀ p ∈ n.factorization.support,
 280      (n.factorization p : ℝ) * primeCost p
 281        ≤ (n.factorization p : ℝ) * Jcost (n : ℝ) := by
 282    intro p hp_mem
 283    have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
 284      (Nat.support_factorization n ▸ hp_mem)
 285    have hp_dvd : p ∣ n :=
 286      Nat.dvd_of_mem_primeFactors (Nat.support_factorization n ▸ hp_mem)
 287    have hp_le_n : p ≤ n := Nat.le_of_dvd hn_pos hp_dvd
 288    have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
 289      exact_mod_cast Nat.zero_le _
 290    have hp_real_ge_one : (1 : ℝ) ≤ (p : ℝ) := by exact_mod_cast hp_prime.one_lt.le
 291    have hp_real_le_n : (p : ℝ) ≤ (n : ℝ) := by exact_mod_cast hp_le_n
 292    have h_J_mono : primeCost p ≤ Jcost (n : ℝ) := by
 293      unfold primeCost
 294      rcases lt_or_eq_of_le hp_real_le_n with h_lt | h_eq
 295      · exact le_of_lt (jcost_strictMono_on_one_le hp_real_ge_one hn_ge_one h_lt)
 296      · rw [h_eq]
 297    exact mul_le_mul_of_nonneg_left h_J_mono hk_nonneg
 298  -- Sum the bound over all primes in the support.
 299  -- LHS: sum of k_p · J(p). RHS: (sum of k_p) · J(n) = sum of k_p · J(n).
 300  have h_rhs_split :
 301      (Omega n : ℝ) * Jcost (n : ℝ)
 302        = n.factorization.sum (fun _ k => (k : ℝ) * Jcost (n : ℝ)) := by
 303    unfold Omega
 304    rw [show (n.factorization.sum fun _ k => (k : ℝ) * Jcost (n : ℝ))
 305          = (n.factorization.sum fun _ k => (k : ℝ)) * Jcost (n : ℝ) by
 306        rw [← Finsupp.sum_mul]]
 307    congr 1
 308    push_cast
 309    rfl
 310  unfold costSpectrumValue
 311  rw [h_rhs_split]
 312  exact Finset.sum_le_sum h_per_summand
 313
 314/-! ## Cost spectrum certificate -/
 315
 316/-- Master certificate: the elementary properties of the cost spectrum
 317    that this module establishes.  Used by the companion paper. -/
 318theorem cost_spectrum_certificate :
 319    -- (1) Prime cost is strictly positive.
 320    (∀ {p : ℕ}, Nat.Prime p → 0 < primeCost p) ∧
 321    -- (2) Prime cost is strictly monotonic in p.
 322    (∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → p < q →
 323      primeCost p < primeCost q) ∧
 324    -- (3) Cost is zero exactly at n = 1 (within positive integers).
 325    (costSpectrumValue 1 = 0) ∧
 326    -- (4) Cost is positive for n ≥ 2.
 327    (∀ {n : ℕ}, 2 ≤ n → 0 < costSpectrumValue n) ∧
 328    -- (5) Cost is completely additive over positive integers.
 329    (∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 →
 330      costSpectrumValue (m * n) = costSpectrumValue m + costSpectrumValue n) ∧
 331    -- (6) Cost on a prime equals its prime cost.
 332    (∀ {p : ℕ}, Nat.Prime p → costSpectrumValue p = primeCost p) ∧
 333    -- (7) Cost on a power: c(n^k) = k · c(n).
 334    (∀ {n : ℕ} (_ : n ≠ 0) (k : ℕ),
 335      costSpectrumValue (n ^ k) = (k : ℝ) * costSpectrumValue n) ∧
 336    -- (8) Cost is bounded above by Ω(n) · J(n).
 337    (∀ {n : ℕ}, 2 ≤ n →
 338      costSpectrumValue n ≤ (Omega n : ℝ) * Jcost (n : ℝ)) :=
 339  ⟨@primeCost_pos,
 340   @primeCost_strictMono,
 341   costSpectrumValue_one,
 342   @costSpectrumValue_pos,
 343   @costSpectrumValue_mul,
 344   @costSpectrumValue_prime,
 345   @costSpectrumValue_pow_general,
 346   @costSpectrumValue_le_omega_mul_jcost⟩
 347
 348end
 349
 350end PrimeCostSpectrum
 351end NumberTheory
 352end IndisputableMonolith
 353