exp_0481_lt_phi
plain-language theorem explainer
The lemma certifies that the degree-10 Taylor sum for exp(0.481) plus its explicit remainder bound lies strictly below the rational 1.61803395. Recognition Science numerics work cites it to obtain the rigorous inequality log(φ) > 0.481 via monotonicity of the exponential. The proof is a single native_decide that evaluates the concrete rational comparison.
Claim. Let $t_{10}(0.481) = 1 + 0.481 + 0.481^2/2 + 0.481^3/6 + 0.481^4/24 + 0.481^5/120 + 0.481^6/720 + 0.481^7/5040 + 0.481^8/40320 + 0.481^9/362880$ and let $e_{10}(0.481) = 0.481^{10} · 11 / (10! · 10)$. Then $t_{10}(0.481) + e_{10}(0.481) < 1.61803395$.
background
The Numerics.Interval.Log module supplies rigorous interval bounds for the natural logarithm by converting log(φ) > 0.481 into the equivalent statement φ > exp(0.481) and controlling the exponential from above. The Taylor polynomial exp_taylor_10_at_0481 and remainder exp_error_10_at_0481 are defined locally as explicit rational expressions at the point 481/1000. These definitions mirror the corresponding constructions in AlphaBounds and rely on the standard Lagrange-form remainder estimate for the exponential series.
proof idea
The proof is a one-line native_decide that performs exact rational arithmetic on the precomputed Taylor sum and error term, then compares the result against the target rational 161803395/100000000.
why it matters
The bound is invoked by the downstream theorem log_phi_gt_0481 that records log(φ) > 0.481. Within Recognition Science this supplies a machine-verified numerical anchor for the golden-ratio fixed point (T6) that appears in the phi-ladder mass formula and the eight-tick octave structure. It closes a concrete gap in the interval-arithmetic pipeline without introducing floating-point hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.