step_mu_tau_bounds
plain-language theorem explainer
The lemma establishes that step_mu_tau, the interval from muon to tau in the forced lepton ladder, satisfies 5.86 < step_mu_tau < 5.87. Physicists deriving Recognition Science mass predictions from the electron anchor would cite these bounds to confirm the tau residue without free parameters. The proof is a term-mode script that simplifies the definition via cube_faces and W_exact, pulls in alpha_bounds, and closes the inequality with nlinarith.
Claim. Let step_mu_tau denote the quantity 6 minus (2W + 3)/2 times the fine-structure constant α, where 6 equals the number of faces of the 3-cube and W equals 17. Then 5.86 < step_mu_tau < 5.87.
background
In Recognition Science the lepton generations form a forced ladder whose first rung is fixed by the electron mass (T9). The step_mu_tau interval is built from cube geometry (cube_faces = 2D, hence 6 for D = 3), the wallpaper count W = 17, and the fine-structure constant supplied by alpha_bounds. This module replaces the two axioms of LeptonGenerations.Defs with derived inequalities, using the eight-tick structure and the RCL to guarantee that only these geometric constants enter the mass formula.
proof idea
The term proof first rewrites step_mu_tau by unfolding its definition together with W_exact, AlphaDerivation.D and cube_faces. It obtains the alpha interval via alpha_bounds, then applies constructor followed by nlinarith to discharge both sides of the target inequality.
why it matters
The result supplies the numerical step that predicted_residue_tau_bounds consumes to bound the tau residue; that bound in turn completes the T10 necessity argument that muon and tau masses are forced once the electron mass and cube geometry are given. It therefore links T8 (D = 3) and the alpha band directly to observable lepton masses, closing one link in the chain from the universal forcing self-reference to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.