exp_six_lower
plain-language theorem explainer
This lemma supplies a strict numerical lower bound for the exponential function at argument 6. Researchers deriving forced values for the electron mass on the Recognition Science phi-ladder cite it when tightening interval estimates against the alpha band. The proof chains a decimal comparison through monotonicity of the power map and the identity exp(6) = exp(1)^6, then applies order transitivity.
Claim. $403.428793 < e^6$
background
The module proves that the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier in the Recognition Science development. This private lemma supplies one concrete numerical anchor inside that necessity argument. It draws on the transitivity of the strict order supplied by ArithmeticFromLogic.lt_trans and on the exponential power identity from the standard real analysis library.
proof idea
The tactic proof first establishes that 2.7182818283^6 is strictly less than exp(1)^6 by applying the monotonicity lemma pow_lt_pow_left₀ to the known inequality exp(1) > 2.7182818283. A norm_num step verifies that 403.428793 lies below that same power. The identity exp(6) = exp(1)^6 is obtained by rewriting 6 as 6·1 and invoking the exponential multiplication rule. The two inequalities are then combined by transitivity.
why it matters
The bound is invoked by the downstream theorem val_824_lt_exp_67145, which splits exp(6.7145) to complete an interval comparison required for the electron-mass necessity statement. It therefore closes one numerical gap in the T9 forcing chain that derives the electron mass directly from the eight-tick octave and the phi-ladder. No open scaffolding remains for this particular inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.