exp_048_lt_phi
plain-language theorem explainer
The lemma certifies that the tenth-order Taylor sum for exp at 0.48 plus its explicit remainder bound lies strictly below the rational 1.61803395. Interval-arithmetic workers cite it to obtain a machine-checked lower bound on log(φ) via monotonicity of the exponential. The argument reduces to a single native_decide call that evaluates the two rational expressions at compile time.
Claim. Let $T_{10}(0.48) = 1 + 0.48 + 0.48^2/2 + 0.48^3/6 + 0.48^4/24 + 0.48^5/120 + 0.48^6/720 + 0.48^7/5040 + 0.48^8/40320 + 0.48^9/362880$ and let $E_{10}(0.48) = 0.48^{10} · 11 / (10! · 10)$. Then $T_{10}(0.48) + E_{10}(0.48) < 1.61803395$.
background
The module supplies rigorous interval bounds for log on (0, ∞) by reducing to the Taylor series of log(1 + x) for |x| < 1, with remainder controlled by |x|^{n+1} / ((n+1)(1 - |x|)). For log(φ) one sets x = φ - 1 ≈ 0.618 and obtains an interval containing the value. The complementary direction requires an upper bound on exp(0.48) so that the inequality φ > exp(0.48) can be checked directly. The two rational constants exp_taylor_10_at_048 and exp_error_10_at_048 are defined in the same file (and duplicated in AlphaBounds) precisely for this comparison.
proof idea
The proof is a one-line term that applies native_decide to the concrete rational inequality between the precomputed Taylor sum plus error term on the left and the fixed denominator 100000000 on the right.
why it matters
The result is the numerical engine behind the downstream theorem log_phi_gt_048, which asserts log(φ) > 0.48. Within Recognition Science, φ is the self-similar fixed point forced at step T6 of the unified forcing chain and appears in the mass formula via the phi-ladder; a certified lower bound on its logarithm tightens the numerical window for the fine-structure constant inside (137.030, 137.039) and for the eight-tick octave. The lemma therefore closes the last computational gap between the analytic Taylor machinery and the concrete value of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.