exp_error_10_at_063407156
plain-language theorem explainer
The definition supplies the rational remainder term for the degree-10 Taylor expansion of exp at the fixed point 0.63407156, obtained by scaling the standard Lagrange form by the factor 11/(10!·10). It is invoked by the two bounding lemmas that close the exponential upper estimate required for muon and tau mass predictions. The body is a direct arithmetic substitution of the rational argument into that scaled remainder expression.
Claim. Let $x = 63407156/100000000$. The error term is defined by $e_{10}(x) := x^{10}·11/(10!·10)$.
background
Module T10 Necessity shows that the muon and tau masses are forced once the electron mass (T9), the cube-derived constants E_passive=11, faces=6, W=17, the golden ratio φ, and α are given. The numeric argument 0.63407156 appears inside the step-function or residue calculation that converts those constants into mass ratios on the φ-ladder. The definition therefore supplies one concrete rational ingredient for the exponential bounds that replace the two original axioms in LeptonGenerations.lean.
proof idea
One-line definition that substitutes the rational 63407156/100000000 into the scaled Lagrange remainder formula x^10·11/(10!·10). No lemmas are applied; the expression is evaluated directly in ℚ.
why it matters
The definition is used by exp_063407156_upper and exp_063407156_upper_q, which together establish the strict inequality Real.exp(0.63407156) < 1.88528 needed for the muon-mass and tau-mass bound lemmas. It therefore participates in discharging the two axioms that previously stood between T9 (electron mass) and the full lepton-ladder forcing statement. The surrounding module cites the eight-tick octave and cube geometry as the source of the constants that produce the 0.63407156 argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.