phi_pow_residue_tau_lower_v2
plain-language theorem explainer
The inequality shows that the golden ratio raised to the predicted tau residue exceeds 0.1635, supplying the numerical lower anchor needed for the tau mass bound. Physicists closing the lepton mass hierarchy in Recognition Science cite it to replace an axiom with a derived inequality inside the T10 necessity argument. The proof is a short chain that feeds the residue interval into the strict monotonicity of φ^x and composes it with a base case at exponent -3.762.
Claim. $0.1635 < φ^{r_τ}$ where $r_τ$ is the predicted tau residue defined by $r_μ + Δ_{μτ}$, $φ$ is the golden ratio, and the residue interval satisfies $-3.7619 < r_τ < -3.7603$.
background
Module T10 proves that the muon and tau masses are forced once the electron structural mass (T9) and the geometric constants (cube edges, faces, wallpaper groups, α, π) are in place. The predicted_residue_tau is the sum of the muon residue and the mu-to-tau step; both quantities descend from the phi-ladder mass formula yardstick · φ^{rung-8+gap(Z)} and the Recognition Composition Law. Upstream results supply the base inequality 0.1635 < φ^{-3.762} together with the strict monotonicity of x ↦ φ^x for φ > 1.
proof idea
Obtain the residue bounds from predicted_residue_tau_bounds_v2, derive -3.762 < predicted_residue_tau by linarith, then apply lt_trans to phi_pow_neg3762_lower_v2 and the lemma phi_rpow_strictMono that φ^x is strictly increasing.
why it matters
The result is invoked by predicted_mass_tau_lower_v2 to obtain 1774 < predicted_mass_tau, completing the lower half of the tau mass necessity statement. It sits inside the T10 forcing chain that derives the entire lepton ladder from T9, the eight-tick octave, D = 3, and the self-similar fixed point φ; no scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.