exp_67144_lt_824
plain-language theorem explainer
The inequality exp(6.7144) < 824.2 holds over the reals. It supplies a numerical endpoint for the electron-mass necessity argument in Recognition Science. The proof splits the argument at 6 + 0.7144, multiplies the separate upper bounds on each exponential factor, and chains the resulting product inequality via transitivity.
Claim. $e^{6.7144} < 824.2$
background
Module T9 Necessity shows the electron mass formula is forced from T8 ledger quantization together with the geometric constants already derived. The hypothesis definition simply asserts that the exponential of 6.7144 is strictly less than 824.2. The argument draws on the companion upper-bound lemma exp(6) < 403.428794, the fractional bound exp(0.7144) < 2.042961, and the transitivity lemma for the order on LogicNat that has been lifted to the reals.
proof idea
The tactic proof unfolds the hypothesis, rewrites the exponential via the addition formula as a product, invokes the two pre-proved upper bounds, applies nlinarith to obtain the product bound, normalizes the numerical comparison to 824.2, and closes with the transitivity lemma.
why it matters
The result supplies the lower endpoint needed by the downstream theorem log_824_lower, which in turn feeds the electron-mass necessity claim. It therefore participates in the T9 forcing step that derives the mass formula from T8 and the phi-ladder constants. The module as a whole closes the necessity direction for the electron mass once the geometric constants are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.