predicted_residue_mu_bounds
plain-language theorem explainer
The lemma pins the predicted muon residue between -9.63 and -9.62. Researchers deriving lepton masses from the Recognition Science ladder cite this to anchor the muon prediction before exponentiating to mass. The proof reduces the definition via simplification, pulls in the gap-shift and step bounds, and closes with linear arithmetic.
Claim. Let $r = F(1332) - s + Delta_{e mu}$, where $F(Z) = ln(1 + Z/phi)/ln(phi)$ is the gap function at the anchor scale, $s$ the refined shift, and $Delta_{e mu}$ the electron-muon step. Then $-9.63 < r < -9.62$.
background
The module establishes necessity for the lepton ladder under T10, showing muon and tau masses follow from the electron mass at T9 together with geometric constants from cube symmetry and the golden ratio. The predicted muon residue combines the anchor gap at charge index 1332, a refined shift, and the step from electron to muon driven by cube faces and wallpaper groups.
proof idea
Simplification unfolds the definition of the predicted muon residue. The proof then obtains the gap-minus-shift bounds via the dedicated lemma gap_minus_shift_bounds_proven and the electron-muon step bounds via step_e_mu_bounds. Constructor splits the conjunction and linarith discharges both sides.
why it matters
This result feeds the lower and upper bounds on phi raised to the muon residue, which in turn support the tau residue bounds. It advances the T10 claim that the lepton ladder is forced from prior electron mass and phi-derived constants. The parent chain reaches mass predictions that match observed values within the derived intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.