predicted_residue_mu
The definition computes the predicted muon residue in the lepton mass ladder as the gap at charge index 1332 minus the refined shift, plus the electron-to-muon geometric step. Researchers deriving lepton masses from the Recognition Science phi-ladder would cite this when assembling the muon mass from the electron structural mass. The definition is a direct algebraic assembly of the gap function, shift correction, and step term drawn from upstream geometry and topology results.
claimThe predicted muon residue is defined by $r_μ = F(1332) - Δ + s_{eμ}$, where $F(Z) = ln(1 + Z/φ)/ln(φ)$ is the gap function at the anchor scale, $Δ$ is the refined shift combining base and radiative terms, and $s_{eμ}$ is the electron-to-muon step incorporating passive edges and the spherical factor $1/(4π)$ minus $α^2$.
background
The T10 Lepton Generations module isolates core definitions to break import cycles in the mass derivations. The gap function $F(Z)$ is the closed-form residue at the anchor scale, given by the logarithmic ratio that equals the integrated mass anomalous dimension for a fermion species with charge index Z. The refined shift is the sum of a base geometric shift and a radiative correction from mass topology. The electron-to-muon step adds the passive-edge contribution (11) to the spherical-geometry term (1/(4π)) and subtracts $α^2$.
proof idea
This is a one-line definition that directly assembles the residue by subtracting the refined shift from the gap evaluated at 1332 and adding the precomputed electron-muon step. It applies the gap definition from the RSBridge anchor, the refined_shift definition from MassTopology, and the step_e_mu definition from the same module.
why it matters in Recognition Science
This supplies the exponent for the predicted muon mass, which is formed as the electron structural mass times $φ$ raised to this residue. It feeds the T10 lepton ladder forced from T9, incorporating cube geometry (passive edges and faces), wallpaper symmetry, and the fine-structure constant. Downstream necessity lemmas use it to bound $φ^{r_μ}$ between 0.0097 and 0.0098 and to prove the full muon and tau masses are determined by the electron mass plus these geometric inputs.
scope and limits
- Does not establish numerical bounds on the residue value itself.
- Does not include higher-order radiative or topological corrections beyond the refined shift.
- Does not compute the tau residue or mass; those build on this definition.
- Does not claim numerical agreement with the experimental muon mass without the full structural-mass formula.
Lean usage
noncomputable def predicted_mass_mu : ℝ := electron_structural_mass * phi ^ predicted_residue_muformal statement (Lean)
49noncomputable def predicted_residue_mu : ℝ :=
proof body
Definition body.
50 (gap 1332 - refined_shift) + step_e_mu
51
52/-- Predicted Tau Residue. -/
used by (28)
-
predicted_mass_mu -
predicted_residue_tau -
gap_minus_shift_bounds_proven -
phi_pow_residue_mu_bounds -
phi_pow_residue_mu_lower -
phi_pow_residue_mu_lower_v2 -
phi_pow_residue_mu_upper -
phi_pow_residue_mu_upper_v2 -
predicted_mass_mu_lower -
predicted_mass_mu_lower_tight -
predicted_mass_mu_lower_v2 -
predicted_mass_mu_upper -
predicted_mass_mu_upper_tight -
predicted_mass_mu_upper_v2 -
predicted_residue_mu_bounds -
predicted_residue_mu_bounds_v2 -
predicted_residue_tau_bounds -
predicted_mass_mu -
predicted_residue_mu -
predicted_residue_tau -
phi_pow_residue_mu_bounds -
phi_pow_residue_mu_lower -
phi_pow_residue_mu_upper -
predicted_mass_mu_lower -
predicted_mass_mu_upper -
predicted_residue_mu_bounds -
predicted_residue_tau_bounds -
step_mu_tau_bounds