theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.log_le_L {x : ℝ} (hx : 0 ≤ x) : Real.log (1 + x) ≤ L x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.inner_le_A {s : ℝ} (hs : 3 ≤ s) : SwitchingPrinciple.jurkatRichertInnerIntegral s ≤ A (s - 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.nested_inner_le_B {t : ℝ} (ht : 5 ≤ t) : ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v ≤ B (t - 5)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.nested_le_D {s : ℝ} (hs : 5 ≤ s) : ∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1) ≤ D (s - 5)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.correction_continuousOn {b : ℝ} (hb : 5 ≤ b) : ContinuousOn (fun (s : ℝ) => ∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) (Set.Icc 5 b)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.actual_correction_le_rational : 53 * ∫ (s : ℝ) in 5..45 / 8, (∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s)) ≤ 1972364 / 10 ^ 10

Actual third-branch correction, retaining the full exterior weight 53. No certificate parameters or target-shaped assumptions.