theorem G67SumCoordinate.integral_weight_first {a b c d l r : ℝ} (φ : ℝ → ℝ) (hlr : l ≤ r) (hL : r ≤ a + d) (hU : r ≤ b + c) : ∫ (s : ℝ) in l..r, φ s * weight a b c d s = ∫ (s : ℝ) in l..r, φ s * (Real.log ((s - c) * (s - a) / (a * c)) / s)

Integrate the early closed branch on a certified subinterval.

theorem G67SumCoordinate.integral_weight_middle {a b c d l r : ℝ} (φ : ℝ → ℝ) (hlr : l ≤ r) (hL : r ≤ a + d) (hU : b + c ≤ l) : ∫ (s : ℝ) in l..r, φ s * weight a b c d s = ∫ (s : ℝ) in l..r, φ s * (Real.log (b * (s - a) / (a * (s - b))) / s)

Integrate the middle closed branch on a certified subinterval.

theorem G67SumCoordinate.integral_weight_last {a b c d l r : ℝ} (φ : ℝ → ℝ) (hlr : l ≤ r) (hL : a + d ≤ l) (hU : b + c ≤ l) : ∫ (s : ℝ) in l..r, φ s * weight a b c d s = ∫ (s : ℝ) in l..r, φ s * (Real.log (b * d / ((s - d) * (s - b))) / s)

Integrate the late closed branch on a certified subinterval.

theorem G67SumCoordinate.square_integral_piecewise : ∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 33 + 4 / 33, profile s * weight (4 / 53) (4 / 33) (4 / 53) (4 / 33) s = (∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 53 + 4 / 33, profile s * (Real.log ((s - 4 / 53) * (s - 4 / 53) / (4 / 53 * (4 / 53))) / s)) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 4 / 33, profile s * (Real.log (4 / 33 * (4 / 33) / ((s - 4 / 33) * (s - 4 / 33))) / s)

The square has two elementary branches, split at a+b.

theorem G67SumCoordinate.rectangle_integral_piecewise : ∫ (s : ℝ) in 4 / 53 + 4 / 33..1 / 2 - 2 * (4 / 53), profile s * weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s = (∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 4 / 33, profile s * (Real.log ((s - 4 / 33) * (s - 4 / 53) / (4 / 53 * (4 / 33))) / s)) + ((∫ (s : ℝ) in 4 / 33 + 4 / 33..4 / 53 + 3 / 11, profile s * (Real.log (4 / 33 * (s - 4 / 53) / (4 / 53 * (s - 4 / 33))) / s)) + ∫ (s : ℝ) in 4 / 53 + 3 / 11..1 / 2 - 2 * (4 / 53), profile s * (Real.log (4 / 33 * (3 / 11) / ((s - 3 / 11) * (s - 4 / 33))) / s))

The rectangle has three branches; the last ends at the exact vanishing cutoff.

noncomputable def G67SumCoordinate.piecewiseIntegral : ℝ

Five fixed one-dimensional integrals, free of moving-domain min/max operations.

Equations

• G67SumCoordinate.piecewiseIntegral = 1 / 2 * ((∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 53 + 4 / 33, G67SumCoordinate.profile s * (Real.log ((s - 4 / 53) * (s - 4 / 53) / (4 / 53 * (4 / 53))) / s)) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 4 / 33, G67SumCoordinate.profile s * (Real.log (4 / 33 * (4 / 33) / ((s - 4 / 33) * (s - 4 / 33))) / s)) + ((∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 4 / 33, G67SumCoordinate.profile s * (Real.log ((s - 4 / 33) * (s - 4 / 53) / (4 / 53 * (4 / 33))) / s)) + ((∫ (s : ℝ) in 4 / 33 + 4 / 33..4 / 53 + 3 / 11, G67SumCoordinate.profile s * (Real.log (4 / 33 * (s - 4 / 53) / (4 / 53 * (s - 4 / 33))) / s)) + ∫ (s : ℝ) in 4 / 53 + 3 / 11..1 / 2 - 2 * (4 / 53), G67SumCoordinate.profile s * (Real.log (4 / 33 * (3 / 11) / ((s - 3 / 11) * (s - 4 / 33))) / s)))

theorem G67SumCoordinate.elementaryIntegral_eq_piecewise : G67ElementaryIntegral.elementaryIntegral = piecewiseIntegral

Exact equality of the original elementary integral with all five explicit branches.

theorem G67SumCoordinate.actual_constant_lower_piecewise : 4 * piecewiseIntegral ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

Final actual-C67 consumer: any future certified estimate can target the five fixed branches.