expLowerSimple
plain-language theorem explainer
expLowerSimple supplies the rational expression x + 1 as a lower bound for the exponential. Interval enclosure code for exp on subintervals of [0,1) cites it to set the lower endpoint of the result interval. The definition is a one-line assignment that directly encodes the standard inequality exp(x) ≥ x + 1.
Claim. For rational $x$, define $L(x) := x + 1$. Then $L(x)$ satisfies the lower bound $e^x ≥ x + 1$.
background
The module supplies interval arithmetic for the exponential on intervals inside [0,1). It combines monotonicity of exp with the elementary inequalities x + 1 ≤ exp(x) for lower bounds and exp(x) ≤ 1/(1-x) for upper bounds. The present definition supplies the concrete expression used for the lower endpoint.
proof idea
The definition is a one-line wrapper that returns x + 1, relying on the known inequality add_one_le_exp from Mathlib to certify the bound in downstream uses.
why it matters
It supplies the lower endpoint inside expIntervalSimple, which is then shown to contain the true value of exp(x) by expIntervalSimple_contains_exp. The construction supports rigorous numeric verification inside the Recognition Science numerics layer that backs the forcing chain and self-reference axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.