step_mu_tau_face_count_forced
plain-language theorem explainer
If the μ→τ step equals f minus (37/2)α, then the leading face-count coefficient f must equal 6. Lepton-mass modelers cite this to close the geometric prefactor in the J-cost linear family. The proof is a short tactic sequence that reduces the hypothesis through the face-term lemma, evaluates cube_faces D via norm_num, and finishes with linarith.
Claim. If the μ→τ step satisfies step_μτ = f − (37/2)α, then f = 6.
background
The JCostPerturbation module supplies the O4 perturbative closure for lepton masses by expressing the μ→τ transition as a linear correction in the fine-structure constant α. The auxiliary definition cube_faces D returns 2D, the number of faces of the D-dimensional hypercube; the Recognition framework fixes D = 3, so the count is exactly 6. The theorem step_mu_tau_face_count_forced is the numeric special case of the more general face-term forcing result step_mu_tau_face_term_forced.
proof idea
Apply step_mu_tau_face_term_forced to the hypothesis to obtain f = cube_faces D. Then use norm_num on the definition cube_faces D = 2 * D together with the fixed value of D to reach cube_faces D = 6. Finish with linarith on the two equalities.
why it matters
The result is invoked by step_mu_tau_coeff_iff_full_forced_under_dim_bound and step_mu_tau_full_family_forced_from_coeff_match to obtain the full coefficient and dimension closure under the bound n ≤ D. It supplies the concrete face count required by the mass-layer J-cost bridge and is consistent with the D = 3 outcome of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.