theorem MathlibNt.SieveTheory.caseII_rounded_transportErr_le_positiveDelta_relative_packet_sourceLarge_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) (hP : 3 ≤ C * Real.exp √K) (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 + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * caseIIEndpointRelativeCoeffSourceLarge N (↑D) Δ σ K)

Exact-ratio, scale-free rounded transport packet for the source-large branch.