exp_0483_gt
plain-language theorem explainer
This lemma proves the numerical inequality 1.6209 < exp(0.483). Researchers tightening interval estimates for the inverse fine-structure constant or logarithmic bounds on the golden ratio cite it when chaining exponential inequalities. The proof applies the general Taylor remainder bound for exp at order 10, equates the partial sum and error to precomputed rationals, subtracts the error term, and compares the result against the target constant via a floor lemma.
Claim. $16209/10000 < e^{0.483}$
background
The module supplies rigorous interval bounds on the inverse fine-structure constant using symbolic derivations and precomputed Taylor data. Local definitions compute the 10-term Taylor polynomial for exp at argument 0.483 together with its Lagrange-style remainder bound, both expressed as explicit rationals. Upstream results supply the associativity and commutativity of addition plus the successor operation from the foundational arithmetic layer; these are invoked only to rearrange the remainder inequality.
proof idea
The tactic sequence first checks |0.483| ≤ 1 and calls the general exp_bound lemma with n = 10. It then rewrites the Taylor sum and error expressions to match the pre-defined rational constants via simp and norm_num. From the absolute-value form of the remainder it isolates a lower bound for exp(0.483). The final step applies the companion floor lemma to show that 1.6209 lies strictly below this lower bound and concludes by transitivity.
why it matters
The result is invoked by the companion lemma that places log phi strictly below 0.483, thereby tightening the numerical interval for alpha inverse inside the Recognition Science phi-ladder. It supplies one concrete link in the chain of exponential bounds that support the claimed alpha band (137.030, 137.039) without introducing new hypotheses. No scaffolding or open questions remain at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.