phi_pow_residue_tau_upper
plain-language theorem explainer
The theorem proves that the golden ratio raised to the predicted tau residue is strictly less than 0.165. Researchers bounding the tau lepton mass in the Recognition Science lepton ladder cite this to close the upper estimate chain from the electron structural mass. The proof applies strict monotonicity of the power map to the residue bounds lemma, then reduces to a pre-established numeric inequality on phi to the power -3.75.
Claim. Let $r$ denote the predicted tau residue, defined as the sum of the predicted muon residue and the muon-to-tau step. Then $r$ satisfies $-3.77 < r < -3.75$, and consequently $phi^r < 0.165$.
background
The module establishes T10 necessity for the lepton ladder, showing that muon and tau masses are forced from the electron structural mass (T9) together with cube-derived constants and the golden ratio fixed point. The predicted tau residue is the sum of the muon residue and the muon-to-tau step, with explicit bounds supplied by the sibling lemma predicted_residue_tau_bounds that place it in the open interval (-3.77, -3.75).
proof idea
The proof obtains the residue interval from predicted_residue_tau_bounds, invokes phi_rpow_strictMono to conclude that phi raised to the residue is strictly less than phi raised to -3.75, then applies the pre-proved theorem phi_pow_neg375_upper_proved (which establishes the numeric claim phi^{-3.75} < 0.165) via a direct calculation.
why it matters
This supplies the upper half of phi_pow_residue_tau_bounds, which is invoked directly by predicted_mass_tau_upper and predicted_mass_tau_upper_tight to bound the tau mass below 1792 (and more tightly below 1791.6). It completes one link in the T10 necessity argument that replaces axiomatic lepton masses with inequalities derived from the phi-ladder and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.