phi_pow_residue_tau_upper
plain-language theorem explainer
phi_pow_residue_tau_upper establishes that the golden ratio raised to the predicted tau residue is strictly less than 0.165. Lepton mass modelers working in the Recognition Science framework cite it to close the upper bound on the tau mass prediction. The argument obtains the residue interval from sibling bounds, applies strict monotonicity of the phi-power map, and chains to a pre-established numeric threshold at exponent -3.75.
Claim. Let φ denote the golden ratio and let r_τ be the predicted tau residue defined as the sum of the predicted muon residue and the muon-to-tau step. Then φ^{r_τ} < 0.165.
background
The module T10 Necessity proves that the muon and tau masses are forced from the electron structural mass (T9) together with geometric constants derived from cube faces, wallpaper groups, and the fine-structure constant. The predicted residue for the tau is defined in LeptonGenerations.Defs as predicted_residue_tau := predicted_residue_mu + step_mu_tau, with bounds (-3.77, -3.75) supplied by the sibling lemma predicted_residue_tau_bounds. Upstream, the lemma phi_rpow_strictMono states that φ > 1 so φ^x is strictly increasing in x.
proof idea
The proof obtains the residue bounds via predicted_residue_tau_bounds. It rewrites phi as Real.goldenRatio and applies the strict monotonicity lemma phi_rpow_strictMono to the upper endpoint, yielding phi^residue < phi^(-3.75). It then chains directly to the numeric result phi_pow_neg375_upper that goldenRatio^(-3.75) < 0.165.
why it matters
This supplies the upper half of phi_pow_residue_tau_bounds, which is invoked in predicted_mass_tau_upper and predicted_mass_tau_upper_tight to bound the predicted tau mass below 1792 (or tighter 1791.6) via multiplication by the structural mass interval. It closes one side of the T10 forcing argument for the lepton ladder, consistent with the phi fixed point (T6), eight-tick octave (T7), and D=3 (T8). The result touches the open question of deriving the exact residue without external numeric thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.