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)
:
Lemma144CaseIIOddClaim145ScalingBridge S H d Δ C K 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.