lepton_params_derived
plain-language theorem explainer
The lepton sector of the RS mass ladder has fixed geometric parameters equal to −22 (power-of-two yardstick exponent) and 62 (base φ-rung offset). Anyone comparing electron, muon, or tau mass predictions to PDG data cites this pair. The proof is a two-conjunct term that reuses the already-proved cube-edge and wallpaper equalities for that sector.
Claim. For the lepton sector, the derived power-of-two yardstick exponent equals $-22$ and the derived base $\varphi$-rung offset equals $62$.
background
The MassComparison module checks Recognition Science mass predictions against PDG 2024 values. It is quarantined from the certified surface because it imports experimental numbers and the φ-ladder anchor system. The sector mass formula is
$m = \mathrm{yardstick} \times \varphi^{r_0 + r_{\mathrm{species}}}$,
with $\mathrm{yardstick} = 2^{B} \times E_{\mathrm{coh}} \times \varphi^{r_0}$ and coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$.
$B$ and $r_0$ are sector integers fixed by cube geometry and wallpaper counting, not free fits. For leptons the definitions give $B = -(2 E_{\mathrm{passive}}) = -22$ (passive field edges on the cube) and $r_0 = 4W - 6 = 62$ (wallpaper group count $W = 17$). Upstream equalities B_pow_Lepton_eq and r0_Lepton_eq already discharge those arithmetic identities by simp and norm_num.
proof idea
Term-mode conjunction. constructor splits the goal into the two equalities; each conjunct is discharged by exact on the corresponding upstream lemma (B_pow_Lepton_eq for the power-of-two exponent, r0_Lepton_eq for the base rung). No new arithmetic is performed here.
why it matters
Locks the lepton yardstick and base rung that feed every electron/muon/tau mass comparison in this module. Without these two integers the φ-ladder formula cannot be evaluated against PDG. They instantiate the primer mass rule (yardstick × φ^(rung − 8 + gap)) for the lepton sector and record that both numbers come from cube-edge and wallpaper geometry rather than phenomenological tuning. No downstream theorems currently depend on this wrapper (used_by is empty); it is a verification checkpoint inside the quarantined comparison layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.