phi_rpow_strictMono
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not address monotonicity for bases in (0,1).
- Does not supply growth rates or derivatives.
- Does not extend to complex exponents.
- Does not reference J-cost, defect distance, or the eight-tick octave.
formal statement (Lean)
230lemma phi_rpow_strictMono : StrictMono (fun x : ℝ => goldenRatio ^ x) := by
proof body
Term-mode proof.
231 intro y z hyz
232 exact Real.rpow_lt_rpow_of_exponent_lt Real.one_lt_goldenRatio hyz
233
234/-- φ^x is monotone increasing in x -/
used by (15)
-
phi_rpow_lt_of_lt -
phi_rpow_mono -
phi_rpow_neg_lt_of_lt -
phi_pow_residue_mu_lower -
phi_pow_residue_mu_lower_v2 -
phi_pow_residue_mu_upper -
phi_pow_residue_mu_upper_v2 -
phi_pow_residue_tau_lower -
phi_pow_residue_tau_lower_v2 -
phi_pow_residue_tau_upper -
phi_pow_residue_tau_upper_v2 -
phi_pow_residue_mu_lower -
phi_pow_residue_mu_upper -
phi_pow_residue_tau_lower -
phi_pow_residue_tau_upper