B_pow_Lepton_eq
The lepton-sector B-power offset equals -22, fixed by three-dimensional cube edge counting in the Recognition mass ladder. Mass-model builders cite this when assembling the phi-exponent rung for charged leptons and neutrinos. The proof reduces directly via simplification of the B_pow definition together with the passive-edge and cube-edge constants, followed by arithmetic normalization.
claimFor the lepton sector the derived power-of-two offset satisfies $B_mathrm{pow}(mathrm{Lepton}) = -22$.
background
The Masses.Anchor module centralizes parameter-free constants for the Recognition mass formula, all derived from D=3 cube geometry. Key quantities include E_total = cube_edges D = 12 total edges, E_passive = passive_field_edges D = 11 passive edges, A = active_edges_per_tick = 1, and W = wallpaper_groups = 17. The B_pow definition assigns to each Sector an integer offset: for Lepton it is -(2 * E_passive).
proof idea
The proof is a term-mode one-liner that unfolds B_pow, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, and D, then applies norm_num to compute the arithmetic value -22.
why it matters in Recognition Science
This theorem supplies the lepton B_pow value to the downstream lepton_pred_eq_aux lemma in Masses.Verification, which supports rs_mass_MeV computations for leptons. It realizes the sector constants derived from cube geometry (D=3) and wallpaper groups as described in the module documentation, consistent with the T8 forcing step that fixes spatial dimensions.
scope and limits
- Does not assert agreement between derived masses and experimental data.
- Does not extend the equality to other sectors.
- Does not incorporate quantum corrections or anomalous moments.
- Does not depend on specific particle masses or charges.
Lean usage
simp only [B_pow_Lepton_eq]formal statement (Lean)
90theorem B_pow_Lepton_eq : B_pow .Lepton = -22 := by
proof body
Term-mode proof.
91 simp only [B_pow, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, D]
92 norm_num
93