exp_v2_2_q
plain-language theorem explainer
This lemma verifies the rational inequality 1.8806 plus the tenth-order remainder bound is strictly less than the ninth-order Taylor polynomial for the exponential at argument 0.6316. Physicists deriving lepton mass predictions in Recognition Science cite it to close a numerical gap in the T10 necessity argument. The verification proceeds by a single native_decide tactic that evaluates the inequality exactly over the rationals.
Claim. Let $x = 0.6316$. Then $1.8806 + x^{10} · 11 / (10! · 10) < 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$.
background
In the T10 module on lepton ladder necessity, this inequality supports replacement of axiomatic muon and tau mass bounds with proven statements derived from the electron mass (T9) and geometric constants. The exponential enters through step functions built from passive cube edges (11), faces (6), wallpaper groups (17), and the fine-structure constant. The supplied definitions fix x = 6316/10000, with exp_taylor_v2_2 the partial sum through order 9 and exp_error_v2_2 the scaled Lagrange remainder bound x^10 · 11 / (10! · 10).
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the rational inequality. It evaluates the difference between the left-hand side (1.8806 plus the error term) and the right-hand side (the explicit partial sum) exactly over ℚ and confirms positivity. No additional lemmas beyond the two upstream definitions are required.
why it matters
The lemma is invoked by exp_06316_lower to obtain the strict real inequality 1.8806 < exp(0.6316), which tightens the predicted bounds on the muon and tau masses. It fills a concrete numerical step inside the T10 necessity proof that the lepton ladder is forced by the eight-tick octave, cube geometry, and the phi-ladder. The result removes one remaining axiom in the lepton-generation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.