Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144CaseIIOddFinalClosure

theorem MathlibNt.SieveTheory.lemma144_caseII_odd_claim145_scaling_bridge (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C K C145 : } (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC : 0 < C) (hK : 0 < K) (hC145 : 0 < C145) :

The quantitative Case-II bracket gap, Claim 14.5 at the moving source endpoint, full Claim 14.6(i), and Euler-product monotonicity give the exact same-C odd endpoint scaling bridge. The cutoff is chosen before s.