phi_pow_residue_tau_lower
plain-language theorem explainer
The inequality establishes 0.163 < φ raised to the predicted tau residue, supplying the lower anchor for tau mass bounds in the lepton ladder. Workers deriving forced masses from the phi-ladder and cube geometry cite it to close the T10 necessity step. The term proof obtains the residue interval from predicted_residue_tau_bounds, invokes strict monotonicity of the golden-ratio power map, and chains the numeric bound at exponent -3.77.
Claim. $0.163 < φ^r$ where $r$ denotes the predicted tau residue, defined as the muon residue plus the mu-to-tau step and known to lie in $(-3.77, -3.75)$.
background
Module T10 Necessity replaces two axioms in LeptonGenerations with proven inequalities for muon and tau masses. The predicted tau residue is the sum of the predicted muon residue and the mu-tau step function, both derived from cube-face counts, wallpaper groups, and the fine-structure constant. Upstream, phi_rpow_strictMono asserts that $φ^x$ is strictly increasing on the reals for $φ$ the golden ratio. The companion bounds lemma states that the residue lies strictly between -3.77 and -3.75, while phi_pow_neg377_lower supplies the concrete numeric comparison $0.163 < φ^{-3.77}$.
proof idea
Term proof first calls predicted_residue_tau_bounds to obtain the open interval on the exponent. It rewrites φ as Real.goldenRatio, applies phi_rpow_strictMono to transfer the lower endpoint to the power, then chains the pre-proven numeric inequality phi_pow_neg377_lower through the resulting comparison.
why it matters
The result is invoked by phi_pow_residue_tau_bounds to close the sandwich on the power value and by predicted_mass_tau_lower to obtain the structural lower bound 1769 < predicted_mass_tau. It completes one link in the T10 chain that forces the lepton ladder from the electron structural mass, the eight-tick octave, and the phi-ladder mass formula. The interval remains wide enough that observed tau mass 1776.86 MeV still lies inside the predicted range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.