step_mu_tau_face_term_forced
plain-language theorem explainer
The theorem shows that if the muon-to-tauon step equals f minus (37/2) alpha then the constant term f equals the number of faces on the D-dimensional hypercube. Lepton mass modelers cite it to anchor the geometric prefactor in the J-cost perturbation for the mu-tau channel. The proof first derives the canonical expression for the step via channel splitting and norm_num, then applies linarith to match the given hypothesis.
Claim. Assume the muon-to-tauon step satisfies $step_{μτ} = f - (37/2)α$. Then the constant term obeys $f = 2D$, where $D$ is the number of spatial dimensions and $α$ is the fine-structure constant.
background
The J-Cost Perturbation module bridges O4 perturbative mass corrections to canonical lepton-step definitions and certifies the Jcost(1+α) channel form together with geometric evaluations of zeroth-order constants. Cube_faces D is the function returning 2D (hence 6 when D=3), while alpha is the fine-structure constant 1/alphaInv. Step_mu_tau is the base term in the mu-to-tau mass ratio inside the phi-ladder construction.
proof idea
The proof constructs a canonical expression for step_mu_tau by applying the channel-split lemma to obtain 6 minus (37/2)alpha, then rewrites the 6 via norm_num on the definitions of cube_faces and D. Linear arithmetic (linarith) equates the hypothesis to this canonical form and solves for f.
why it matters
The result feeds the downstream theorem step_mu_tau_face_count_forced that forces the numeric value 6. It supplies the geometric matching step inside the O4 perturbative closure for lepton masses, consistent with the T8 forcing of D=3 and the cube_faces definition. It closes one coefficient-forcing link in the alpha band without addressing higher-order radiative terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.