theorem MathlibNt.SieveTheory.caseI_claim145Scale_le_transported_remainderUnit (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {C CB K d Δ s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD3 : 3 ≤ D) (hC : 0 < C) (hCB : 0 ≤ CB) (hs : 1 ≤ s) (hsσ : s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) (htransport : SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) : CB * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ CB / C * caseI1423RemainderUnit (sigma12InheritedBudget S H N D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s) (↑D) (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Pointwise normalization of the Claim-14.5 endpoint into the budget at s. The Claim-14.6 transport is supplied at this same D; no new eventual cutoff is selected here. This applies to both the strict Case-I range and s = 2.

theorem MathlibNt.SieveTheory.caseI_three_remainders_le_gap {x₀ x₁ x₂ a₀ a₁ a₂ B D d ρ : ℝ} (hB : 0 ≤ B) (h₀ : x₀ ≤ a₀ * caseI1423RemainderUnit B D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) (h₁ : x₁ ≤ a₁ * caseI1423RemainderUnit B D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) (h₂ : x₂ ≤ a₂ * caseI1423RemainderUnit B D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) (hgap : caseISourceOrderCoefficient (a₀ + a₁ + a₂) D d ≤ 1 - ρ) : x₀ + x₁ + x₂ ≤ (1 - ρ) * B

Add the three independently paid endpoint terms and spend their combined source-order coefficient against the remaining contraction budget.