All reduced points, their positive multiplicities, and the resulting local determinant lower bound. The sharp finite-field total-multiplicity estimate is a separate geometric obligation.

def CCDN.PlaneResidue (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) : Type

All affine rational points of the reduced plane equation.

Equations

• CCDN.PlaneResidue f p = { a : Fin 2 → ZMod p // MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) a f = 0 }

@[instance_reducible]

instance CCDN.instFintypePlaneResidueOfNeZeroNat (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) [NeZero p] : Fintype (PlaneResidue f p)

Equations

• CCDN.instFintypePlaneResidueOfNeZeroNat f p = id inferInstance

def CCDN.PlaneResidueCountBound (C : ℝ) (d : ℕ) (f : MvPolynomial (Fin 2) ℤ) : Prop

The finite-field point-count hypothesis for one plane equation f, with degree parameter d and constant C: at every prime p > stepanovThreshold d where f has irreducible reduction, f has at most p + C d² √p zeros in 𝔽_p². PlaneResidueBound C asserts it for every equation with d = deg f, and planeResidueBound proves it with C = planeResidueConstant.

Equations

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

def CCDN.planeResidueLift {f : MvPolynomial (Fin 2) ℤ} {p : ℕ} (a : PlaneResidue f p) : Fin 2 → ℤ

The integer lift, with coordinates in [0, p), of an 𝔽_p-point of the reduced affine plane curve.

Equations

• CCDN.planeResidueLift a j = ↑(↑a j).val

theorem CCDN.cast_planeResidueLift {f : MvPolynomial (Fin 2) ℤ} {p : ℕ} [NeZero p] (a : PlaneResidue f p) (j : Fin 2) : ↑(planeResidueLift a j) = ↑a j

The integer lift of a residue point reduces modulo p to the point itself.

theorem CCDN.planeResidueLift_zero {f : MvPolynomial (Fin 2) ℤ} {p : ℕ} [NeZero p] (a : PlaneResidue f p) : MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin 2) => ↑(planeResidueLift a j)) f = 0

The reduction of f modulo p vanishes at the reduction of the integer lift of a residue point of f.

noncomputable def CCDN.planeResidueMultiplicity (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (a : PlaneResidue f p) : ℕ

Multiplicity is selected from the translated reduced equation.

Equations

• CCDN.planeResidueMultiplicity f p hf a = Classical.choose ⋯

theorem CCDN.planeResidueMultiplicity_spec (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (a : PlaneResidue f p) : 0 < planeResidueMultiplicity f p hf a ∧ planeResidueMultiplicity f p hf a ≤ f.totalDegree ∧ (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (planeResidueLift a)) f) ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ planeResidueMultiplicity f p hf a ∧ (MvPolynomial.homogeneousComponent (planeResidueMultiplicity f p hf a)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (planeResidueLift a)) f)) ≠ 0

The multiplicity of f mod p at a residue point a is between 1 and the total degree of f; after translating a to the origin, the reduced equation lies in that power of the ideal of the origin and has a nonzero homogeneous component of that degree.

noncomputable def CCDN.planeTotalMultiplicity (f : MvPolynomial (Fin 2) ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) : ℕ

The finite-field total multiplicity appearing in the denominator of the local determinant exponent.

Equations

• CCDN.planeTotalMultiplicity f p hf = ∑ a : CCDN.PlaneResidue f p, CCDN.planeResidueMultiplicity f p hf a

theorem CCDN.singular_reduction_minorGcd {s N p : ℕ} [Fact (Nat.Prime p)] (hs : 0 < s) (f : MvPolynomial (Fin 2) ℤ) (g : Fin N → MvPolynomial (Fin 2) ℤ) (z : Fin s → Fin 2 → ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : 0 < planeTotalMultiplicity f p hf ∧ ∃ (e : ℕ), s ^ 2 ≤ 2 * planeTotalMultiplicity f p hf * (e + s) ∧ ↑s ^ 2 / (2 * ↑(planeTotalMultiplicity f p hf)) - ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k))

Integral zeros supply all residue labels and multiplicities. The sum of the local exponents has the full quadratic leading coefficient. Singular points are allowed.