IndisputableMonolith.NumberTheory.UniversalCostSpectrum

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# The Universal Cost Spectrum
   6
   7This module abstracts the prime cost spectrum framework from
   8`IndisputableMonolith.NumberTheory.PrimeCostSpectrum` and
   9`...PrimeCostSpectrumPoly` to a single abstract setting parameterized
  10by any "norm-equipped prime structure".
  11
  12A `PrimeNormStructure P` consists of a type `P` (the "primes") together
  13with a real-valued norm `‖p‖ > 1` on each prime.  Both classical primes
  14in `ℕ` (with `‖p‖ = p`) and monic irreducibles in `Fq[T]` (with
  15`‖P‖ = q^deg P`) are instances.
  16
  17For any such structure, we define the universal cost arithmetic function
  18
  19  `c(f) := Σ_p f(p) · J(‖p‖)`
  20
  21on finitely-supported functions `f : P →₀ ℕ` (representing elements of
  22the multiplicative monoid generated by `P`).  We prove the universal
  23elementary properties: `c(0) = 0`, `c(f + g) = c(f) + c(g)`, `c(f) ≥ 0`,
  24and `c(f) > 0` for `f ≠ 0`.
  25
  26This module supports the Cost-Reciprocity synthesis paper, which argues
  27that all cost-spectrum constructions across the Selberg class of
  28L-functions are instances of this single abstract framework.
  29
  30## Main definitions
  31
  32* `PrimeNormStructure P`     : the typeclass of "primes with norm > 1".
  33* `primeJcost p`              : `J(‖p‖)`, the cost of an abstract prime.
  34* `universalCost f`           : the cost spectrum value on a Finsupp.
  35
  36## Main theorems (all 0 sorry, 0 non-standard axioms)
  37
  38* `primeJcost_pos`            : `0 < primeJcost p` for any `p`.
  39* `universalCost_zero`        : `c(0) = 0`.
  40* `universalCost_single`      : `c(single p k) = k · J(‖p‖)`.
  41* `universalCost_add`         : `c(f + g) = c(f) + c(g)`.
  42* `universalCost_nonneg`      : `0 ≤ c(f)`.
  43* `universalCost_pos`         : `f ≠ 0 → 0 < c(f)`.
  44* `universal_cost_certificate`: bundled certificate.
  45
  46## Instances
  47
  48* `Nat.Primes.instPrimeNormStructure` : integer primes, `‖p‖ = p`.
  49
  50The function-field instance is parameterized by the field `F` and is
  51provided as a `def` rather than an `instance` (since it depends on `F`).
  52
  53## Lean status: 0 sorry
  54-/
  55
  56namespace IndisputableMonolith
  57namespace NumberTheory
  58namespace UniversalCostSpectrum
  59
  60open Cost
  61
  62noncomputable section
  63
  64/-! ## The abstract structure -/
  65
  66/-- A type `P` is a `PrimeNormStructure` if it carries a real-valued
  67    norm `‖·‖ > 1` on each element.  This abstracts away from the
  68    specific arithmetic structure (integer primes, monic irreducible
  69    polynomials, prime ideals in number fields, etc.). -/
  70class PrimeNormStructure (P : Type*) where
  71  norm : P → ℝ
  72  norm_gt_one : ∀ p : P, 1 < norm p
  73
  74variable {P : Type*} [PrimeNormStructure P]
  75
  76/-- The cost of an abstract prime: `J(‖p‖)`. -/
  77def primeJcost (p : P) : ℝ := Jcost (PrimeNormStructure.norm p)
  78
  79/-- The cost of any prime is strictly positive. -/
  80theorem primeJcost_pos (p : P) : 0 < primeJcost p := by
  81  unfold primeJcost
  82  apply Jcost_pos_of_ne_one
  83  · linarith [PrimeNormStructure.norm_gt_one p]
  84  · linarith [PrimeNormStructure.norm_gt_one p]
  85
  86theorem primeJcost_nonneg (p : P) : 0 ≤ primeJcost p :=
  87  le_of_lt (primeJcost_pos p)
  88
  89/-! ## The universal cost spectrum value -/
  90
  91variable [DecidableEq P]
  92
  93/-- The universal cost spectrum value on `f : P →₀ ℕ`.
  94
  95    Interpreting `f` as the multiplicity vector of an element of the
  96    multiplicative monoid generated by `P`, this is the cost-weighted
  97    sum `Σ_p f(p) · J(‖p‖)`. -/
  98def universalCost (f : P →₀ ℕ) : ℝ :=
  99  f.sum (fun p k => (k : ℝ) * primeJcost p)
 100
 101@[simp] theorem universalCost_zero : universalCost (0 : P →₀ ℕ) = 0 := by
 102  simp [universalCost]
 103
 104theorem universalCost_single (p : P) (k : ℕ) :
 105    universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p := by
 106  unfold universalCost
 107  simp [Finsupp.sum_single_index]
 108
 109@[simp] theorem universalCost_single_one (p : P) :
 110    universalCost (Finsupp.single p 1) = primeJcost p := by
 111  rw [universalCost_single]
 112  ring
 113
 114theorem universalCost_add (f g : P →₀ ℕ) :
 115    universalCost (f + g) = universalCost f + universalCost g := by
 116  unfold universalCost
 117  rw [Finsupp.sum_add_index']
 118  · intro p; simp
 119  · intro p i j; push_cast; ring
 120
 121theorem universalCost_nonneg (f : P →₀ ℕ) : 0 ≤ universalCost f := by
 122  apply Finsupp.sum_nonneg
 123  intro p _
 124  apply mul_nonneg
 125  · exact_mod_cast Nat.zero_le _
 126  · exact primeJcost_nonneg p
 127
 128theorem universalCost_pos {f : P →₀ ℕ} (hf : f ≠ 0) : 0 < universalCost f := by
 129  obtain ⟨p, hp_mem⟩ := Finsupp.support_nonempty_iff.mpr hf
 130  have hk_pos : 0 < f p := by
 131    have := Finsupp.mem_support_iff.mp hp_mem
 132    exact Nat.pos_of_ne_zero this
 133  have hJ_pos : 0 < primeJcost p := primeJcost_pos p
 134  have hsummand_pos : 0 < (f p : ℝ) * primeJcost p := by
 135    have hk_real : (0 : ℝ) < (f p : ℝ) := by exact_mod_cast hk_pos
 136    exact mul_pos hk_real hJ_pos
 137  unfold universalCost
 138  rw [Finsupp.sum, ← Finset.sum_erase_add _ _ hp_mem]
 139  apply add_pos_of_nonneg_of_pos
 140  · apply Finset.sum_nonneg
 141    intro q _
 142    apply mul_nonneg
 143    · exact_mod_cast Nat.zero_le _
 144    · exact primeJcost_nonneg q
 145  · exact hsummand_pos
 146
 147/-! ## Power and multiplicative structure -/
 148
 149/-- The cost of a power `n · single p 1`: `c(n · single p 1) = n · J(‖p‖)`.
 150    More generally, scaling a single-prime Finsupp scales the cost. -/
 151theorem universalCost_smul_single (n : ℕ) (p : P) :
 152    universalCost (n • Finsupp.single p 1) = (n : ℝ) * primeJcost p := by
 153  rw [show n • Finsupp.single p (1 : ℕ) = Finsupp.single p n by
 154        ext q; by_cases hpq : q = p
 155        · subst hpq; simp
 156        · simp [Finsupp.single_apply, hpq]]
 157  exact universalCost_single p n
 158
 159/-! ## Universal certificate -/
 160
 161/-- Master certificate: the elementary properties of the universal
 162    cost spectrum. -/
 163theorem universal_cost_certificate :
 164    -- (1) Every prime cost is strictly positive.
 165    (∀ (p : P), 0 < primeJcost p) ∧
 166    -- (2) Cost is zero at the trivial Finsupp (the unit element).
 167    (universalCost (0 : P →₀ ℕ) = 0) ∧
 168    -- (3) Cost is additive.
 169    (∀ (f g : P →₀ ℕ),
 170      universalCost (f + g) = universalCost f + universalCost g) ∧
 171    -- (4) Cost on a singleton: c(single p k) = k · J(‖p‖).
 172    (∀ (p : P) (k : ℕ),
 173      universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p) ∧
 174    -- (5) Cost is nonneg.
 175    (∀ (f : P →₀ ℕ), 0 ≤ universalCost f) ∧
 176    -- (6) Cost is strictly positive on non-trivial Finsupps.
 177    (∀ {f : P →₀ ℕ}, f ≠ 0 → 0 < universalCost f) :=
 178  ⟨primeJcost_pos,
 179   universalCost_zero,
 180   universalCost_add,
 181   universalCost_single,
 182   universalCost_nonneg,
 183   @universalCost_pos P _ _⟩
 184
 185/-! ## Instance: Integer primes -/
 186
 187instance natPrimesInstance : PrimeNormStructure Nat.Primes where
 188  norm := fun p => (p.val : ℝ)
 189  norm_gt_one := fun p => by exact_mod_cast p.prop.one_lt
 190
 191example (p : Nat.Primes) : 0 < primeJcost p := primeJcost_pos p
 192
 193/-! ## Function-field instance (parameterized) -/
 194
 195/-- The function-field prime norm structure: monic irreducible polynomials
 196    in `F[X]` with norm `q^deg P` where `q = Fintype.card F`.  Parameterized
 197    by the field `F` (so it cannot be a global instance). -/
 198def funcFieldNormStructure (F : Type*) [Field F] [Fintype F]
 199    [DecidableEq F] (h2 : 2 ≤ Fintype.card F) :
 200    PrimeNormStructure {P : Polynomial F // P.Monic ∧ Irreducible P} where
 201  norm := fun P => (Fintype.card F : ℝ) ^ P.val.natDegree
 202  norm_gt_one := fun P => by
 203    have hP_irr : Irreducible P.val := P.prop.2
 204    have hP_ne : P.val ≠ 0 := hP_irr.ne_zero
 205    have hP_deg : 0 < P.val.natDegree := by
 206      rw [Nat.pos_iff_ne_zero]
 207      intro h_zero
 208      obtain ⟨c, hc⟩ := Polynomial.natDegree_eq_zero.mp h_zero
 209      have hc_ne : c ≠ 0 := by
 210        intro h_c_zero
 211        apply hP_ne
 212        rw [← hc, h_c_zero]; simp
 213      have hP_unit : IsUnit P.val := by
 214        rw [← hc]
 215        exact Polynomial.isUnit_C.mpr (isUnit_iff_ne_zero.mpr hc_ne)
 216      exact hP_irr.not_isUnit hP_unit
 217    have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by exact_mod_cast h2
 218    exact one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP_deg)
 219
 220end
 221
 222end UniversalCostSpectrum
 223end NumberTheory
 224end IndisputableMonolith
 225