The integer minor has the logarithmic height needed by the fourth-power prime cutoff. The charge applies to primes with proved matrix rank drop; identifying these with the geometric bad primes is a separate step.

theorem CCDN.closedForm_minor_log_height (d r : ℕ) (hd : 1 ≤ d) (hr : r ≤ 2 * d ^ 2) (f : Polynomial (Polynomial ℤ)) (H : ℝ) (hH : 1 ≤ H) (hf : BivariateCoefficientBound f H) (houter : f.natDegree ≤ d) (hinner : ∀ (i : ℕ), (f.coeff i).natDegree ≤ d) (a : Fin r → ℕ × ℕ) (c : Fin r → ClosedFormColumns d) (hD : ((closedFormCoefficientMatrix d f).submatrix a c).det ≠ 0) : Real.log |↑((closedFormCoefficientMatrix d f).submatrix a c).det| ≤ 27 * ↑d ^ 4 * (1 + Real.log H / ↑d ^ 2)

The determinant height fits the cutoff L=27*d^4 with scaled height 1+log(H)/d².