predicted_mass_tau_lower_tight
plain-language theorem explainer
This result supplies a strict lower bound of 1768.4 on the predicted tau mass obtained by scaling the electron structural mass by a phi-power residue. Researchers deriving lepton masses from the Recognition Science forcing chain cite it to fix the lower edge of the tau prediction interval. The proof reduces the claim to a numerical comparison by invoking the structural mass bounds and the phi-power inequality, then closes the chain with norm_num followed by nlinarith.
Claim. $1768.4 < m_τ^{pred}$, where $m_τ^{pred} := m_{struct} ⋅ φ^{r_τ}$, $m_{struct}$ is the electron structural mass (bounded between 10856 and 10858), and $r_τ$ is the predicted residue for the tau generation.
background
In the T10 Necessity module the lepton ladder is forced from the electron mass (T9) together with geometric constants derived from cube geometry and the eight-tick octave. The electron structural mass equals lepton_yardstick times phi to the power (electron_rung minus octave period) and is proven to satisfy 10856 < m_struct < 10858. The predicted tau mass is defined as the product of this structural mass with phi raised to the predicted residue tau, where the residue itself is the sum of the muon residue and the muon-to-tau step function.
proof idea
The tactic proof first simplifies the definition of predicted_mass_tau to expose the product form. It obtains the structural-mass lower bound from ElectronMass.Necessity.structural_mass_bounds and the phi-power lower bound from phi_pow_residue_tau_lower. A calc block verifies the numerical inequality 1768.4 < 10856 * 0.1629 by norm_num; nlinarith then combines the two inequalities to reach the target product.
why it matters
This theorem supplies the lower half of tau_mass_pred_bounds_tight, which tightens the tau-mass prediction to the interval (1768.4, 1791.6). It completes part of the T10 necessity argument that the lepton generations are determined by the eight-tick octave and the phi-ladder without extra axioms. The result sits downstream of the electron structural mass bounds (T9) and the residue calculations, and upstream of the full lepton mass bounds used in spectrum comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.