phi_pow_residue_mu_bounds
plain-language theorem explainer
Bounds on the golden ratio raised to the muon residue exponent are fixed between 0.0097 and 0.0098. Researchers deriving lepton masses from the Recognition Science phi-ladder cite this to anchor the muon scaling step from the electron base. The proof is a direct term that pairs a lower-bound lemma with an upper-bound lemma.
Claim. Let ϕ denote the golden ratio and let r_μ be the predicted residue exponent for the muon in the lepton ladder. Then 0.0097 < ϕ^{r_μ} < 0.0098.
background
The lepton generations module (T10) proves that muon and tau masses are forced once the electron structural mass (T9) and the geometric constants from cube geometry are fixed. The predicted residue for the muon is the exponent that scales the base mass along the phi-ladder; it is obtained from the combination of E_passive = 11, six cube faces, W = 17 wallpaper groups, the fine-structure constant α, and π. Upstream, SpectralEmergence.of shows that the cube Q₃ simultaneously forces three generations, while PhiForcingDerived.of encodes the J-cost minimization that selects the golden ratio as the unique self-similar fixed point.
proof idea
The proof is a one-line term wrapper that applies the two specialized numeric bound lemmas phi_pow_residue_mu_lower and phi_pow_residue_mu_upper to construct the required conjunction.
why it matters
The lemma supplies a verified numerical anchor inside the T10 necessity argument for the lepton ladder, feeding directly into the RRF.Physics.LeptonGenerations.Necessity copies of the same bounds. It closes one link in the chain from T6 (phi forced) and T7 (eight-tick octave) to concrete mass predictions without extra axioms. The result also supports the downstream claim that the full set of lepton masses is determined by the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.