lepton_B
plain-language theorem explainer
The lepton sector binary gauge is assigned the integer value -22. Researchers deriving the electron mass from Recognition Science geometry cite this gauge when constructing the sector yardstick scale. The definition is a direct constant assignment that encodes the bilateral factor times the passive edge count from the underlying cube topology.
Claim. The lepton sector binary gauge $B$ is defined as $B = -22$.
background
Module T9 isolates the electron mass definitions to break import cycles in the Recognition Science development. The lepton sector binary gauge $B$ is set to -22 in this definition. Upstream results include the Lepton inductive type enumerating electron, muon, tau and neutrinos from CubeFaceUniversality, and a restricted version for charged leptons in AnomalousMoments. The numerical value follows from $B = -(2 × 11)$, with the factor 2 from reciprocal pairing and 11 from the passive field edges in MassTopology.
proof idea
This declaration is a direct definition that assigns -22. It is referenced in the proof of the equality theorem, which uses simplification over the bilateral factor and passive edges followed by numerical normalization to confirm the value.
why it matters
This gauge enters the yardstick $Y = 2^B E_{coh} φ^{R0}$ and thereby the structural mass expression $2^{-22} φ^{51}$ in the forced mass theorem. It supports the derivation that the entire lepton sector is fixed by cube geometry, as stated in the sector derivation theorem. The constant closes a step in the T9 chain and connects to the phi-ladder scaling with rung adjustments in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.