The bounded-parameter section loses only O_m(d²) in logarithmic height. The resulting nonzero integer witness fits the fourth-power prime cutoff.

theorem CCDN.integerPlaneHeight_one_le (m d : ℕ) (hd : 1 ≤ d) (H : ℝ) (hH : 1 ≤ H) : 1 ≤ integerPlaneHeight m d H (2 * ↑d ^ 3)

For d ≥ 1 and H ≥ 1, the interpolation height integerPlaneHeight m d H (2 * d ^ 3) is at least 1.

def CCDN.hypersurfaceHeightConstant (m : ℕ) : ℝ

A dimension-dependent constant at the d⁴ cutoff.

Equations

• CCDN.hypersurfaceHeightConstant m = 28 * (↑m + 12)

theorem CCDN.hypersurfaceHeightConstant_one_le (m : ℕ) : 1 ≤ hypersurfaceHeightConstant m

The constant hypersurfaceHeightConstant m is at least 1.

theorem CCDN.integerPlaneHeight_scaled_log_le (m d : ℕ) (hd : 1 ≤ d) (H : ℝ) (hH : 1 ≤ H) : Real.log (integerPlaneHeight m d H (2 * ↑d ^ 3)) + 27 * ↑d ^ 4 * (1 + Real.log (integerPlaneHeight m d H (2 * ↑d ^ 3)) / ↑d ^ 2) ≤ 27 * ↑d ^ 4 * (hypersurfaceHeightConstant m * (1 + Real.log H / ↑d ^ 2))

For d ≥ 1 and H ≥ 1, with L the logarithm of the interpolation height integerPlaneHeight m d H (2 * d ^ 3), the quantity L + 27 d⁴ (1 + L / d²) is at most 27 d⁴ · hypersurfaceHeightConstant m · (1 + log H / d²).