val_824_lt_exp_67145
plain-language theorem explainer
The inequality 824.2218 < exp(6.7145) holds over the reals. Electron-mass derivations in Recognition Science cite it to close the upper bound on log(1 + 1332/phi). The proof splits the exponential argument, invokes separate lower-bound lemmas on exp(6) and exp(0.7145), forms their product via nlinarith, and chains the comparison with lt_trans.
Claim. $824.2218 < e^{6.7145}$
background
The declaration lives in the ElectronMass.Necessity module, whose module doc states that the electron mass formula is forced from T8 ledger quantization together with geometric constants. The target proposition is the hypothesis definition (824.2218 : ℝ) < Real.exp(6.7145 : ℝ). Upstream lemmas supply the concrete lower bounds: exp_six_lower gives 403.428793 < exp(6) and exp_07145_lower gives 2.0431648 < exp(0.7145). The arithmetic lemma lt_trans from Foundation.ArithmeticFromLogic supplies the final transitivity step.
proof idea
The tactic proof first unfolds the hypothesis definition. It rewrites the argument as 6 + 0.7145 via norm_num and Real.exp_add. It retrieves the two lower-bound lemmas exp_six_lower and exp_07145_lower. A product inequality is obtained by nlinarith using those bounds together with positivity of the exponentials. A numerical comparison shows 824.2218 lies below the product, after which lt_trans closes the chain.
why it matters
The result supplies the missing numerical endpoint for the downstream theorem log_824_upper, which bounds log(1 + 1332/phi) from above and thereby supports the T9 necessity argument that the electron mass is forced by the phi-ladder and Recognition Composition Law. It belongs to the chain of interval closures that convert the abstract forcing steps T5–T8 into concrete mass values inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.