r0_Lepton_eq
plain-language theorem explainer
The declaration fixes the lepton sector phi-exponent offset at 62 inside the Recognition Science mass ladder. Researchers computing lepton yardsticks from cube geometry would cite this when evaluating the rung formula. The proof reduces directly by simplification of the sector definition followed by numerical normalization.
Claim. The phi-exponent offset for the lepton sector satisfies $r_0 = 62$.
background
In the Masses.Anchor module, canonical mass constants derive from cube geometry with D=3. Total edges equal 12, passive edges equal 11, and W stands for the 17 wallpaper groups. The r0 definition assigns offsets per sector: leptons receive 4W minus 6, which evaluates to 62. Upstream results supply wallpaper_groups as the Fedorov crystallographic constant 17 and the Sector inductive type that tags Lepton.
proof idea
The proof is a one-line wrapper that applies simp only on r0, W, and wallpaper_groups, then invokes norm_num to confirm the integer equality.
why it matters
This supplies the lepton rung offset for the mass formula yardstick times phi to the power (rung minus 8 plus gap). It feeds lepton_pred_eq_aux in Verification, which unfolds rs_mass_MeV and combines the offset with B_pow_Lepton_eq. The result closes the geometric derivation step in the canonical mass constants chain that begins from cube edges and wallpaper groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.