exp_080454125_lower_q
plain-language theorem explainer
The lemma verifies the rational inequality 2.23567 plus the explicit 10th-order remainder bound is strictly less than the 9-term Taylor polynomial for exp at x = 0.80454125. Physicists deriving the muon and tau masses in the Recognition Science lepton ladder would cite this check when converting axiomatic bounds into proven inequalities. The proof is a one-line wrapper that invokes native_decide on the decidable rational comparison.
Claim. Let $x = 80454125/100000000$. Let $T_9(x) = 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$ and let $R(x) = x^{10} · 11 / (10! · 10)$. Then $2.23567 + R(x) < T_9(x)$.
background
The module proves T10 necessity for the lepton ladder, replacing two axioms in LeptonGenerations.lean with derived bounds on predicted muon and tau masses. These bounds combine the electron structural mass from T9, the step functions from cube geometry (E_passive = 11, faces = 6, W = 17), the fine-structure constant α, and π. The exponential enters the mass formula through the phi-ladder rung calculations that arise from the eight-tick octave structure.
proof idea
The proof is a one-line wrapper that applies native_decide to the decidable proposition comparing the two explicit rational expressions obtained from the upstream definitions of exp_taylor_10_at_080454125 and exp_error_10_at_080454125.
why it matters
This lemma supplies the rational arithmetic step required by the downstream lemma exp_080454125_lower, which in turn supports the muon_mass_pred_bounds and tau_mass_pred_bounds that discharge the axioms in the lepton generations necessity proof. It closes a numerical gap in the T10 forcing chain that links the electron mass (T9) to the higher lepton rungs via the geometric constants and the phi-ladder. No open scaffolding remains for this check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.