theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_fixed_lower_threshold (d L : ℝ) (hd : 0 ≤ d) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → L ≤ sourceSigma D d

The source cutoff eventually exceeds every fixed real number.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.fixedCompactPerturbationContract {d M : ℝ} (_hd : 0 ≤ d) (hM : 4 ≤ M) : FixedCompactPerturbationContract d M

The elementary fixed-compact perturbation input used by the source assembly.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma133WeightedHeadContract_corrected {H : Section13HatLayers} (hH : Section13HatContract H 2) {d Δ M : ℝ} (hd : 0 ≤ d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hM : 4 ≤ M) : Lemma133WeightedHeadContract H d Δ (1 - Δ) M

Corrected fixed-head source contract, with gap = 1 - Δ. All thresholds are chosen after the fixed cutoff M; no fixed-endpoint theorem is diagonalized.