phi_pow_residue_mu_lower
plain-language theorem explainer
This result establishes a strict lower bound of 0.0097 on the golden ratio raised to the predicted muon residue. Researchers deriving forced lepton masses from the Recognition Science forcing chain cite it when anchoring the muon mass interval from below. The proof is a short tactic sequence that applies the strict monotonicity of the power map for base greater than one to a residue lower bound, then chains the result with a numerical boundary inequality.
Claim. $0.0097 < phi^{r}$ where $r$ is the predicted muon residue obtained from the gap at 1332, the refined shift, and the electron-to-muon step function.
background
The T10 Necessity module shows that the lepton ladder is forced once the electron structural mass from T9 and the geometric constants (including phi from T4) are in place. The predicted muon residue is the real number formed by adding the gap term at rung 1332, subtracting the refined shift, and adding the electron-muon step. The supporting monotonicity result states that since phi exceeds 1 the map sending an exponent to phi raised to that exponent is strictly increasing.
proof idea
The proof obtains the residue lower bound -9.63 from the residue bounds lemma. It rewrites phi as the golden ratio and applies the strict monotonicity lemma to produce the inequality between phi to the power -9.63 and phi to the power of the residue. A calculation then inserts the already-proved numerical fact that phi to the power -9.63 exceeds 0.0097.
why it matters
The lower bound supplies one half of the phi-power bounds lemma that feeds the predicted muon mass lower bound theorems. It advances the T10 program of replacing lepton-generation axioms with derived inequalities built from the eight-tick octave and the phi-ladder. The argument closes a necessary step in showing that the muon mass interval is forced by the same cube geometry and alpha derivation that fix the electron mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.