exp_six_upper
plain-language theorem explainer
The lemma supplies the strict upper bound exp(6) < 403.428794 as a numerical anchor for splitting arguments near 6.7144 in electron mass necessity arguments. Researchers closing the T9 forcing proof for the electron mass on the phi-ladder cite it when verifying the composite inequality exp(6.7144) < 824.2. The tactic proof rewrites exp(6) as (exp 1)^6, lifts the known decimal bound on exp(1) to the sixth power, and confirms the target inequality by direct numerical comparison.
Claim. $exp(6) < 403.428794$
background
The lemma sits inside the module proving T9 necessity: the electron mass formula is forced from T8 ledger quantization and the geometric constants obtained earlier. It supplies one half of the pair of endpoint bounds required to confirm the numerical hypotheses exp(6.7144) < 824.2 and 824.2218 < exp(6.7145). The local setting therefore consists of the exponential function on the reals together with its algebraic identities exp(a + b) = exp(a) exp(b) and exp(n x) = (exp x)^n for natural n.
proof idea
The tactic proof proceeds in three steps. It first obtains (exp 1)^6 ≤ (2.7182818286)^6 by pow_le_pow_left₀ applied to the known inequality exp(1) < 2.7182818286. It then verifies the powered decimal is strictly less than 403.428794 by norm_num. The equality exp(6) = (exp 1)^6 is established by rewriting the coefficient 6 as 6 · 1 and invoking exp_nat_mul, after which lt_of_le_of_lt assembles the two inequalities.
why it matters
The bound is invoked directly by the downstream theorem exp_67144_lt_824 to finish the upper estimate after the argument split. It thereby supports the necessity claim that the electron mass matches the phi-ladder prediction under T8 without external numerical hypotheses. In the Recognition framework the lemma closes a concrete verification step inside the T9 module, ensuring the mass formula yardstick · phi^(rung - 8 + gap(Z)) is forced once the exponential endpoints are secured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.