log_one_add_bounds
plain-language theorem explainer
The lemma supplies explicit error bounds for the partial sum of the alternating series approximating log(1 + y) when 0 < y < 1. Numerics routines in the Recognition Science framework cite it to enclose log(φ) and related constants inside rigorous intervals. The argument reduces the claim to Mathlib's abs_log_sub_add_sum_range_le by the substitution x = -y, sign adjustment on the sum, and two applications of the triangle inequality.
Claim. For $0 < y < 1$ and $n ∈ ℕ$, let $S_n = ∑_{i=0}^{n-1} (-1)^i y^{i+1}/(i+1)$ and $err = y^{n+1}/(1-y)$. Then $S_n - err ≤ log(1+y) ≤ S_n + err$.
background
The module Numerics.Interval.Log supplies rigorous interval enclosures for the natural logarithm on positive reals. It relies on monotonicity of log together with Taylor series with remainder for log(1 + x) when |x| < 1. The local strategy reduces log(φ) to the case x = φ - 1 ≈ 0.618 which lies in (0,1), then applies the alternating series bound.
proof idea
The proof applies Real.abs_log_sub_add_sum_range_le to the argument -y after verifying |-y| < 1. It shows the Mathlib sum equals -S by negating the series term-by-term and using (-1)^{i+1} = -(-1)^i. The identity log(1 - (-y)) = log(1 + y) follows by ring. After rewriting to |log(1+y) - S| ≤ err, the two-sided bound follows from -|z| ≤ z ≤ |z| applied to z = log(1+y) - S together with linarith.
why it matters
This lemma supports numerical verification of constants such as log(φ) in the Recognition Science framework, where φ is the self-similar fixed point forced at T6. It feeds interval computations for the phi-ladder and mass formulas that rely on the eight-tick octave and D = 3. Although no direct downstream theorems appear, it closes the gap between the abstract forcing chain (T5 J-uniqueness) and concrete bounds needed for α^{-1} inside (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.