phi_pow_residue_mu_bounds
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.
claimLet ϕ 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of the residue exponent itself.
- Does not compute the absolute muon mass.
- Applies only to the muon; separate bounds are required for the tau.
- Relies on externally computed numeric intervals for the residue.
formal statement (Lean)
583lemma phi_pow_residue_mu_bounds :
584 (0.0097 : ℝ) < phi ^ predicted_residue_mu ∧ phi ^ predicted_residue_mu < (0.0098 : ℝ) :=
proof body
Term-mode proof.
585 ⟨phi_pow_residue_mu_lower,
586 phi_pow_residue_mu_upper⟩
587
588/-! CORRECTED: φ^(predicted_residue_tau) where residue_tau ∈ (-3.77, -3.75)
589Previous claim of 0.346 < φ^residue < 0.348 was FALSE!
590Actual: φ^(-3.76) ≈ 0.164
591Conservative seam bounds: φ^(-3.77) > 0.1629 and φ^(-3.75) < 0.165. -/
592
593/-- External numeric hypothesis: φ^(-3.77) > 0.1629. -/