Import CCDN dimension growth and uniform point-counting bounds

LeanPool/CCDN.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+public import LeanPool.CCDN.AffineCurveBound
+public import LeanPool.CCDN.AffineHypersurfaceDimensionGrowth
+public import LeanPool.CCDN.ClassGroupBound
+public import LeanPool.CCDN.ProjectiveCurveBound
+public import LeanPool.CCDN.ProjectiveDimensionGrowth
+public import LeanPool.CCDN.ProjectiveCurveLowerBound
+
+/-!
+# Polynomial degree bounds for rational points on varieties
+
+Source: arxiv:1904.13109, doi:10.2140/ant.2020.14.2261, url:https://github.com/jasondavies/ccdn-dimension-growth/tree/bb025e7207f3a35a21b898629f5678b72aa7e44f
+Authors: Jason Davies, Ralf Stephan, PrimeNumberTheoremAnd contributors
+Status: verified
+Main declarations: `CCDN.projective_dimension_growth`
+Tags: arithmetic-geometry, rational-points, determinant-method, class-groups
+MSC: 11D45, 14G05, 11R29
+-/
+
+-- Dependency licenses and upstream notices are recorded in CCDN/Attribution.lean.

LeanPool/CCDN/AffineCurveBound.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+/- Modified for Lean Pool: module paths, toolchain compatibility, and quality repairs.
+Upstream: jasondavies/ccdn-dimension-growth @ bb025e7207f3a35a21b898629f5678b72aa7e44f. -/
+
+public import LeanPool.CCDN.Statements
+import LeanPool.CCDN.Curve.AffineCurveCount
+
+/-! The full coefficient-uniform affine curve counting theorem, with constants
+depending only on ambient dimension and with the exact degree dependence in
+CCDN Theorem 3. The proof is `affine_curve_count`, in `CCDN.Curve.AffineCurveCount`. -/
+
+@[expose] public section
+namespace CCDN
+noncomputable section
+open MvPolynomial
+
+/-- The affine curve counting bound `AffineCurveBound` of CCDN Theorem 3. -/
+theorem affineCurveBound : AffineCurveBound :=
+  affine_curve_count
+
+end
+end CCDN

LeanPool/CCDN/AffineHypersurfaceDimensionGrowth.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+/- Modified for Lean Pool: module paths, toolchain compatibility, and quality repairs.
+Upstream: jasondavies/ccdn-dimension-growth @ bb025e7207f3a35a21b898629f5678b72aa7e44f. -/
+
+public import LeanPool.CCDN.Statements
+import LeanPool.CCDN.Hypersurface.AffineHypersurfaceCount
+
+/-! CCDN Theorem 4 with the corrected degree exponent of Remark 4.3.8.
+In `N = n + 3` variables the exponent is `18 + 3n = 3N + 9`: the corrected surface
+bound `d^18` and a cost of `d^3` for each bounded good hyperplane slice
+(`affineHypersurfaceGrowth`, in `CCDN.Hypersurface.AffineHypersurfaceCount`). -/
+
+@[expose] public section
+namespace CCDN
+noncomputable section
+open MvPolynomial
+
+/-- CCDN Theorem 4 for integer equations in all affine ambient dimensions
+at least three. The constant depends only on dimension, and the explicit
+degree exponent is 18 + 3n in n+3 variables. -/
+theorem affine_hypersurface_dimension_growth (n : ℕ) :
+    ∃ C : ℝ, 0 < C ∧
+      ∀ f : MvPolynomial (Fin (n + 3)) ℤ,
+      HasAbsIrreducibleTopForm f →
+      5 ≤ f.totalDegree → ∀ B : ℝ, 1 ≤ B →
+      (count (zeroLocus (map (Int.castRingHom ℚ) f)) B : ℝ) ≤
+        C * (f.totalDegree : ℝ) ^ (18 + 3 * n) * B ^ (n + 1) :=
+  affineHypersurfaceGrowth n
+
+/-- CCDN Theorem 4 for rational equations, with the degree exponent 18 + 3n in
+n+3 variables. -/
+theorem affine_hypersurface_dimension_growth_rat (n : ℕ) :
+    ∃ C : ℝ, 0 < C ∧
+      ∀ f : MvPolynomial (Fin (n + 3)) ℚ,
+      HasAbsIrreducibleTopFormRat f →
+      5 ≤ f.totalDegree → ∀ B : ℝ, 1 ≤ B →
+      (count (zeroLocus f) B : ℝ) ≤
+        C * (f.totalDegree : ℝ) ^ (18 + 3 * n) * B ^ (n + 1) :=
+  (affineHypersurfaceGrowth n).rational
+
+end
+end CCDN

