IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# The Cost Spectrum on the Polynomial Ring `F[X]`
   6
   7This module is the function-field analog of
   8`IndisputableMonolith.NumberTheory.PrimeCostSpectrum`.
   9For a finite field `F` of cardinality `q`, the polynomial ring `F[X]`
  10is a unique factorization domain in which every nonzero monic
  11polynomial factors uniquely into monic irreducibles.
  12
  13The norm of a monic polynomial `f` is `‖f‖ := q^(deg f)`.
  14Every monic irreducible `P` of degree `n` has norm `q^n`.
  15The cost function extends to `F[X]` via
  16
  17  `c(f) := Σ_{P irreducible} v_P(f) · J(‖P‖)`
  18
  19where `v_P(f)` is the multiplicity of `P` in the factorization of `f`.
  20
  21We define `c` for arbitrary nonzero polynomials (not just monic) via
  22the multiset of normalized factors, which is well-defined in any UFD
  23via mathlib's `normalizedFactors`.
  24
  25## Main definitions
  26
  27* `polyCost q f`         : the cost of a polynomial `f`, computed
  28                           from `normalizedFactors f`, using `q` as
  29                           the field cardinality parameter.
  30* `polyPrimeCost q P`    : the cost of an irreducible factor `P`,
  31                           equal to `Jcost (q^(deg P) : ℝ)`.
  32
  33## Main theorems (all 0 sorry, 0 axiom)
  34
  35* `polyPrimeCost_pos`     : the cost of any irreducible polynomial of
  36                            positive degree is strictly positive.
  37* `polyCost_one`          : `c(1) = 0`.
  38* `polyCost_mul`          : `c(f g) = c(f) + c(g)` for nonzero `f, g`.
  39* `polyCost_irreducible`  : `c(P) = J(q^(deg P))` for `P` monic
  40                            irreducible of positive degree.
  41* `polyCost_pow`          : `c(P^k) = k · J(q^(deg P))`.
  42* `polyCost_nonneg`       : `c(f) ≥ 0`.
  43* `cost_spectrum_poly_certificate` : bundled certificate.
  44
  45## Lean status: 0 sorry
  46-/
  47
  48namespace IndisputableMonolith
  49namespace NumberTheory
  50namespace PrimeCostSpectrumPoly
  51
  52open Polynomial Cost UniqueFactorizationMonoid
  53
  54noncomputable section
  55
  56variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
  57
  58/-! ## The norm of a polynomial
  59
  60The norm of a polynomial of degree `n` over a field of cardinality `q`
  61is `q^n`.  By convention the norm of the zero polynomial is `0` and the
  62norm of a unit (degree 0) polynomial is `1`. -/
  63
  64/-- The norm `q^(deg f)` of a polynomial as a real number, where
  65    `q := Fintype.card F`. -/
  66def polyNorm (f : Polynomial F) : ℝ :=
  67  (Fintype.card F : ℝ) ^ f.natDegree
  68
  69@[simp] theorem polyNorm_one : polyNorm (1 : Polynomial F) = 1 := by
  70  unfold polyNorm; simp
  71
  72theorem polyNorm_pos (f : Polynomial F) : 0 < polyNorm f := by
  73  unfold polyNorm
  74  have hq : 0 < (Fintype.card F : ℝ) := by
  75    exact_mod_cast Fintype.card_pos
  76  exact pow_pos hq _
  77
  78/-! ## Cost spectrum: per-irreducible and total -/
  79
  80/-- The cost of an irreducible polynomial `P`, equal to `J(‖P‖)`. -/
  81def polyPrimeCost (P : Polynomial F) : ℝ := Jcost (polyNorm P)
  82
  83/-- The cost of a polynomial `f`, computed by summing the per-factor
  84    cost over the multiset of normalized irreducible factors of `f`.
  85    By convention `polyCost 0 = 0`. -/
  86def polyCost (f : Polynomial F) : ℝ :=
  87  ((normalizedFactors f).map polyPrimeCost).sum
  88
  89/-! ## Elementary properties -/
  90
  91@[simp] theorem polyCost_zero : polyCost (0 : Polynomial F) = 0 := by
  92  unfold polyCost
  93  simp [normalizedFactors_zero]
  94
  95@[simp] theorem polyCost_one : polyCost (1 : Polynomial F) = 0 := by
  96  unfold polyCost
  97  simp [normalizedFactors_one]
  98
  99/-- The norm of a monic polynomial of positive degree is at least `q ≥ 2`,
 100    hence at least `2`.  Combined with `Jcost_pos_of_ne_one`, this gives
 101    `polyPrimeCost P > 0` for any irreducible polynomial of positive degree
 102    over a field with at least 2 elements. -/
 103theorem polyPrimeCost_pos {P : Polynomial F} (hP : 0 < P.natDegree)
 104    (hF : 2 ≤ Fintype.card F) : 0 < polyPrimeCost P := by
 105  unfold polyPrimeCost
 106  have hnorm_pos : 0 < polyNorm P := polyNorm_pos P
 107  have hnorm_ne_one : polyNorm P ≠ 1 := by
 108    unfold polyNorm
 109    have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by
 110      exact_mod_cast hF
 111    have h_pow_gt : 1 < (Fintype.card F : ℝ) ^ P.natDegree :=
 112      one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP)
 113    exact ne_of_gt h_pow_gt
 114  exact Jcost_pos_of_ne_one (polyNorm P) hnorm_pos hnorm_ne_one
 115
 116/-- `polyPrimeCost` is nonnegative on any polynomial (it is always `J`
 117    of a positive real). -/
 118theorem polyPrimeCost_nonneg (P : Polynomial F) : 0 ≤ polyPrimeCost P :=
 119  Jcost_nonneg (polyNorm_pos P)
 120
 121/-- `polyCost` is nonnegative on any polynomial. -/
 122theorem polyCost_nonneg (f : Polynomial F) : 0 ≤ polyCost f := by
 123  unfold polyCost
 124  apply Multiset.sum_nonneg
 125  intro x hx
 126  obtain ⟨P, _, hP_eq⟩ := Multiset.mem_map.mp hx
 127  rw [← hP_eq]
 128  exact polyPrimeCost_nonneg P
 129
 130/-! ## Multiplicativity over factorization -/
 131
 132/-- The total cost is additive under multiplication of nonzero polynomials.
 133    This is the function-field analog of `costSpectrumValue_mul`. -/
 134theorem polyCost_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
 135    polyCost (f * g) = polyCost f + polyCost g := by
 136  unfold polyCost
 137  rw [normalizedFactors_mul hf hg]
 138  rw [Multiset.map_add, Multiset.sum_add]
 139
 140/-! ## Cost on irreducibles and powers -/
 141
 142/-- For a monic irreducible polynomial `P`, the cost equals `J(‖P‖)`.
 143    Mathlib's `normalizedFactors` returns the multiset of monic
 144    irreducible factors. -/
 145theorem polyCost_irreducible {P : Polynomial F}
 146    (hP_irr : Irreducible P) (hP_monic : P.Monic) :
 147    polyCost P = polyPrimeCost P := by
 148  unfold polyCost
 149  rw [normalizedFactors_irreducible hP_irr]
 150  have hP_ne : P ≠ 0 := hP_irr.ne_zero
 151  have h_norm : normalize P = P :=
 152    (normalize_eq_self_iff_monic hP_ne).mpr hP_monic
 153  rw [h_norm]
 154  simp
 155
 156/-- Cost on a power: `c(P^k) = k · c(P)` for any nonzero `P`. -/
 157theorem polyCost_pow {P : Polynomial F} (hP : P ≠ 0) (k : ℕ) :
 158    polyCost (P ^ k) = (k : ℝ) * polyCost P := by
 159  induction k with
 160  | zero => simp [polyCost_one]
 161  | succ k ih =>
 162    have hPk : P ^ k ≠ 0 := pow_ne_zero k hP
 163    rw [pow_succ, polyCost_mul hPk hP, ih]
 164    push_cast
 165    ring
 166
 167/-- Cost is monotonic under multiplication by nonzero polynomials. -/
 168theorem polyCost_le_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
 169    polyCost f ≤ polyCost (f * g) := by
 170  rw [polyCost_mul hf hg]
 171  have := polyCost_nonneg g
 172  linarith
 173
 174/-! ## Strict positivity for non-units -/
 175
 176/-- An irreducible polynomial over a field has positive `natDegree`.
 177    A polynomial with `natDegree = 0` is either zero or a unit;
 178    irreducibles are neither. -/
 179private lemma irreducible_natDegree_pos {P : Polynomial F}
 180    (hP_irr : Irreducible P) : 0 < P.natDegree := by
 181  rw [Nat.pos_iff_ne_zero]
 182  intro h_zero
 183  have hP_ne : P ≠ 0 := hP_irr.ne_zero
 184  -- natDegree = 0 ⟹ P = C (coeff P 0).
 185  obtain ⟨c, hc⟩ := Polynomial.natDegree_eq_zero.mp h_zero
 186  -- coeff P 0 ≠ 0 because P ≠ 0.
 187  have hc_ne : c ≠ 0 := by
 188    intro h_c_zero
 189    apply hP_ne
 190    rw [← hc, h_c_zero]
 191    simp
 192  -- A constant polynomial with nonzero constant is a unit in F[X].
 193  have hP_unit : IsUnit P := by
 194    rw [← hc]
 195    exact Polynomial.isUnit_C.mpr (isUnit_iff_ne_zero.mpr hc_ne)
 196  exact hP_irr.not_isUnit hP_unit
 197
 198/-- If `f` is a nonzero non-unit polynomial over a field with `q ≥ 2`,
 199    then `polyCost f > 0`. -/
 200theorem polyCost_pos {f : Polynomial F}
 201    (hf : f ≠ 0) (h_not_unit : ¬ IsUnit f)
 202    (hF : 2 ≤ Fintype.card F) :
 203    0 < polyCost f := by
 204  -- Since f is a nonzero non-unit, normalizedFactors f is nonempty.
 205  have h_factors_ne : normalizedFactors f ≠ 0 := by
 206    intro h_empty
 207    have h_prod : (normalizedFactors f).prod = normalize f :=
 208      prod_normalizedFactors_eq hf
 209    rw [h_empty, Multiset.prod_zero] at h_prod
 210    have h_norm_unit : IsUnit (normalize f) := h_prod ▸ isUnit_one
 211    have h_f_unit : IsUnit f :=
 212      (associated_normalize f).symm.isUnit h_norm_unit
 213    exact h_not_unit h_f_unit
 214  -- Pick a factor P from normalizedFactors f.
 215  obtain ⟨P, hP_mem⟩ := Multiset.exists_mem_of_ne_zero h_factors_ne
 216  have hP_irr : Irreducible P := irreducible_of_normalized_factor P hP_mem
 217  have hP_deg : 0 < P.natDegree := irreducible_natDegree_pos hP_irr
 218  have hP_pos : 0 < polyPrimeCost P := polyPrimeCost_pos hP_deg hF
 219  -- Decompose the multiset sum: P contributes hP_pos, others ≥ 0.
 220  unfold polyCost
 221  have h_decomp :
 222      (normalizedFactors f).map polyPrimeCost
 223        = polyPrimeCost P ::ₘ ((normalizedFactors f).erase P).map polyPrimeCost := by
 224    rw [← Multiset.map_cons polyPrimeCost P]
 225    congr 1
 226    exact (Multiset.cons_erase hP_mem).symm
 227  rw [h_decomp, Multiset.sum_cons]
 228  apply add_pos_of_pos_of_nonneg hP_pos
 229  apply Multiset.sum_nonneg
 230  intro x hx
 231  obtain ⟨Q, _, hQ_eq⟩ := Multiset.mem_map.mp hx
 232  rw [← hQ_eq]
 233  exact polyPrimeCost_nonneg Q
 234
 235/-! ## Cost spectrum certificate -/
 236
 237/-- Master certificate: the elementary properties of the polynomial
 238    cost spectrum.  Mirrors `cost_spectrum_certificate` from the integer
 239    module.  Used by the companion paper. -/
 240theorem cost_spectrum_poly_certificate :
 241    -- (1) Per-irreducible cost is strictly positive (positive degree, q ≥ 2).
 242    (∀ {P : Polynomial F}, 0 < P.natDegree → 2 ≤ Fintype.card F →
 243      0 < polyPrimeCost P) ∧
 244    -- (2) Cost is zero at the unit polynomial 1.
 245    (polyCost (1 : Polynomial F) = 0) ∧
 246    -- (3) Cost is nonnegative everywhere.
 247    (∀ (f : Polynomial F), 0 ≤ polyCost f) ∧
 248    -- (4) Cost is strictly positive on non-units (q ≥ 2).
 249    (∀ {f : Polynomial F}, f ≠ 0 → ¬ IsUnit f → 2 ≤ Fintype.card F →
 250      0 < polyCost f) ∧
 251    -- (5) Cost is completely additive over nonzero products.
 252    (∀ {f g : Polynomial F}, f ≠ 0 → g ≠ 0 →
 253      polyCost (f * g) = polyCost f + polyCost g) ∧
 254    -- (6) Cost on a monic irreducible equals its prime cost.
 255    (∀ {P : Polynomial F}, Irreducible P → P.Monic →
 256      polyCost P = polyPrimeCost P) ∧
 257    -- (7) Cost on a power: c(P^k) = k · c(P) for any nonzero P.
 258    (∀ {P : Polynomial F} (_ : P ≠ 0) (k : ℕ),
 259      polyCost (P ^ k) = (k : ℝ) * polyCost P) :=
 260  ⟨@polyPrimeCost_pos F _ _ _,
 261   polyCost_one,
 262   polyCost_nonneg,
 263   @polyCost_pos F _ _ _,
 264   @polyCost_mul F _ _ _,
 265   @polyCost_irreducible F _ _ _,
 266   @polyCost_pow F _ _ _⟩
 267
 268end
 269
 270end PrimeCostSpectrumPoly
 271end NumberTheory
 272end IndisputableMonolith
 273