A degree-dependent logarithmic prime window discharges all height conditions of the surface residue cover. Its complete residual point count is O(B), uniformly in coefficients, auxiliaries and initial curve families.

noncomputable def CCDN.surfaceResidueWindowScale (d : ℕ) (K : ℝ) : ℝ

The constant 4 log (d + 1) + K + d + 2 scaling the logarithmic prime window of the residue cover for a surface of degree d with logarithmic height constant K.

Equations

• CCDN.surfaceResidueWindowScale d K = 4 * Real.log (↑d + 1) + K + ↑d + 2

noncomputable def CCDN.surfaceResidueWindow (d : ℕ) (K B : ℝ) : ℝ

The logarithmic size surfaceResidueWindowScale d K * (log B + 1) of the prime window of the residue cover for a surface of degree d in the box of radius B.

Equations

• CCDN.surfaceResidueWindow d K B = CCDN.surfaceResidueWindowScale d K * (Real.log B + 1)

noncomputable def CCDN.surfaceResidueLogScale (d : ℕ) (K : ℝ) : ℝ

The constant 1 + (log 4 + 4) c s, with c the constant scalingPrimeRatio and s the window scale surfaceResidueWindowScale d K, by which the logarithmic budget of the residue cover is a multiple of log B + 1.

Equations

• CCDN.surfaceResidueLogScale d K = 1 + (Real.log 4 + 4) * CCDN.scalingPrimeRatio * CCDN.surfaceResidueWindowScale d K

theorem CCDN.surfaceResidueWindowScale_two_le (d : ℕ) {K : ℝ} (hK : 0 ≤ K) : 2 ≤ surfaceResidueWindowScale d K

For K ≥ 0, the window scale surfaceResidueWindowScale d K is at least two.

theorem CCDN.surfaceResidueWindow_one_le (d : ℕ) {K B : ℝ} (hK : 0 ≤ K) (hB : 1 ≤ B) : 1 ≤ surfaceResidueWindow d K B

For K ≥ 0 and B ≥ 1, the prime window size surfaceResidueWindow d K B is at least one.

theorem CCDN.surfaceResidueLogScale_one_le (d : ℕ) {K : ℝ} (hK : 0 ≤ K) : 1 ≤ surfaceResidueLogScale d K

For K ≥ 0, the budget constant surfaceResidueLogScale d K is at least one.

theorem CCDN.surfaceResidueLogBudget_window (d : ℕ) (K B : ℝ) : surfaceResidueLogBudget B (surfaceResidueWindow d K B) = surfaceResidueLogScale d K * (Real.log B + 1)

For the prime window surfaceResidueWindow d K B, the logarithmic budget of the residue cover equals surfaceResidueLogScale d K * (log B + 1).

theorem CCDN.isSurfaceResidueWindow_of_log_height {f : MvPolynomial (Fin 3) ℤ} (hd : 1 ≤ f.totalDegree) {K B H : ℝ} (hK : 0 ≤ K) (hB : 1 ≤ B) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (hheight : Real.log H ≤ K * (Real.log B + 1)) : IsSurfaceResidueWindow f B H (surfaceResidueWindow f.totalDegree K B) (2 * B ^ (1 / √↑f.totalDegree))

For a surface equation of degree d ≥ 1 whose coefficients are bounded by H ≥ 1 with log H ≤ K (log B + 1), the chosen window surfaceResidueWindow d K B and the cutoff 2 B^(1/√d) are residue-cover parameters.

theorem CCDN.surface_residue_linear_count (d : ℕ) (hd : 5 ≤ d) (K A : ℝ) (hK : 0 ≤ K) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 < C ∧ ∀ (f : MvPolynomial (Fin 3) ℤ), f.totalDegree = d → ∀ (B : ℝ) (hB : 1 ≤ B) (F : SurfaceCongruenceFamily f B A), Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f) → ∀ (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ), (∀ I ∈ S, IsSurfaceCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) I (δ I)) → ↑(count (surfaceResidueResidualLocus F S (surfaceResidueWindow d K B) (2 * B ^ (1 / √↑d)) ⋯) B) ≤ C * B

The residual locus has a uniform linear count. The constant is chosen before the equation, radius, congruence auxiliaries and curve family.