exp_error_v2_1
plain-language theorem explainer
This definition supplies the explicit rational error term for the 10-term Taylor expansion of exp at argument 0.6327. It is cited inside the lemmas that close the upper bound on that exponential for use in lepton mass predictions. The body is a direct arithmetic expression that evaluates the scaled Lagrange remainder.
Claim. Define the rational error term $e := (6327/10000)^{10} · 11 / (10! · 10)$. This quantity upper-bounds the remainder after ten terms in the Taylor series for exp(0.6327).
background
The module establishes that the lepton ladder is forced from the electron structural mass (T9) together with step functions drawn from cube geometry, the fine-structure constant, and the golden ratio. The local setting replaces the two axioms of the earlier LeptonGenerations file with derived inequalities on predicted muon and tau masses. The present definition supplies a concrete rational that appears in the exponential bound used to certify those inequalities.
proof idea
One-line definition that directly computes the expression: set x = 6327/10000 and return x^10 * 11 / (10! * 10). No lemmas are invoked; the value is obtained by ordinary rational arithmetic.
why it matters
The definition feeds the two downstream lemmas that together prove exp(0.6327) < 1.8827. Those lemmas in turn support the replacement of axiomatic mass bounds by proven inequalities in the T10 necessity argument. Within the Recognition framework it contributes to showing that muon and tau masses follow from the eight-tick octave and D = 3 geometry once the electron mass and geometric constants are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.