phi_pow_residue_tau_upper_v2
plain-language theorem explainer
The declaration shows that the golden ratio raised to the predicted tau residue is strictly less than 0.16381. Physicists closing upper bounds on lepton masses within the Recognition Science framework cite it to bound the tau prediction. The proof is a short tactic sequence that applies strict monotonicity of the phi-power map and order transitivity to chain the residue interval to a known numerical bound.
Claim. Let $r_τ$ be the predicted tau residue (muon residue plus muon-to-tau step). Then $φ^{r_τ} < 0.16381$, where $φ$ is the golden ratio.
background
In the LeptonGenerations.Necessity module the predicted tau residue is defined as predicted_residue_mu + step_mu_tau, with both terms obtained from the geometric step functions of the lepton ladder. The module replaces two axioms from the parent LeptonGenerations file with proven bounds on muon and tau masses, using the electron structural mass from T9 together with cube-derived constants (E_passive = 11, faces = 6, W = 17) and the golden ratio fixed by T6. Upstream results supply the residue interval (-3.7619, -3.7603) and the auxiliary bound Real.goldenRatio^(-3.760) < 0.16381.
proof idea
Obtain the residue upper bound from predicted_residue_tau_bounds_v2. Rewrite phi as Real.goldenRatio. Use linarith to deduce residue < -3.760. Apply the strict-monotonicity lemma phi_rpow_strictMono to conclude the power is less than the value at -3.760. Finish with lt_trans to chain the inequality to phi_pow_neg3760_upper_v2.
why it matters
The result is invoked inside predicted_mass_tau_upper_v2 to obtain predicted_mass_tau < 1779. It completes the necessity argument for the tau rung of the lepton ladder, consistent with the eight-tick phase structure and the phi-ladder mass formula. The declaration closes one link in the T10 forcing chain that derives all lepton masses from the electron mass and geometric constants without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.