predicted_mass_tau_upper
plain-language theorem explainer
The theorem bounds the predicted tau mass below 1792 in Recognition Science units. Researchers deriving lepton hierarchies from geometric forcing cite it to close the upper limit on the third-generation rung. The proof unfolds the mass definition then chains the structural-mass interval with the phi-residue bound via nlinarith followed by norm_num.
Claim. Let $m_τ^pred = m_struct ⋅ φ^r$ where $m_struct$ is the electron structural mass and $r$ is the predicted tau residue. Then $m_τ^pred < 1792$.
background
The module T10 proves that the lepton ladder is forced once the electron structural mass and the golden-ratio steps are fixed. The structural mass is the lepton yardstick scaled by φ to the power of the electron rung offset by the octave period; it satisfies the tight interval 10856 < m_struct < 10858. The tau residue is the muon residue plus the muon-to-tau step, and the phi-power of that residue is bounded above by 0.165.
proof idea
The tactic proof first simplifies the definition of predicted_mass_tau. It then obtains the structural-mass bounds and the phi-residue upper bound, applies a calc block with nlinarith to the product inequality 10858 ⋅ 0.165, and finishes with norm_num to reach the target 1792.
why it matters
The result supplies the upper half of tau_mass_pred_bounds_proven, which replaces the original axiom for the tau mass in the lepton-generations necessity theorem. It therefore completes the T10 forcing chain that begins from the electron structural mass (T9) and the phi fixed point (T6). The bound keeps the entire predicted ladder inside the interval required by the eight-tick octave and the observed alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.