exp_taylor_v2_4
plain-language theorem explainer
exp_taylor_v2_4 defines the rational value of the Taylor polynomial for exp(x) truncated after the x^9 term at the fixed point x = 8093/10000. It is invoked inside the same module to certify strict lower bounds on Real.exp(0.8093) that feed the muon and tau mass interval proofs. The definition is obtained by a single let-binding that substitutes the rational directly into the nine-term sum.
Claim. Let $x = 8093/10000$. Define the rational $e_{taylor} := 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
Module T10 replaces the two lepton-mass axioms of the earlier LeptonGenerations file with derived bounds that start from the electron mass (T9) and the geometric constants E_passive = 11, cube faces = 6, wallpaper count W = 17, together with the fine-structure constant and the golden ratio fixed point. The exponential appears in the mass-ratio step functions that map rung indices on the phi-ladder to the muon and tau values. This definition supplies an exact rational proxy for the partial sum of exp(0.8093) so that subsequent lemmas can compare it against explicit decimal thresholds without leaving the rational field.
proof idea
The declaration is a direct definition. It binds the rational x := 8093/10000 and then writes the nine-term Taylor sum as a single expression; no lemmas or tactics are invoked.
why it matters
The definition is the numerical anchor for the two lemmas exp_08093_lower and exp_v2_4_q that close the T10 necessity argument. Those lemmas convert the rational proxy into a verified strict inequality Real.exp(0.8093) > 2.2463, which is required to keep the predicted muon and tau masses inside the intervals forced by the eight-tick octave and the cube-face geometry. It therefore removes one of the remaining numerical axioms that the module was written to eliminate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.