The local exponent at a possibly singular plane reduction, bounded by the residue-point count plus the singular correction.

theorem CCDN.singular_reduction_minorGcd_card_bound {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 → ℤ) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hchar : f.totalDegree < p) : have m := Nat.card (PlaneResidue f p) + f.totalDegree ^ 2 * (f.totalDegree - 1); 0 < m ∧ ∃ (e : ℕ), ↑s ^ 2 / (2 * ↑m) - ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k))

The local exponent can be bounded using the reduced point count and the proved degree-dependent singular correction.