Multiplicity greater than one forces a singular point.
theorem
CCDN.singular_of_origin_order_ge_two
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(a : σ → K)
{μ : ℕ}
(hμ : 2 ≤ μ)
(hf : (originShift a) f ∈ MvPolynomial.idealOfVars σ K ^ μ)
(j : σ)
:
Only singular points can have local order at least two.
theorem
CCDN.origin_order_eq_one_of_smooth
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(a : σ → K)
{μ : ℕ}
(hμ : 0 < μ)
(hf : (originShift a) f ∈ MvPolynomial.idealOfVars σ K ^ μ)
(hs : ∃ (j : σ), (MvPolynomial.eval a) ((MvPolynomial.pderiv j) f) ≠ 0)
:
In particular, every positive order at a smooth point is one.
theorem
CCDN.planeTotalMultiplicity_le_card_add_correction
{p : ℕ}
[Fact (Nat.Prime p)]
(f : MvPolynomial (Fin 2) ℤ)
(hf : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f))
(hpos : 0 < ((MvPolynomial.map (Int.castRingHom (ZMod p))) f).totalDegree)
(hchar : f.totalDegree < p)
:
planeTotalMultiplicity f p ⋯ ≤ Fintype.card (PlaneResidue f p) + f.totalDegree ^ 2 * (f.totalDegree - 1)
The multiplicity correction costs only a degree-dependent constant. The leading term remains the number of finite-field points.