Fourth-power cutoff removes the polynomial-in-degree error from the singular determinant prime sum, retaining an explicit logarithmic cutoff cost.

theorem CCDN.singular_correction_absorb {d p : ℕ} (hd : 0 < d) {L : ℝ} (hdL : ↑d ^ 4 ≤ L) (hpL : L < ↑p) : ↑(d ^ 2 * (d - 1)) ≤ ↑d ^ 2 * √↑p

For d⁴ ≤ L < p, the singular-point correction d² (d - 1) is at most d² √p.

noncomputable def CCDN.degreeFourDeterminantError (C : ℝ) : ℝ

The absolute error of the plane determinant lower bound at the cutoff stepanovThreshold d, for residue constant C (singular_determinant_log_lower_at_rank): log 27 from log (27 d⁴) = log 27 + 4 log d, 2 mertensError from Mertens' estimate, 2 primeBlockMass (C + 1) from the point-count error C d² √p and the singular correction d² (d - 1) ≤ d² √p, and 2 (log 4 + 4) from the term s (log 4 + 4) x at x = s.

Equations

• CCDN.degreeFourDeterminantError C = Real.log 27 + 2 * CCDN.mertensError + 2 * CCDN.primeBlockMass * (C + 1) + 2 * (Real.log 4 + 4)

theorem CCDN.singular_determinant_log_lower_at_rank {s N : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin 2) ℤ) (hd : 0 < f.totalDegree) (g : Fin N → MvPolynomial (Fin 2) ℤ) (z : Fin s → Fin 2 → ℤ) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (hrows : LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k)).map Int.cast).row) {C : ℝ} (hC : 0 ≤ C) (B : Finset ℕ) (hf : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 s) \ B, stepanovThreshold ↑f.totalDegree < ↑p → Irreducible ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) (hupper : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 s) \ B, stepanovThreshold ↑f.totalDegree < ↑p → ↑(Nat.card (PlaneResidue f p)) ≤ ↑p + C * ↑f.totalDegree ^ 2 * √↑p) : ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑f.totalDegree - ∑ p ∈ B, Real.log ↑p / ↑p - degreeFourDeterminantError C) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (k : Fin N) => (MvPolynomial.eval (z i)) (g k)))

Choosing the prime upper endpoint to equal the row count yields the plane-case shape of CCDN Proposition 3.2.6, with the geometric point-count and bad-prime hypotheses explicit.