noncomputable def G67SumCoordinate.profile (s : ℝ) : ℝ

The actual elementary kernel as a function of the sum coordinate.

Equations

• G67SumCoordinate.profile s = max 0 (Real.log ((1 / 2 - s - 4 / 53) / (4 / 53)) / (1 / 2 - s))

theorem G67SumCoordinate.profile_domain {s : ℝ} (hs : s ≤ 4 / 33 + 3 / 11) : 0 < 1 / 2 - s ∧ 0 < (1 / 2 - s - 4 / 53) / (4 / 53)

Strict denominator and logarithm-domain bounds on both actual sum ranges.

theorem G67SumCoordinate.profile_continuousOn : ContinuousOn profile (Set.Icc (4 / 53 + 4 / 53) (4 / 33 + 3 / 11))

Continuity of the actual profile on the whole compact sum range.

theorem G67SumCoordinate.profile_add (u v : ℝ) : profile (u + v) = G67ElementaryIntegral.elementaryKernel (u, v)

Literal equality to the imported original elementary kernel, not a replacement definition.

theorem G67SumCoordinate.profile_zero {s : ℝ} (hs : 1 / 2 - 2 * (4 / 53) ≤ s) (hupper : s ≤ 4 / 33 + 3 / 11) : profile s = 0

The elementary logarithm vanishes above the exact cutoff, within the actual domain.

noncomputable def G67SumCoordinate.oneDimensionalIntegral : ℝ

A genuine one-dimensional expression for the original half-square plus rectangle.

Equations

• G67SumCoordinate.oneDimensionalIntegral = (1 / 2 * ∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 33 + 4 / 33, G67SumCoordinate.profile s * G67SumCoordinate.weight (4 / 53) (4 / 33) (4 / 53) (4 / 33) s) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 3 / 11, G67SumCoordinate.profile s * G67SumCoordinate.weight (4 / 53) (4 / 33) (4 / 33) (3 / 11) s

theorem G67SumCoordinate.elementaryIntegral_eq_oneDimensional : G67ElementaryIntegral.elementaryIntegral = oneDimensionalIntegral

Exact specialization: both original rectangles and the half-square factor are preserved.

theorem G67SumCoordinate.actual_constant_lower_oneDimensional : 4 * oneDimensionalIntegral ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

The actual C67 bound consumes the exact one-dimensional expression without analytic premises.

theorem G67SumCoordinate.actual_constant_lower_explicit : 4 * ((1 / 2 * ∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 33 + 4 / 33, max 0 (Real.log ((1 / 2 - s - 4 / 53) / (4 / 53)) / (1 / 2 - s)) * (Real.log (min (4 / 33) (s - 4 / 53) * (s - max (4 / 53) (s - 4 / 33)) / (max (4 / 53) (s - 4 / 33) * (s - min (4 / 33) (s - 4 / 53)))) / s)) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..4 / 33 + 3 / 11, max 0 (Real.log ((1 / 2 - s - 4 / 53) / (4 / 53)) / (1 / 2 - s)) * (Real.log (min (4 / 33) (s - 4 / 33) * (s - max (4 / 53) (s - 3 / 11)) / (max (4 / 53) (s - 3 / 11) * (s - min (4 / 33) (s - 4 / 33)))) / s)) ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant

Fully expanded public endpoint for later certified one-dimensional constant estimates.