pow_strict_mono
plain-language theorem explainer
The lemma establishes that for real x less than y and base a greater than 1, a to the power x is strictly less than a to the power y. Numerics workers verifying phi-ladder bounds or interval claims in Recognition Science would cite it to certify monotonicity without external libraries. The proof reduces the claim to strict monotonicity of the exponential after scaling the inequality by the positive logarithm of the base.
Claim. Let $x, y, a$ be real numbers with $a > 1$ and $x < y$. Then $a^x < a^y$.
background
The IntervalProofs module supplies minimal helpers that convert small numerical inequalities into Lean proofs, relying on norm_num together with monotonicity of exp and log. This lemma appears among siblings including exp_strict_mono and the phi-bound lemmas. It draws on lt_trans from ArithmeticFromLogic to obtain positivity of the base and on standard facts for the logarithm and exponential.
proof idea
The tactic proof first obtains positivity of a via lt_trans and norm_num. It then derives log a > 0 from Real.log_pos and linarith. Multiplication by this positive quantity preserves the strict inequality via nlinarith. Application of exp_strict_mono produces the exponential inequality, which is rewritten to the power form by simpa using the definition of real power for positive bases.
why it matters
The lemma supports the numerics layer that certifies bounds on phi-powers and golden-ratio identities required by the forcing chain (T5 J-uniqueness through T8 D=3). It underpins interval arguments for constants such as alpha inverse inside (137.030, 137.039) and mass formulas on the phi-ladder. Though currently unused downstream, it closes a gap in turning analytic inequalities into machine-checked statements for Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.