step_mu_tau_coeff_forced_from_six_face_term
plain-language theorem explainer
The theorem shows that the linear coefficient c in the expansion step_mu_tau = 6 - c α is forced to equal 37/2. Researchers closing perturbative coefficients for lepton mass ratios in the Recognition Science mass layer would cite this specialization. The tactic proof equates the constant term to the three-dimensional cube face count and reduces directly to the general linear forcing lemma.
Claim. If the muon-to-tau step satisfies step_mu_tau = 6 - c α, then the coefficient equals 37/2.
background
The module supplies the O4 perturbative closure for J-cost perturbations on lepton masses, certifying the form Jcost(1+α) together with its α² + 12α³ radiative decomposition. Here α denotes the fine-structure constant, defined as the reciprocal of the derived alphaInv. The constant 6 arises as cube_faces D for D=3, where cube_faces(d) := 2d counts the faces of the D-hypercube. The proof invokes the sibling result step_mu_tau_linear_coeff_forced, which forces the coefficient in the general denominator family F - ((2W + D)/k)α under canonical matching.
proof idea
The tactic proof first applies norm_num to establish 6 = cube_faces D, rewrites the hypothesis to match the general form, and then applies the lemma step_mu_tau_linear_coeff_forced.
why it matters
This declaration specializes the general linear coefficient forcing to the six-face geometric term required by D=3. It forms part of the O4 coefficient closure package in the mass layer and supports sibling results such as mass_topology_counts and ledger_fraction_denominator_forced. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.