The number of subsets and edges of a common logarithmic prime window costs only an arbitrarily small positive power of the box radius. Constants are fixed before the radius, including the bounded range near B = 1.

theorem CCDN.congruencePrimeWindow_card_log_two {L : ℝ} (hL : 1 ≤ L) : ↑(congruencePrimeWindow L).card * Real.log 2 ≤ (Real.log 4 + 4) * scalingPrimeRatio * L

For L ≥ 1, the number of primes in congruencePrimeWindow L, multiplied by log 2, is at most (log 4 + 4) c L, where c is scalingPrimeRatio.

theorem CCDN.congruencePrimeWindow_surface_residual_bound {K R : ℝ} (hK : 1 ≤ K) (hR : 1 ≤ R) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (d : ℕ), 5 ≤ d → ∀ (B : ℝ), 1 ≤ B → ↑(congruencePrimeWindow (K * (Real.log B + 1))).card * R ^ (congruencePrimeWindow (K * (Real.log B + 1))).card * B ^ (2 / √↑d) * (Real.log B + 1) ^ k ≤ C * B

For K, R ≥ 1 and k : ℕ, there is a constant C such that, for every degree d ≥ 5 and every B ≥ 1, the prime window W of logarithmic size K (log B + 1) satisfies #W R^#W B^(2/√d) (log B + 1)^k ≤ C B.