phi_pow_residue_mu_bounds
plain-language theorem explainer
The lemma establishes the numerical interval 0.0097 < φ^{r_μ} < 0.0098 for the muon residue exponent in the lepton ladder. Researchers deriving forced lepton masses from geometric constants and the golden ratio would cite it when closing the T10 necessity argument. The proof is a one-line wrapper that pairs the separately proved lower and upper bounds.
Claim. Let φ be the golden ratio. Let r_μ be the predicted residue exponent for the muon. Then 0.0097 < φ^{r_μ} < 0.0098.
background
The module proves T10 necessity: the muon and tau masses are forced once the electron structural mass (T9) and the geometric step functions are fixed. These steps combine E_passive = 11, cube faces = 6, wallpaper count W = 17, the fine-structure constant α, and π from spherical geometry, all scaled by φ from the self-similar fixed point (T6). The residue exponent r_μ is computed in the sibling Defs module from these inputs and the phi-ladder mass formula.
proof idea
The proof is a one-line wrapper that applies the lower-bound lemma phi_pow_residue_mu_lower together with the upper-bound lemma phi_pow_residue_mu_upper.
why it matters
The result supplies the tight residue factor needed for the muon-mass prediction inside the T10 lepton-ladder necessity argument. It is used by the corresponding tau-residue bound and thereby supports replacement of the original axioms in LeptonGenerations with derived inequalities. The construction rests on the eight-tick octave and D = 3 forced by the upstream chain (T5–T8) together with the three-generation structure from SpectralEmergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.