phi_pow_residue_mu_lower
plain-language theorem explainer
This result supplies the strict lower bound 0.0097 < φ^r_μ on the golden-ratio power of the predicted muon residue. Workers closing the lepton-mass ladder from the electron structural mass would cite the bound when converting residue intervals into mass predictions. The argument is a short chain that invokes the strict monotonicity of x ↦ φ^x on the residue lower limit -9.63 together with a pre-established numerical comparison φ^(-9.63) > 0.0097.
Claim. Let φ denote the golden ratio. Let r_μ be the predicted muon residue defined by r_μ = (gap(1332) - refined_shift) + step_{e→μ}. Then 0.0097 < φ^{r_μ}.
background
The module replaces two lepton-generation axioms with derived inequalities that follow from the electron structural mass (T9) and the geometric constants of the cube. The predicted muon residue is the sum of a phi-ladder gap term, a refined shift, and the electron-to-muon step obtained from cube-face and wallpaper-group counts together with the fine-structure constant. Upstream, the monotonicity lemma records that φ^x is strictly increasing on the reals because φ > 1. The residue bounds lemma supplies the concrete interval -9.63 < r_μ that feeds the present inequality.
proof idea
Apply the strict-monotonicity lemma for the map x ↦ goldenRatio^x to the lower bound on the exponent taken from predicted_residue_mu_bounds. The resulting comparison goldenRatio^(-9.63) < goldenRatio^r_μ is then chained by calculation with the numerical fact that 0.0097 < goldenRatio^(-9.63).
why it matters
The bound is the left half of the combined interval lemma phi_pow_residue_mu_bounds and is invoked directly by the muon-mass lower-bound theorems predicted_mass_mu_lower and predicted_mass_mu_lower_tight. It therefore supplies one concrete step in the T10 necessity program that forces the muon mass from the electron mass, the eight-tick octave, and the phi self-similar fixed point. The result leaves open whether tighter residue intervals can be extracted from the same geometric data to reach the observed 105.658 MeV value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.