noncomputable def G67Analytic.weightArg (a b c d s : ℝ) : ℝ

The original sum-fiber logarithm argument, with no deleted branches.

Equations

• G67Analytic.weightArg a b c d s = G67SumCoordinate.upper b c s * (s - G67SumCoordinate.lower a d s) / (G67SumCoordinate.lower a d s * (s - G67SumCoordinate.upper b c s))

theorem G67Analytic.weightArg_ge_one {a b c d s : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) : 1 ≤ weightArg a b c d s

theorem G67Analytic.weightArg_continuousOn {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) : ContinuousOn (weightArg a b c d) (Set.Icc (a + c) (b + d))

noncomputable def G67Analytic.weightLower (n : ℕ) (a b c d s : ℝ) : ℝ

Log-free lower density of the entire original sum fiber.

Equations

• G67Analytic.weightLower n a b c d s = G67Analytic.logLower n (G67Analytic.weightArg a b c d s) / s

theorem G67Analytic.weightLower_nonneg {a b c d s : ℝ} (n : ℕ) (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) : 0 ≤ weightLower n a b c d s

theorem G67Analytic.weightLower_le {a b c d s : ℝ} (n : ℕ) (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) : weightLower n a b c d s ≤ G67SumCoordinate.weight a b c d s

theorem G67Analytic.weightLower_continuousOn {a b c d : ℝ} (n : ℕ) (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) : ContinuousOn (weightLower n a b c d) (Set.Icc (a + c) (b + d))

theorem G67Analytic.profileLower_continuousOn (n : ℕ) : ContinuousOn (profileLower n) (Set.Iic (1 / 2 - 2 * (4 / 53)))

theorem G67Analytic.densityLower_le {a b c d s : ℝ} (n : ℕ) (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) (hcut : s ≤ 1 / 2 - 2 * (4 / 53)) : profileLower n s * weightLower n a b c d s ≤ G67SumCoordinate.profile s * G67SumCoordinate.weight a b c d s

Pointwise product comparison has both multiplier signs justified.

theorem G67Analytic.integral_densityLower_le {a b c d l r : ℝ} (n : ℕ) (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hlr : l ≤ r) (hleft : a + c ≤ l) (hright : r ≤ b + d) (hcut : r ≤ 1 / 2 - 2 * (4 / 53)) (hprofile : ContinuousOn G67SumCoordinate.profile (Set.Icc l r)) : ∫ (s : ℝ) in l..r, profileLower n s * weightLower n a b c d s ≤ ∫ (s : ℝ) in l..r, G67SumCoordinate.profile s * G67SumCoordinate.weight a b c d s

Integral comparison on any certified subinterval; its hypotheses are geometry, not a carried numerical estimate.

noncomputable def G67Analytic.rationalIntegral (n : ℕ) : ℝ

The log-free approximation retains the original half-square and the full rectangle up to the exact vanishing cutoff. This is a lower bound, not equality.

Equations

• G67Analytic.rationalIntegral n = (1 / 2 * ∫ (s : ℝ) in 4 / 53 + 4 / 53..4 / 33 + 4 / 33, G67Analytic.profileLower n s * G67Analytic.weightLower n (4 / 53) (4 / 33) (4 / 53) (4 / 33) s) + ∫ (s : ℝ) in 4 / 53 + 4 / 33..1 / 2 - 2 * (4 / 53), G67Analytic.profileLower n s * G67Analytic.weightLower n (4 / 53) (4 / 33) (4 / 33) (3 / 11) s

theorem G67Analytic.rationalIntegral_le_piecewise (n : ℕ) : rationalIntegral n ≤ G67SumCoordinate.piecewiseIntegral

Unconditional lower bound for the exact five-branch production object.

theorem G67Analytic.weightLower_first {a b c d s : ℝ} (n : ℕ) (hL : s ≤ a + d) (hU : s ≤ b + c) : weightLower n a b c d s = logLower n ((s - c) * (s - a) / (a * c)) / s

The early-branch formula for the lower fiber uses the same original argument.

theorem G67Analytic.weightLower_middle {a b c d s : ℝ} (n : ℕ) (hL : s ≤ a + d) (hU : b + c ≤ s) : weightLower n a b c d s = logLower n (b * (s - a) / (a * (s - b))) / s

The middle branch is retained, not replaced by an early-branch surrogate.

theorem G67Analytic.weightLower_last {a b c d s : ℝ} (n : ℕ) (hL : a + d ≤ s) (hU : b + c ≤ s) : weightLower n a b c d s = logLower n (b * d / ((s - d) * (s - b))) / s

The late branch remains present through the exact profile cutoff.