step_mu_tau_numerator_offset_forced
plain-language theorem explainer
In the J-cost perturbation for lepton masses, the theorem shows that matching the muon-tau step to the form involving hypercube faces minus a scaled alpha term forces the integer offset n to equal the dimension D. Researchers deriving lepton mass ratios from Recognition Science constants would reference this to close the coefficient family. The proof derives the canonical D-version by simplification, equates the alpha-multiplied coefficients via linear arithmetic and cancellation, then recovers n = D by natural-number left cancellation.
Claim. Let $F_D = 2D$ denote the number of faces of the D-dimensional hypercube and let $W = 17$ be the number of wallpaper groups. If the muon-tau step equals $F_D - ((2W + n)/2) alpha$, where $alpha$ is the fine-structure constant, then $n = D$.
background
The module supplies the Lean closure package for O4 perturbative coefficients in the mass layer, linking J-cost perturbations to canonical lepton-step definitions. Key definitions include the fine-structure constant $alpha := 1/alphaInv$, cube_faces(D) := 2D, and wallpaper_groups := 17 (Fedorov 1891). Upstream results include arithmetic cancellation lemmas such as add_left_cancel, which transfers equality via the recovery isomorphism to natural numbers.
proof idea
The tactic proof first simplifies to obtain the canonical expression with D. It establishes positivity of alpha from bounds, equates the scaled terms by linarith on the hypothesis and canonical form, cancels the nonzero alpha factor via mul_right_cancel, recovers the coefficient equality by nlinarith, casts to naturals, and applies Nat.add_left_cancel to conclude n = D.
why it matters
This result completes the Diophantine forcing for the mu-to-tau coefficient family in the numerator-offset form F - ((2W+n)/2)alpha, ensuring the offset equals D. It supports the O4 closure in the J-cost perturbation module and feeds sibling declarations on mass topology counts and ledger fractions. Within Recognition Science it reinforces spatial dimension forcing (D=3) by tying perturbative corrections to hypercube geometry and wallpaper group count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.