Case-II cutoff uniform in K on the source large-log branch

The fixed-K bracket is too coarse for the source quantifier order because it replaces 1 + 3K/log D by 1 + 3K. Here we retain the exact ratio in both finite endpoint coefficients. After the common-scale cancellation of the cubic q_D(3) term, every endpoint is bounded by O(K^2 * sourceSigma(D,d)^2 * (log D)^(Δ-1)) after multiplying by the source gap denominator. The source inequality (14.4)

2/Θ + 3/d < 1-Δ

then gives one cutoff in C1, before arbitrary K, D, and odd depth N.

noncomputable def MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracketSourceLarge (N : ℕ) (D d Δ σ K : ℝ) : ℝ

The natural-ceiling Case-II bracket. As in the production rounded assembler, natural ceilings occur in the discrete carrier; the analytic coordinates here remain the exact real roots.

Equations

• MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracketSourceLarge N D d Δ σ K = (1 + 3 * K / Real.log D) * (1 - 1 / σ) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 + MathlibNt.SieveTheory.caseIIEndpointRelativeCoeffSourceLarge N D Δ σ K

theorem MathlibNt.SieveTheory.exists_caseIIConcreteRoundedRelativeBracketSourceLarge_gap_uniform {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {d Δ Θ : ℝ} (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 K : ℝ) (N D : ℕ), C1min ≤ C1 → 2 ≤ K → 2 ≤ D → C1 * K ^ Θ < Real.log ↑D → Odd N → 3 ≤ N → 27 * (1 - Δ) / (32 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ 1 - caseIIConcreteRoundedRelativeBracketSourceLarge N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K

Quantitative source-large-log replacement for the moving rounded Case-II bracket. The witness is a lower bound for the source separator C1; it is chosen before arbitrary K, natural D, and odd recursion depth N. The conclusion retains exactly 27/32 of the source contraction gap.