theorem MathlibNt.SieveTheory.caseII_rounded_transportErr_le_positiveDelta_relative_packet_fixed_coefficients (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {yr zr d Δ σ C K B0 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hD : Real.exp 1 ≤ ↑D) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hσ : 3 ≤ σ) (hs1 : 1 < s) (hK : 0 ≤ K) (hC : 0 ≤ C) (hsmall : 3 ^ d ≤ Real.log ↑D) (hE : 1 / 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (hyr : yr = ↑D ^ (1 / 3)) (hzr : zr = ↑D ^ (1 / s)) (hz : z = ⌈zr⌉₊) : caseIIRoundedTransportErr S H N (↑D) yr zr d Δ σ C K B0 s + SwitchingPrinciple.suzukiVProduct S ↑z * (K * 3 ^ 2 / (s * Real.log ↑D)) ≤ B0 + SwitchingPrinciple.suzukiVProduct S ↑z * (caseIIPositiveDeltaIntegralPart H N (↑D) yr d Δ σ C K s + (caseIIAlgebraicEndpointCoeffA0 N K * Real.log ↑D ^ (Δ - 1) + σ * caseIIAlgebraicEndpointCoeffA1 N K * Real.log ↑D ^ (Δ - 1) + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log ↑D + 27 * K * Real.log ↑D ^ (Δ - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) * Real.log ↑D ^ (-Δ))

The rounded transport remainder, together with the sharp source-base term, is absorbed by the canonical rounded positive-Δ endpoint packet. The proof expands caseIIEndpointSigma11 and caseIIEndpointQD: the integral summand is identified exactly with caseIIPositiveDeltaIntegralPart, while the three remaining summands pay the fixed coefficients A0, σ*A1, and σ*Aq0.