exp_07145_lower
plain-language theorem explainer
The lemma establishes that 2.0431648 is strictly less than exp(0.7145). Researchers deriving the electron mass formula under T9 necessity cite this bound to anchor comparisons against mass topology values. The proof invokes Mathlib's exp_bound for |x| ≤ 1 at n=10, equates the Taylor sum and remainder to sibling rational definitions, casts a native_decide inequality, and chains the result with linarith.
Claim. $2.0431648 < e^{0.7145}$ holds.
background
The declaration lives in the T9 Necessity module, whose module doc states that the electron mass formula is forced from T8 ledger quantization and geometric constants. It depends on the sibling definitions exp_taylor_10_at_7145 (the explicit 10-term Taylor polynomial at x = 7145/10000) and exp_error_10_at_7145 (the corresponding remainder bound x^{10} * 11 / (10! * 10)). The upstream lemma exp_07145_lower_q supplies the rational comparison 20431648/10000000 + error < taylor_sum via native_decide. The module imports interval arithmetic and gap properties to support mass calculations.
proof idea
The tactic proof first confirms |0.7145| ≤ 1 by norm_num and applies Real.exp_bound with n=10. It equates the 10-term sum and error term to the precomputed rationals exp_taylor_10_at_7145 and exp_error_10_at_7145 via simp and norm_num. A cast from exp_07145_lower_q gives the strict inequality between the target rational and the difference taylor minus error. A final calc block combines norm_num, linarith on the absolute-error inequality, and the bound to reach the conclusion.
why it matters
This numerical anchor feeds the parent theorem val_824_lt_exp_67145, which decomposes exp(6.7145) to compare against a mass-related threshold. It supplies a concrete step in the T9 necessity argument that the electron mass is forced by Recognition Science constants, including the phi-ladder and alpha band derived from T5–T8. The result closes a numerical gap between ledger quantization and the specific mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.