phi_pow_residue_tau_lower
plain-language theorem explainer
The inequality establishes that the golden ratio raised to the predicted tau residue exceeds 0.1629. Researchers deriving forced tau masses from the Recognition Science lepton ladder would cite it when combining the structural electron mass interval with residue calculations. The proof is a short tactic sequence that obtains the residue interval, applies strict monotonicity of the power map, and chains to a numeric lower bound at exponent -3.77.
Claim. $0.1629 < phi^{r}$ where $r$ is the predicted tau residue defined as the muon residue plus the muon-to-tau step, and this residue lies in the open interval $(-3.77, -3.75)$.
background
In the T10 module proving the lepton ladder is forced, muon and tau masses are derived from the electron structural mass (T9) together with geometric steps from cube edges, faces, wallpaper groups, and the fine-structure constant. The predicted tau residue is defined in LeptonGenerations.Defs as the sum of the predicted muon residue and the muon-tau step function. Upstream, phi_rpow_strictMono states that the map sending a real exponent to goldenRatio raised to that exponent is strictly increasing. The bounds lemma predicted_residue_tau_bounds places the residue strictly between -3.77 and -3.75. A separate numeric result confirms that goldenRatio to the power -3.77 exceeds 0.1629.
proof idea
The tactic proof first obtains the residue bounds via predicted_residue_tau_bounds. It rewrites phi to Real.goldenRatio, then applies phi_rpow_strictMono to deduce that goldenRatio to the power of the residue exceeds goldenRatio to -3.77. Finally it chains this comparison to the proved numeric inequality phi_pow_neg377_lower_proved inside a calc block, using simpa to discharge the hypothesis.
why it matters
This lower bound completes the interval for phi raised to the predicted tau residue when paired with the matching upper bound, directly enabling the tau mass lower bound theorems predicted_mass_tau_lower and predicted_mass_tau_lower_tight. It supports the T10 necessity claim that the tau mass is forced within (1768, 1791) MeV from the structural mass interval and the phi-ladder. The construction relies on the golden ratio fixed point from T5 J-uniqueness and the eight-tick octave. An open question remains whether tighter residue intervals can recover the observed tau mass of 1776.86 MeV without external numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.