exp_07144_upper
plain-language theorem explainer
The lemma establishes that the real exponential of 0.7144 is strictly less than 2.042961. Researchers verifying the forced electron mass under T9 would cite this bound when checking consistency of the exponential factor against the phi-ladder constants. The proof applies the Taylor remainder estimate at order 10, equates the sum and error to precomputed rationals, casts the rational inequality, and chains to the decimal target.
Claim. $e^{0.7144} < 2.042961$
background
This lemma sits inside the module proving T9 necessity, which shows the electron mass formula is forced from T8 ledger quantization together with geometric constants obtained earlier in the chain. The supporting definitions are the 10-term Taylor partial sum at argument 7144/10000, written explicitly as the sum from m=0 to 9 of x^m/m!, and the matching remainder bound x^10 * 11/(10! * 10). The upstream structure for supplies the meta-realization axioms that underwrite self-reference coherence throughout the forcing sequence from T0 onward.
proof idea
The tactic proof first records that the argument is nonnegative and at most 1. It calls Real.exp_bound' with n=10 to obtain the sum-plus-remainder inequality. The partial sum is identified with the sibling definition exp_taylor_10_at_7144 and the error term with exp_error_10_at_7144 by simplification and norm_num. The rational inequality supplied by exp_07144_upper_q is cast to reals, after which a calc chain assembles the bound, the two equalities, the strict inequality, and final normalization to reach 2.042961.
why it matters
The bound supplies a concrete numerical control required by the T9 necessity argument for the electron mass. It is used directly by the downstream theorem that factors exp(6.7144) as exp(6) times exp(0.7144) to close a larger inequality. In the Recognition Science setting it anchors the numerical verification step that follows T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 three spatial dimensions, confirming the mass formula sits on the phi-ladder without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.