LeanPool/CCDN/Algebra/AffineLineLeading.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+/- Modified for Lean Pool: module paths, toolchain compatibility, and quality repairs.
+Upstream: jasondavies/ccdn-dimension-growth @ bb025e7207f3a35a21b898629f5678b72aa7e44f. -/
+
+public import Mathlib.RingTheory.MvPolynomial.Homogeneous
+
+/-! The coefficient of highest possible degree on an affine line depends only
+on the top homogeneous component and the direction, not the base point. -/
+
+@[expose] public section
+namespace CCDN
+noncomputable section
+
+private lemma polynomial_coeff_prod_sum_of_natDegree_le
+    {R ι : Type*} [CommRing R] (s : Finset ι) (q : ι → Polynomial R) (e : ι → ℕ)
+    (hq : ∀ i ∈ s, (q i).natDegree ≤ e i) :
+    (∏ i ∈ s, q i).coeff (∑ i ∈ s, e i) = ∏ i ∈ s, (q i).coeff (e i) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert i s hi ih =>
+    rw [Finset.prod_insert hi, Finset.sum_insert hi, Finset.prod_insert hi]
+    have ht : (∏ j ∈ s, q j).natDegree ≤ ∑ j ∈ s, e j :=
+      (Polynomial.natDegree_prod_le _ _).trans
+        (Finset.sum_le_sum fun j hj => hq j (Finset.mem_insert_of_mem hj))
+    rw [Polynomial.coeff_mul_add_eq_of_natDegree_le
+      (hq i (Finset.mem_insert_self _ _)) ht,
+      ih (fun j hj => hq j (Finset.mem_insert_of_mem hj))]
+
+/-- The affine polynomial `C a + C b * X` has degree at most `1`. -/
+lemma polynomial_affine_natDegree_le {R : Type*} [CommRing R] (a b : R) :
+    (Polynomial.C a + Polynomial.C b * Polynomial.X).natDegree ≤ 1 := by
+  apply Polynomial.natDegree_add_le_of_degree_le
+  · simp
+  · exact Polynomial.natDegree_mul_le.trans (by simpa using (Polynomial.natDegree_X_le (R := R)))
+
+/-- Restriction to the affine line a+t*b. -/
+def affineLinePolynomial {R σ : Type*} [CommRing R] (a b : σ → R) :
+    MvPolynomial σ R →+* Polynomial R :=
+  MvPolynomial.eval₂Hom Polynomial.C
+    (fun i => Polynomial.C (a i) + Polynomial.C (b i) * Polynomial.X)
+
+private lemma affineLinePolynomial_monomial_top {R σ : Type*} [CommRing R]
+    (a b : σ → R) (m : σ →₀ ℕ) (c : R) (d : ℕ) (hd : m.degree ≤ d) :
+    (affineLinePolynomial a b (MvPolynomial.monomial m c)).coeff d =
+      if d = m.degree then c * m.prod (fun i e => b i ^ e) else 0 := by
+  classical
+  let q : σ → Polynomial R := fun i => Polynomial.C (a i) + Polynomial.C (b i) * Polynomial.X
+  have hq (i : σ) : (q i).natDegree ≤ 1 := polynomial_affine_natDegree_le _ _
+  have hp (i : σ) : ((q i) ^ m i).natDegree ≤ m i := by
+    exact Polynomial.natDegree_pow_le.trans (by simpa using Nat.mul_le_mul_left (m i) (hq i))
+  have hprod : (m.prod (fun i e => (q i) ^ e)).natDegree ≤ m.degree :=
+    (Polynomial.natDegree_prod_le _ _).trans (Finset.sum_le_sum fun i _ => hp i)
+  rw [affineLinePolynomial, MvPolynomial.eval₂Hom_monomial]
+  change (Polynomial.C c * m.prod (fun i e => (q i) ^ e)).coeff d = _
+  rw [Polynomial.coeff_C_mul]
+  by_cases he : d = m.degree
+  · rw [ite_eq_left he, he]
+    congr 1
+    simp only [Finsupp.prod]
+    rw [show m.degree = ∑ i ∈ m.support, m i from rfl,
+      polynomial_coeff_prod_sum_of_natDegree_le m.support (fun i => q i ^ m i) m (fun i _ => hp i)]
+    apply Finset.prod_congr rfl
+    intro i _
+    have hh := Polynomial.coeff_pow_of_natDegree_le (m := m i) (hq i)
+    simpa only [mul_one, q, Polynomial.coeff_add, Polynomial.coeff_C_succ,
+      Polynomial.coeff_C_mul_X, zero_add, ite_true] using hh
+  · rw [ite_eq_right he,
+      Polynomial.coeff_eq_zero_of_natDegree_lt (hprod.trans_lt (by omega)), mul_zero]
+
+/-- At any degree at least the total degree, the affine-line coefficient equals
+the corresponding homogeneous component evaluated on its direction. -/
+theorem affineLinePolynomial_top_coefficient {R σ : Type*} [CommRing R]
+    (a b : σ → R) (f : MvPolynomial σ R) (d : ℕ) (hd : f.totalDegree ≤ d) :
+    (affineLinePolynomial a b f).coeff d =
+      MvPolynomial.eval b (MvPolynomial.homogeneousComponent d f) := by
+  classical
+  conv_lhs => rw [f.as_sum]
+  conv_rhs => rw [f.as_sum]
+  simp only [map_sum, Polynomial.finsetSum_coeff]
+  apply Finset.sum_congr rfl
+  intro m hm
+  rw [affineLinePolynomial_monomial_top a b m _ d ((MvPolynomial.le_totalDegree hm).trans hd),
+    MvPolynomial.homogeneousComponent_of_mem (MvPolynomial.isHomogeneous_monomial _ rfl)]
+  split_ifs <;> simp [MvPolynomial.eval_monomial]
+
+end
+end CCDN

