theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_three_le_perturb_three_mul_lambda_caseII {H : Section13HatLayers} {D d s : ℝ} (hH : Section13HatContract H 2) (hD : 1 < D) (_hd : 0 ≤ d) (hs : 0 < s) (hs3 : s ≤ 3) : lambda H ErrorSign.plus D d 0 3 ≤ perturbation D d 0 3 * lambda H ErrorSign.plus D d 0 s

On the odd Case-II initial interval, the cubic-endpoint lambda is bounded by one explicit perturbation factor times the current lambda. A factor one would have the wrong direction in general.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_integral_absorb_with_lambda_ratio {H : Section13HatLayers} {N : ℕ} {D d Δ σ s R : ℝ} (hs : 0 < s) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (_hR : 0 ≤ R) (hiii : ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * lambda H (ErrorSign.ofDepth N) D d 0 3) (hLambda3 : lambda H (ErrorSign.ofDepth N) D d 0 3 ≤ R * lambda H (ErrorSign.ofDepth N) D d 0 s) : 1 / s * ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * R * errorEnvelope H N D d s

Correct Case-II integral absorption with an explicit short-interval lambda ratio. This replaces the generally false factor-one comparison lambda(3) ≤ lambda(s).