step_mu_tau_scale_forced_no_hc_pos
plain-language theorem explainer
The result forces the real-scale denominator c in the μ→τ mass-step matching to equal 2 when the expression is written in the canonical form that subtracts a geometric multiple of alpha from the hypercube face count. Lepton-mass workers in the Recognition Science program cite it to certify the O4 coefficient without a separate positivity hypothesis on c. The tactic proof first rules out c = 0 by contradiction with alpha positivity, then equates the alpha coefficients, cancels alpha, and cross-multiplies to reach the equality.
Claim. Let $F = 2D$, $W = 17$, and let $α$ be the fine-structure constant. If the muon-tau step satisfies $Δ_{μτ} = F - ((2W + D)/c) α$, then $c = 2$.
background
The J-Cost Perturbation module expresses lepton mass steps through perturbative corrections linear in the fine-structure constant alpha. cube_faces(D) evaluates to 2D, the face count of a D-dimensional hypercube, while wallpaper_groups is the fixed crystallographic number 17. The canonical step_mu_tau is supplied by the channel-split identity as 6 - (37/2) alpha, which matches the geometric form precisely when D = 3 and the numerator 2W + D equals 37.
proof idea
Tactic-mode proof. First prove c ≠ 0 by assuming c = 0, substituting into the hypothesis to obtain step_mu_tau equal to the face count, then using step_mu_tau_channel_split and norm_num to reach 6 - (37/2) alpha and deriving a contradiction with alpha > 0 from alpha_bounds. With c nonzero, derive the canonical expression, obtain alpha ≠ 0, equate the two alpha-coefficient expressions by linarith, cancel alpha via mul_right_cancel, simplify the numerator to 37, apply div_eq_div_iff, and finish with nlinarith on the cross-multiplied relation 37 · 2 = 37 · c.
why it matters
The theorem supplies the positivity-free forcing step that is packaged into the downstream family result step_mu_tau_full_real_family_forced_from_face_term_no_hc_pos and the equivalence step_mu_tau_scale_iff_face_count_no_hc_pos. It belongs to the O4 coefficient-forcing closure in the JCostPerturbation module, which certifies the J-cost(1 + α) perturbative channel form and the exact geometric evaluation of the zeroth-order constants. In the Recognition Science chain it fixes the linear alpha correction inside the mass formula on the phi-ladder at the lepton level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.