theorem MathlibNt.SieveTheory.exists_caseII_source_relative_bracket_lt_one_threshold (N : ℕ) (K C d Δ : ℝ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hK : 0 ≤ K) (hC : 0 ≤ C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → (1 + 3 * K / Real.log D) * (1 - 1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 + caseIISharpPositiveEndpointRelativeCoeff N D d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) C K < 1

The complete source Case-II relative bracket is eventually strictly contractive. The integral transport excess, all four positive endpoint terms, and the source contraction gap are paid at one common explicit (finite max) threshold; no D-dependent decay premise remains.