exp_error_10_at_481212
plain-language theorem explainer
This definition supplies the explicit rational error bound for the tenth-order Taylor polynomial of the exponential at x = 0.481212. Researchers verifying the forced electron mass in Recognition Science cite it to control truncation error when comparing exp(x) against the golden ratio. It is obtained by direct substitution of the scaled Lagrange remainder into a single rational expression.
Claim. Let $x = 481212/1000000$. The error bound is $e = x^{10} · 11 / (10! · 10)$.
background
The module proves that the electron mass formula is forced from T8 ledger quantization together with the geometric constants phi and alpha derived earlier. This definition provides a concrete rational upper bound on the remainder of the Taylor series for exp(x) at the specific point x = 0.481212, which is used to compare against phi ≈ 1.618034. Upstream results on empirical programs and simplicial ledgers supply the structural constraints that embed such numerical checks inside the necessity argument.
proof idea
The definition is a direct algebraic expression: it sets x to the rational 481212/1000000 and multiplies the tenth power by the factor 11 over (10! times 10). No lemmas are invoked; the body is a single let-binding followed by the arithmetic term.
why it matters
It supports the numerical lemma exp_taylor_481212_gt_target which in turn discharges the comparison in log_upper_numerical, confirming log(phi) < 0.481212. This inequality is required for the T9 necessity proof that the electron mass formula follows from the eight-tick octave and the phi-ladder without additional assumptions. The definition closes a numerical gap in the chain from T8 to the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.