phi_pow_residue_mu_upper
plain-language theorem explainer
The declaration establishes that the golden ratio raised to the predicted muon residue lies strictly below 0.0098. Researchers deriving lepton masses in the Recognition framework cite this to cap the muon prediction from the phi-ladder. The proof obtains the residue interval, applies strict monotonicity of exponentiation by phi greater than 1, and chains to the separate numeric bound on phi to the power -9.62.
Claim. Let $r_μ$ denote the predicted muon residue $(g_{1332} - s) + Δ_{eμ}$, where $g_{1332}$ is the gap at 1332, $s$ the refined shift, and $Δ_{eμ}$ the electron-to-muon step. Let $φ$ be the golden ratio. Then $φ^{r_μ} < 0.0098$.
background
The module proves T10 necessity for the lepton ladder, replacing axioms for muon and tau masses with inequalities forced from the electron structural mass (T9) together with cube geometry steps and the golden ratio $φ$ (T4). The predicted muon residue is defined as the sum of the gap at rung 1332 minus a refined shift plus the electron-muon step function. Upstream, the lemma establishing that $φ^x$ is strictly increasing for $φ > 1$ supplies the monotonicity tool, while the numeric result $φ^{-9.62} < 0.0098$ supplies the final comparison value.
proof idea
The term proof first calls the residue bounds lemma to obtain the interval containing the exponent, equates $φ$ to the golden ratio, invokes the strict monotonicity lemma to transfer the upper endpoint -9.62 to the power, and concludes by applying the numeric theorem on $φ^{-9.62}$ inside a calc chain.
why it matters
This supplies the upper half of the residue-power bounds lemma, which feeds the predicted muon mass upper bound below 107. It closes one link in the T10 chain that forces the lepton ladder from the eight-tick octave, cube-derived steps, and the phi-ladder mass formula without extra axioms. The result relies on $φ$ as the self-similar fixed point (T4) and the residue model for rung placement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.