theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_argument_mem {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : (1 / 2 - u) / (4 / 53) ∈ Set.Icc (53 / 24) (45 / 8)

Exact argument range of the unchanged S3 integrand.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_intervalIntegrable {β : ℝ} (hβ : 4 / 53 ≤ β) (hβu : β ≤ 1 / 3) : IntervalIntegrable (fun (u : ℝ) => suzukiContinuousUpperFactor ((1 / 2 - u) / (4 / 53)) / u) MeasureTheory.volume (4 / 53) β

Compact integrability of the literal production kernel, not a surrogate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_cancel_first {s : ℝ} (hs : 3 / 2 ≤ s) (hs3 : s ≤ 3) : Real.exp (-Real.eulerMascheroniConstant) * suzukiContinuousUpperFactor s = 2 / s

First branch, with the genuine amplitude cancelled exactly.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_cancel_second {s : ℝ} (hs : 3 ≤ s) (hs5 : s ≤ 5) : Real.exp (-Real.eulerMascheroniConstant) * suzukiContinuousUpperFactor s = 2 / s * (1 + SwitchingPrinciple.jurkatRichertInnerIntegral s)

Second branch, with no source-contract premise exposed to the consumer.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_cancel_third {s : ℝ} (hs : 5 ≤ s) (hs7 : s ≤ 7) : Real.exp (-Real.eulerMascheroniConstant) * suzukiContinuousUpperFactor s = 2 / s * (1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1))

Third branch in exact integrated-lower form, with exp(gamma) cancelled. The nested integral is retained, including its nonzero correction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_change_variable (β : ℝ) : goldbachS3_primeKernelIntegral β = ∫ (s : ℝ) in (1 / 2 - β) / (4 / 53)..45 / 8, suzukiContinuousUpperFactor s / (53 / 8 - s)

Affine change of variables for the literal production integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_free {β : ℝ} (hβ : 4 / 53 ≤ β) (hβu : β ≤ 1 / 3) : 53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral β = 53 * ∫ (s : ℝ) in (1 / 2 - β) / (4 / 53)..45 / 8, (if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))

Exact exp-free reduction on the whole admissible beta range. The third branch retains the full iterated lower-factor correction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_cancel {s : ℝ} (hs : 3 / 2 ≤ s) (hs7 : s ≤ 7) : Real.exp (-Real.eulerMascheroniConstant) * suzukiContinuousUpperFactor s = 2 / s * if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)

All three actual source branches, glued without changing the factor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_exp_free_continuousOn : ContinuousOn (fun (s : ℝ) => (if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))) (Set.Icc (53 / 24) (45 / 8))

Genuine continuity of the exp-free expression, including both joins. Thus the change of variables is not exploiting a nonintegrable zero value.