val_824_lt_exp_67145_hypothesis
plain-language theorem explainer
Defines the proposition 824.2218 < exp(6.7145) to close one numerical endpoint required for bounding the exponential in the electron mass necessity derivation. Researchers confirming that particle masses follow from T8 ledger quantization and the phi-ladder cite this bound when checking T9 consistency. The declaration is a direct Prop definition; the dependent theorem discharges it by splitting the argument and applying Taylor remainder controls.
Claim. $824.2218 < e^{6.7145}$
background
The module proves the electron mass formula is forced from T8 ledger quantization together with geometric constants obtained earlier. Upstream structures supply J-cost minimization (strictly convex, global minimum at unity) and spectral emergence (forcing SU(3) x SU(2) x U(1) content, three generations, and 24 chiral flavors). The local setting places all masses on the phi-ladder with yardstick scaling phi^(rung-8+gap(Z)).
proof idea
Direct definition of the Prop. The dependent theorem unfolds the hypothesis, rewrites 6.7145 as 6 + 0.7145, invokes the exponential addition formula, bounds exp(6) via exp(1) inequalities and nat_mul, then controls the fractional part with 10-term Taylor bounds and native_decide rational checks.
why it matters
Closes one of the two exponential endpoint hypotheses needed to prove the electron mass is forced in the T9 necessity module. It feeds the parent theorem val_824_lt_exp_67145 and anchors the numerical step that links the Recognition Composition Law to the observed mass value on the phi-ladder. The declaration removes a concrete numerical gap between the functional equation and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.