predicted_mass_tau_lower
plain-language theorem explainer
The theorem establishes that the predicted tau mass exceeds 1768 in Recognition Science units. Researchers deriving forced lepton spectra from geometric constants would cite this to anchor the lower edge of the tau rung. The short tactic proof chains the proven structural mass interval with a separate lower bound on the phi-powered residue via a direct numerical comparison followed by linear arithmetic.
Claim. $1768 < m_0^Y$ where $m_0^Y$ denotes the electron structural mass scaled by the golden ratio to the power of the tau residue exponent.
background
The T10 module derives the lepton ladder from the electron structural mass and phi-powered steps forced by cube geometry. The structural mass is the lepton yardstick multiplied by phi raised to the electron rung offset by the octave period, and a prior theorem places it strictly between 10856 and 10858. The tau residue is obtained by adding the mu-to-tau step to the muon residue, with a companion result showing that phi to this power exceeds 0.1629. The module replaces earlier axioms on muon and tau masses with inequalities built from the eight-tick structure, cube faces, and wallpaper groups.
proof idea
The proof rewrites the predicted tau mass as the product of the structural mass and phi to the residue power. It pulls in the structural mass bounds theorem together with the phi-power residue lower bound theorem. A calculation first verifies that 1768 lies below 10856 times 0.1629, after which nlinarith combines the two interval inequalities to reach the desired product bound.
why it matters
The result supplies the lower half of the interval that replaces the original tau mass axiom inside the lepton generations necessity module. It advances the T10 forcing step that obtains the full lepton ladder from the T9 electron mass together with the golden ratio fixed point and the eight-tick octave. The derived interval (1768, 1792) comfortably contains the observed tau mass while remaining strictly geometric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.