LeanPool/CCDN/Algebra/AffineTranslation.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+/- Modified for Lean Pool: module paths, toolchain compatibility, and quality repairs.
+Upstream: jasondavies/ccdn-dimension-growth @ bb025e7207f3a35a21b898629f5678b72aa7e44f. -/
+
+public import LeanPool.CCDN.Algebra.HomogeneousChart
+public import LeanPool.CCDN.Algebra.HomogeneousTranslation
+public import LeanPool.CCDN.Algebra.OriginShift
+
+/-! The affine translations underlying the homogeneous coordinate changes
+preserve degree and irreducibility, over every coefficient field. -/
+
+@[expose] public section
+namespace CCDN
+noncomputable section
+open MvPolynomial
+
+/-- The translation `X j ↦ X j + a j` of polynomials in `Fin n` variables, as an algebra
+automorphism over `R`. -/
+def affineTranslation (R : Type*) [CommRing R] {n : ℕ} (a : Fin n → R) :
+    MvPolynomial (Fin n) R ≃ₐ[R] MvPolynomial (Fin n) R :=
+  originShiftEquiv a
+
+/-- An affine translation of variables preserves and reflects irreducibility. -/
+lemma affineTranslation_irreducible_iff {R : Type*} [CommRing R] {n : ℕ}
+    (a : Fin n → R) (f : MvPolynomial (Fin n) R) :
+    Irreducible (affineTranslation R a f) ↔ Irreducible f :=
+  MulEquiv.irreducible_iff (f := affineTranslation R a)
+
+/-- An affine translation of variables does not increase the total degree. -/
+lemma affineTranslation_totalDegree_le {R : Type*} [CommRing R] [Nontrivial R] {n : ℕ}
+    (a : Fin n → R) (f : MvPolynomial (Fin n) R) :
+    (affineTranslation R a f).totalDegree ≤ f.totalDegree := by
+  classical
+  have hm (m : Fin n →₀ ℕ) (c : R) :
+      (affineTranslation R a (monomial m c)).totalDegree ≤ m.sum (fun _ e => e) := by
+    change (aeval (fun j => X j + C (a j)) (monomial m c)).totalDegree ≤ _
+    rw [aeval_monomial]
+    have hp : (m.prod (fun j e => (X j + C (a j)) ^ e)).totalDegree ≤ m.sum (fun _ e => e) := by
+      apply (totalDegree_finsetProd _ _).trans
+      apply Finset.sum_le_sum
+      intro j _
+      have hh : (X j + C (a j) : MvPolynomial (Fin n) R).totalDegree ≤ 1 := by
+        exact (totalDegree_add _ _).trans (by simp)
+      exact (totalDegree_pow _ _).trans (by simpa using Nat.mul_le_mul_left (m j) hh)
+    have hh := totalDegree_mul (C c) (m.prod (fun j e => (X j + C (a j)) ^ e))
+    simp only [totalDegree_C, zero_add] at hh
+    exact hh.trans hp
+  conv_lhs => rw [f.as_sum, map_sum]
+  apply totalDegree_finsetSum_le
+  intro m hm'
+  exact (hm m _).trans (le_totalDegree hm')
+
+/-- An affine translation of variables preserves the total degree over a nontrivial ring. -/
+lemma affineTranslation_totalDegree {R : Type*} [CommRing R] [Nontrivial R] {n : ℕ}
+    (a : Fin n → R) (f : MvPolynomial (Fin n) R) :
+    (affineTranslation R a f).totalDegree = f.totalDegree := by
+  apply le_antisymm (affineTranslation_totalDegree_le a f)
+  have hh := affineTranslation_totalDegree_le (-a) (affineTranslation R a f)
+  have he : affineTranslation R (-a) (affineTranslation R a f) = f :=
+    (affineTranslation R a).symm_apply_apply f
+  rwa [he] at hh
+
+/-- Affine translation commutes with mapping coefficients along a ring homomorphism `φ`, the
+translation vector being mapped by `φ` as well. -/
+lemma affineTranslation_map {R S : Type*} [CommRing R] [CommRing S] {n : ℕ}
+    (φ : R →+* S) (a : Fin n → R) (f : MvPolynomial (Fin n) R) :
+    MvPolynomial.map φ (affineTranslation R a f) =
+      affineTranslation S (φ ∘ a) (MvPolynomial.map φ f) :=
+  originShift_map φ a f
+
+/-- Dehomogenizing at `X 0` intertwines the homogeneous translation
+`Xⱼ₊₁ ↦ Xⱼ₊₁ + aⱼ X₀` with the affine translation `Xⱼ ↦ Xⱼ + aⱼ`. -/
+lemma affineChart_homogeneousTranslation {R : Type*} [CommRing R] {n : ℕ}
+    (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) :
+    affineChart n (homogeneousTranslation R a f) = affineTranslation R a (affineChart n f) := by
+  have he : (affineChart n).comp (homogeneousTranslation R a).toRingHom =
+      (affineTranslation R a).toRingHom.comp (affineChart n) := by
+    apply MvPolynomial.ringHom_ext
+    · intro c
+      simp [affineChart, homogeneousTranslation, homogeneousTranslationHom, affineTranslation]
+    · intro i
+      refine Fin.cases ?_ (fun j => ?_) i <;>
+        simp [affineChart, homogeneousTranslation, homogeneousTranslationHom, affineTranslation]
+  exact RingHom.congr_fun he f
+
+end
+end CCDN

LeanPool/CCDN/Algebra/BinaryHomogeneousIrreducibility.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+/- Modified for Lean Pool: module paths, toolchain compatibility, and quality repairs.
+Upstream: jasondavies/ccdn-dimension-growth @ bb025e7207f3a35a21b898629f5678b72aa7e44f. -/
+
+public import Mathlib.FieldTheory.IsAlgClosed.Basic
+public import Mathlib.RingTheory.MvPolynomial.Homogeneous
+import LeanPool.CCDN.Algebra.HomogeneousChartIrreducible
+
+/-! Over an algebraically closed field, an irreducible homogeneous binary
+form has degree one. The affine chart reduces this to a univariate polynomial. -/
+
+@[expose] public section
+namespace CCDN
+noncomputable section
+open MvPolynomial
+
+private theorem uniqueAlgEquiv_natDegree {R σ : Type*} [CommRing R] [Unique σ]
+    (f : MvPolynomial σ R) :
+    ((uniqueAlgEquiv R σ) f).natDegree = f.totalDegree := by
+  classical
+  apply le_antisymm
+  · apply Polynomial.natDegree_le_iff_coeff_eq_zero.mpr
+    intro k hk
+    rw [coeff_uniqueAlgEquiv]
+    apply coeff_eq_zero_of_totalDegree_lt
+    change f.totalDegree < (Finsupp.single (default : σ) k).degree
+    rwa [Finsupp.degree_single]
+  · unfold totalDegree
+    apply Finset.sup_le
+    intro m hm
+    have hc : ((uniqueAlgEquiv R σ) f).coeff (m default) ≠ 0 := by
+      rw [coeff_uniqueAlgEquiv, ← Finsupp.unique_single m]
+      exact mem_support_iff.mp hm
+    have hle := Polynomial.le_natDegree_of_ne_zero hc
+    have he : m.degree = m default := by
+      calc
+        _ = (Finsupp.single default (m default)).degree :=
+          congrArg Finsupp.degree (Finsupp.unique_single m)
+        _ = _ := Finsupp.degree_single _ _
+    change m.degree ≤ _
+    rwa [he]
+
+/-- Over an algebraically closed field, an irreducible homogeneous polynomial in two variables
+has degree at most `1`. -/
+theorem binary_homogeneous_irreducible_degree_le_one
+    {K : Type*} [Field K] [IsAlgClosed K] {d : ℕ}
+    (f : MvPolynomial (Fin 2) K) (hf : f.IsHomogeneous d)
+    (hir : Irreducible f) : d ≤ 1 := by
+  by_contra h
+  have hd : 2 ≤ d := by omega
+  have hX := variable_not_dvd_irreducible_homogeneous f hf hir hd 0
+  have hdeg := affineChart_degree_of_not_variable_dvd f hf hX
+  have hc := affineChart_irreducible_of_not_variable_dvd f hf hir hX
+  have hu : Irreducible ((uniqueAlgEquiv K (Fin 1)) (affineChart 1 f)) :=
+    (MulEquiv.irreducible_iff (f := (uniqueAlgEquiv K (Fin 1)).toMulEquiv)).mpr hc
+  have hh : ((uniqueAlgEquiv K (Fin 1)) (affineChart 1 f)).natDegree = 1 :=
+    Polynomial.natDegree_eq_of_degree_eq_some
+      (IsAlgClosed.degree_eq_one_of_irreducible K hu)
+  rw [uniqueAlgEquiv_natDegree, hdeg] at hh
+  omega
+
+end
+end CCDN