exp_strict_mono
plain-language theorem explainer
The lemma asserts that the real exponential function strictly preserves order. Numerics workers in the Recognition framework cite it when formalizing interval comparisons that feed into power-spectrum inequalities. The proof is a one-line term wrapper that applies the strict monotonicity of exp supplied by Mathlib.
Claim. If $x < y$ for real numbers $x$ and $y$, then $e^x < e^y$.
background
The IntervalProofs module supplies minimal helpers that convert small numerical inequalities into formal proofs by relying on norm_num and monotonicity lemmas rather than heavy dependencies. This lemma records the elementary fact that the exponential is strictly increasing. It appears in the same file as the power-strict-mono lemma and sits downstream of the power definition imported from Cosmology.PrimordialSpectrum.
proof idea
The proof is a one-line term that directly invokes Real.strictMono_exp on the supplied hypothesis.
why it matters
The result feeds the pow_strict_mono lemma in the same module, which supports numerical verification of power spectra. In the Recognition framework it supplies a basic monotonicity step used when deriving bounds on the phi-ladder and related constants from interval data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.