step_mu_tau_kn_forced_under_dim_bound
plain-language theorem explainer
Joint Diophantine forcing for the μ→τ coefficient family shows that n ≤ D together with the canonical match step_mu_tau = cube_faces D - ((2W + n)/k) α forces k = 2 and n = D. Lepton mass modelers cite the result to pin the denominator and rung index in the Recognition Science mass ladder. Algebraic cancellation of α followed by integer bounding and case analysis on k yields the unique solution.
Claim. Assume positive integers $k$ and $n$ satisfy $n ≤ D$. If step_μτ = 2D − ((2W + n)/k) α with W the number of wallpaper groups, then k = 2 and n = D.
background
The J-Cost Perturbation module expresses the μ→τ lepton step in the form F − ((2W + n)/k)α, where F = cube_faces D = 2D and W = wallpaper_groups = 17. The bound n ≤ D keeps the perturbation index inside the spatial dimension D fixed by the framework. Upstream constants supply alpha as the fine-structure constant 1/alphaInv, cube_faces(d) := 2d, and wallpaper_groups = 17 from the 1891 crystallographic count.
proof idea
The argument invokes step_mu_tau_channel_split to obtain the canonical form 6 − (37/2)α, then equates coefficients after norm_num simplification on D = 3. Alpha positivity cancels the fine-structure term, reducing to (2W + n)/k = 37/2. Cross-multiplication produces the Diophantine equation 2(2W + n) = 37k. With n ≤ 3 and W = 17 the left side is at most 37, forcing k ≤ 2; case analysis eliminates k = 1 by contradiction, leaving k = 2 and n = 3 = D.
why it matters
This supplies the Diophantine core for downstream μ→τ theorems including step_mu_tau_coeff_iff_kn_under_dim_bound and step_mu_tau_full_family_forced_under_dim_bound. It completes the O4 perturbative closure for lepton mass steps by forcing the coefficient family under the dimensional bound, consistent with D = 3 and the alpha band. The result removes the need for separate positivity hypotheses on k in related statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.