Singular plane-curve local determinant divisibility, obtained from finite-precision homogeneous generators of the local maximal-ideal filtration.

theorem CCDN.singular_plane_pow_dvd_det_mod {p μ s : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) ≠ 0) (x : Fin s → Fin 2 → ℤ) (hx : ∀ (i : Fin s) (j : Fin 2), ↑p ∣ x i j) (hfx : ∀ (i : Fin s), ↑p ^ multiplicityExponent s μ ∣ (MvPolynomial.eval (x i)) f) (F : Fin s → MvPolynomial (Fin 2) ℤ) : ↑p ^ multiplicityExponent s μ ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

Every square evaluation determinant of integral zeros in one singular residue class has the repeated-weight multiplicity exponent. The curve's multiplicity is determined by its reduction.

theorem CCDN.singular_plane_pow_dvd_det {p μ s : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) ≠ 0) (x : Fin s → Fin 2 → ℤ) (hx : ∀ (i : Fin s) (j : Fin 2), ↑p ∣ x i j) (hfx : ∀ (i : Fin s), (MvPolynomial.eval (x i)) f = 0) (F : Fin s → MvPolynomial (Fin 2) ℤ) : ↑p ^ multiplicityExponent s μ ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

The exact-zero form follows from finite-precision divisibility.