phi_rpow_strictMono
plain-language theorem explainer
Golden ratio to a real power is strictly increasing. Interval bounds and lepton mass residue calculations cite this for preserving order under exponentiation. The proof is a one-line wrapper invoking the standard real analysis inequality for bases exceeding one.
Claim. The map $xmapsto phi^x$ is strictly increasing on the reals, where $phi$ denotes the golden ratio.
background
The module supplies interval arithmetic for the power function via the identity $x^y = exp(y log x)$ for positive $x$. The golden ratio exceeds one, enabling monotonicity results that propagate bounds without explicit derivative estimates. Upstream imports include Mathlib facts on real exponentiation and the golden ratio definition.
proof idea
One-line wrapper that applies the Mathlib lemma establishing strict increase of real powers for bases greater than one, using the fact that the golden ratio exceeds one.
why it matters
This monotonicity result feeds the strict and weak inequality lemmas for phi-powers in the same module and is invoked in lepton generations necessity theorems to bound residues such as the muon mass prediction. It supports order preservation on the phi-ladder consistent with the self-similar fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.