phi_pow_residue_mu_lower_v2
plain-language theorem explainer
The inequality shows that the golden ratio raised to the predicted muon residue exceeds 0.00972. Researchers deriving lepton masses from the Recognition Science phi-ladder would cite this to anchor the lower bound on the muon mass. The short tactic proof obtains the residue interval from predicted_residue_mu_bounds_v2, rewrites phi as goldenRatio, then chains the known bound on phi to the power -9.627 through strict monotonicity and lt_trans.
Claim. Let $r_μ$ denote the predicted muon residue, defined as (gap at 1332 minus refined shift) plus the electron-to-muon step. Then $0.00972 < φ^{r_μ}$.
background
In the Recognition Science setting the lepton ladder is built from the electron structural mass (T9) together with fixed geometric inputs: passive cube edges equal to 11, cube faces equal to 6, wallpaper groups equal to 17, and the fine-structure constant α. The predicted muon residue is the sum of the gap term at rung 1332 and the step function that encodes those geometric constants. The golden ratio φ is the self-similar fixed point forced in T6 and appears here as the base of the exponential that converts residue to mass on the phi-ladder.
proof idea
The tactic first calls predicted_residue_mu_bounds_v2 to obtain the open interval (-9.6268, -9.6254) for the residue. It rewrites φ as Real.goldenRatio, then uses linarith to strengthen the lower endpoint to -9.627. The final step applies lt_trans to the already-proven lower bound phi_pow_neg9627_lower_v2 together with the strict monotonicity lemma phi_rpow_strictMono.
why it matters
This bound is invoked directly by the downstream theorem predicted_mass_mu_lower_v2, which establishes that the predicted muon mass exceeds 105.5 MeV and thereby contributes one clause to the T10 statement that the full lepton ladder is forced from T9 with no free parameters. It closes a concrete link between the eight-tick octave, the phi-ladder mass formula, and the observed muon mass within the documented accuracy interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.