Statements of the main results

The counting statements of Theorems 1–4, as propositions, together with the plane case of Theorem 3 and the hypersurface case of Theorem 1 that the proofs use as intermediate targets. This module imports only the foundation directories (the counting functions of Height/, the zero loci and degree predicates of Algebra/, and the Hilbert-function degrees of Hilbert/), so each statement can be read without the proof infrastructure.

• PlaneCurveBound: Theorem 3 for plane curves, proved in CCDN.Plane.CurveCount;
• AffineCurveBound: Theorem 3, proved in CCDN.AffineCurveBound;
• ProjectiveCurveBound: Theorem 2, proved in CCDN.ProjectiveCurveBound;
• AffineHypersurfaceGrowth and RationalAffineHypersurfaceGrowth: Theorem 4 with a given degree exponent, proved in CCDN.AffineHypersurfaceDimensionGrowth;
• ProjectiveHypersurfaceGrowth: Theorem 1 for hypersurfaces, proved in CCDN.Hypersurface.ProjectiveHypersurfaceDimensionGrowth;
• ProjectiveGrowth: Theorem 1 with a given degree exponent, proved in CCDN.ProjectiveDimensionGrowth.

Theorem 6 and Proposition 5 are stated directly by their endpoint theorems classGroup_two_torsion_bound and projective_integral_curve_lower_bound.

Theorem 3: affine curves

noncomputable def CCDN.curveBound (d : ℕ) (B : ℝ) : ℝ

The bound d³ B^(1/d) (log B + d) of Theorem 3.

Equations

• CCDN.curveBound d B = ↑d ^ 3 * B ^ (1 / ↑d) * (Real.log B + ↑d)

def CCDN.PlaneCurveBound : Prop

The n = 2 case of CCDN (2020), Theorem 3, expressed using rational defining polynomials. The proof (planeCurveBound, in CCDN.Plane.CurveCount) includes denominator clearing and content removal. Irreducibility is over ℚ, not absolute irreducibility. The one constant is uniform in the polynomial, its degree, its coefficients, and the real radius.

Equations

• One or more equations did not get rendered due to their size.

def CCDN.AffineCurveBound : Prop

CCDN (2020), Theorem 3, using the affine Hilbert function to specify degree. The constant is chosen before the ideal, degree, and real box radius.

Equations

• One or more equations did not get rendered due to their size.

Theorem 2: projective curves

noncomputable def CCDN.projectiveCurveEstimate (d : ℕ) (B : ℝ) : ℝ

The bound d⁴ B^(2/d) of Theorem 2.

Equations

• CCDN.projectiveCurveEstimate d B = ↑d ^ 4 * B ^ (2 / ↑d)

def CCDN.ProjectiveCurveBound : Prop

CCDN (2020), Theorem 2, with projective degree specified by the homogeneous Hilbert function. The constant precedes the ideal, degree and radius.

Equations

• One or more equations did not get rendered due to their size.

Theorem 4: affine hypersurfaces

def CCDN.AffineHypersurfaceGrowth (n e : ℕ) : Prop

Affine dimension growth with degree exponent e for integer equations in n + 3 variables of degree at least five whose top-degree form is absolutely irreducible. The constant depends only on n and e.

Equations

• One or more equations did not get rendered due to their size.

def CCDN.RationalAffineHypersurfaceGrowth (n e : ℕ) : Prop

The rational-equation form of AffineHypersurfaceGrowth.

Equations

• One or more equations did not get rendered due to their size.

Theorem 1: projective varieties

def CCDN.ProjectiveHypersurfaceGrowth (n e : ℕ) : Prop

Dimension growth with degree exponent e for rationally irreducible projective hypersurfaces of degree at least five in ℙ^(n+2). The height exponent is the hypersurface dimension n + 1.

Equations

• One or more equations did not get rendered due to their size.

def CCDN.ProjectiveGrowth (n E : ℕ) : Prop

CCDN Theorem 1 in ℙⁿ with degree exponent E. A homogeneous prime ideal whose Hilbert polynomial has degree r and leading coefficient d / r!, with d ≥ 5, has at most C d^E B^(r-1) rational points of height at most B. The constant depends only on n and E.

Equations

• One or more equations did not get rendered due to their size.