theorem
MathlibNt.SieveTheory.exists_caseII_endpoint_common_threshold_uniform
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(K C d Δ : ℝ)
(hK : 0 ≤ K)
(_hC : 0 ≤ C)
(hΔ0 : 0 < Δ)
(hΔ1 : Δ < 1)
(hd : 7 / (1 - Δ) < d)
:
The four positive Case-II endpoint terms admit one large-D threshold
uniformly for every odd depth N ≥ 3.
theorem
MathlibNt.SieveTheory.exists_caseIIConcreteRoundedRelativeBracket_gap_threshold_uniform
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(K C d Δ : ℝ)
(hK : 0 ≤ K)
(hC : 0 ≤ C)
(hΔ0 : 0 < Δ)
(hΔ1 : Δ < 1)
(hd : 7 / (1 - Δ) < d)
:
One cutoff, independent of the odd depth, preserves the quantitative
27/32 Case-II rounded-bracket gap.