theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.one_third_le_errorEnvelope_caseII {H : Section13HatLayers} {N : ℕ} {D d s : ℝ} (hH : Section13HatContract H 2) (hN : Odd N) (hD : 1 < D) (hs1 : 1 < s) (hs3 : s ≤ 3) : 1 / 3 ≤ errorEnvelope H N D d s

Uniform lower bound for the odd Case-II error envelope on 1 < s ≤ 3. This is what allows all fixed finite endpoint terms divided by log D to be absorbed uniformly as D → ∞.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_minus_three_eq {H : Section13HatLayers} {D d Δ : ℝ} (hH : Section13HatContract H 2) : qD H ErrorSign.minus D d Δ 3 = (1 + 3 ^ d / Real.log D) ^ 2 * (3 / 2) ^ Δ

At the cubic endpoint the opposite-sign q_D is completely explicit from Section 13 initial data.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_opposite_three_eq_of_odd {H : Section13HatLayers} {N : ℕ} {D d Δ : ℝ} (hH : Section13HatContract H 2) (hN : Odd N) : qD H (ErrorSign.ofDepth N).opposite D d Δ 3 = (1 + 3 ^ d / Real.log D) ^ 2 * (3 / 2) ^ Δ

In odd Case II, the endpoint q_D in the transported Case-I remainder is the explicit minus-sign cubic value.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.one_div_log_cubic_endpoint {D y : ℝ} (hD : 1 < D) (hy : y = D ^ (1 / 3)) : 1 / Real.log y = 3 / Real.log D

Exact reciprocal logarithm at the cubic cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.one_div_log_sigma_endpoint {D w σ : ℝ} (hD : 1 < D) (hσ : 0 < σ) (hw : w = D ^ (1 / σ)) : 1 / Real.log w = σ / Real.log D

Exact reciprocal logarithm at the lower σ power coordinate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation_three_le_one_add_seven_ratio {D d : ℝ} (hD : 1 < D) (hsmall : 3 ^ d ≤ Real.log D) : perturbation D d 0 3 ≤ 1 + 7 * (3 ^ d / Real.log D)

Cubic perturbation is quantitatively 1 + O(3^d / log D).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_contraction_with_cubic_perturbation {D d Δ σ : ℝ} (hσ : 1 < σ) (_hΔ : Δ < 1) (hpert : perturbation D d 0 3 ≤ 1 + (1 - (1 - 1 / σ) ^ (1 - Δ)) / (2 * (1 - 1 / σ) ^ (1 - Δ))) : (1 - 1 / σ) ^ (1 - Δ) * perturbation D d 0 3 ≤ (1 + (1 - 1 / σ) ^ (1 - Δ)) / 2

Once the cubic perturbation is smaller than half the strict Claim-14.6(iii) margin, its product with the contraction coefficient still leaves half of that margin for all finite endpoint terms.