step_mu_tau_linear_coeff_forced
plain-language theorem explainer
The theorem forces the linear coefficient of alpha in the muon-to-tau step to equal 37/2 whenever the constant term matches the face count of the three-cube. Researchers deriving lepton mass hierarchies from Recognition Science J-cost expansions would cite this to fix the first-order correction. The argument first rewrites the step via channel split to the explicit 6 minus (37/2) alpha form, then cancels the positive alpha multiplier using supplied bounds.
Claim. If the canonical muon-to-tau step satisfies $s = 2D - c α$ with $D = 3$, then $c = 37/2$.
background
The JCostPerturbation module supplies the O4 perturbative closure for mass-layer calculations by expressing lepton steps in the linear family constant minus coefficient times alpha. The function cube_faces counts 2D faces of a D-dimensional hypercube and equals 6 for the forced D = 3. Alpha is defined as the reciprocal of the derived inverse fine-structure constant. The canonical step_mu_tau_channel_split supplies the invariant zeroth-order expression that the proof matches against the given linear form.
proof idea
The proof first builds an auxiliary equality step_mu_tau = 6 - (37/2) alpha by applying the channel split lemma and simplifying the cube faces count for D = 3. It then extracts positivity and nonzeroness of alpha from the supplied bounds. Subtracting the two expressions for the step produces a common alpha term that is canceled by right multiplication inverse.
why it matters
This coefficient forcing result is the direct input to the sibling theorems step_mu_tau_coeff_forced_from_six_face_term and step_mu_tau_full_affine_forced_from_face_term that close the full affine match for the muon-tau step. It completes one piece of the O4 coefficient forcing inside the mass perturbation bridge, consistent with geometric face counting in three dimensions and the forced alpha value. No open scaffolding remains for this linear coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.