exp_063407156_upper_q
plain-language theorem explainer
This lemma supplies a rational upper bound confirming that the 10-term Taylor sum for exp(0.63407156) plus its scaled remainder stays below 1.88528. It is cited inside the proof of the real exponential inequality used for lepton mass step functions. The proof is a one-line wrapper invoking native_decide on the precomputed rationals.
Claim. Let $x = 63407156/100000000$. Then $1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880 + x^{10}·11/(10!·10) < 188528/100000$.
background
The module proves the muon and tau masses are forced from the electron mass (T9) and geometric constants derived from cube geometry, the golden ratio, and the eight-tick octave. The two upstream definitions compute the Taylor polynomial of degree 9 and the Lagrange remainder bound scaled by 11/10 at the fixed point x = 0.63407156, which appears in the exponential factor of the lepton rung formula.
proof idea
One-line wrapper that applies native_decide to the rational inequality formed by the precomputed Taylor sum and error term.
why it matters
It discharges the rational check inside exp_063407156_upper, which supplies the exponential bound required by the lepton mass prediction inequalities. This step closes part of the T10 forcing chain that replaces the original lepton axioms with theorems derived from T9, cube geometry (E_passive = 11, faces = 6, W = 17), and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.