error_term_eq_rational
plain-language theorem explainer
The lemma equates the explicit real-number remainder expression for the 10-term Taylor expansion of exp at 0.481211 to the exact rational value stored in the helper definition. Researchers closing the numerical bound in the T9 electron-mass necessity argument would cite it to justify replacing the floating-point error with a rational that norm_num can handle. The proof is a direct term-mode simplification that unfolds the helper and normalizes the arithmetic.
Claim. Let $x = 0.481211$. The Lagrange remainder bound satisfies $x^{10} · 11 / (10! · 10) = x^{10} · 11 / (3628800 · 10)$, where the left-hand side is the definition of the error-term helper.
background
The declaration sits inside the module that proves T9: the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier. The helper exp_error_10_at_481211 is defined as the rational $x^{10} · 11 / (10! · 10)$ with $x = 481211/1000000$; it supplies the explicit Lagrange-form remainder after ten terms of the exponential series. Upstream dependencies include the definition of this helper itself and several foundational structures (collision-free option-A programs, simplicial-ledger edge lengths, and mechanism-design signatures), though only the error definition is used in the immediate simplification.
proof idea
The proof is a term-mode one-liner. It applies simp only to unfold exp_error_10_at_481211 and Nat.factorial, then invokes norm_num to verify that the resulting rational expression matches the left-hand side exactly.
why it matters
The equality is invoked by the downstream lemma taylor_sum_lt_target, which rewrites the full Taylor sum plus remainder to obtain the strict inequality less than 1.618033 (the numerical stand-in for the self-similar fixed point phi). It therefore supplies one concrete numerical step inside the T9 necessity argument that the electron mass is forced by the eight-tick octave and the phi-ladder. No scaffolding remains; the claim is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.