exp_error_10_at_0481
plain-language theorem explainer
Error bound definition for the 10-term Taylor series of exp at 0.481 supplies the rational value used to certify exp(0.481) < φ. Interval arithmetic researchers in the Recognition Science numerics pipeline cite this to close the log(φ) > 0.481 inequality. The definition evaluates the explicit formula x^{10} * 11 / (10! * 10) at x = 481/1000.
Claim. The 10-term Taylor remainder bound for exp at x = 0.481 equals $ (481/1000)^{10} * 11 / (10! * 10) $.
background
The module develops interval arithmetic for the natural logarithm using monotonicity on (0, ∞) and Taylor remainders for log(1 + x) with |x| < 1. The error after n terms is bounded by |x|^{n+1} / ((n+1)(1 - |x|)). This definition isolates the specific remainder term at x = 0.481 to support upper bounds on exp(0.481) and thereby lower bounds on log(φ). It reuses the identical computational structure from the AlphaBounds sibling module and connects indirectly to recognition-weighted stellar assembly derivations.
proof idea
The definition directly constructs the rational by substituting x := 481/1000 into the expression x^{10} * 11 / (Nat.factorial 10 * 10). It is a one-line computational definition with no tactic steps or lemma applications.
why it matters
This supplies the numerical ceiling needed for the lemma exp_0481_lt_phi, which in turn proves the theorem log_phi_gt_0481 establishing log(φ) > 0.481. Within Recognition Science this numerical fact anchors the lower bound on the self-similar fixed point φ (T6) and feeds the phi-ladder mass formula. It forms part of the interval chain that constrains the fine-structure constant alpha within (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.