lepton_B
plain-language theorem explainer
The lepton sector binary gauge B is defined as the negative product of the ledger bilateral factor (2, from reciprocal pairing) and the passive edge count E_passive (11, from 3-cube geometry). Researchers deriving the electron yardstick or structural mass in Recognition Science cite this when scaling the phi-ladder from T9 constants. The definition is a direct algebraic assignment that evaluates immediately to -22 without further reduction.
Claim. The lepton sector binary gauge is defined by $B := -(2 × 11)$, where the factor 2 is the ledger bilateral factor from reciprocal pairing and 11 is the passive field edge count in three-dimensional cube geometry.
background
In the T9 Electron Mass Definitions module the lepton sector constants are derived from cube geometry at D = 3. The passive edge count E_passive equals cube_edges(3) minus one active edge per tick, giving 11. The ledger bilateral factor equals 2, reflecting the doubling symmetry of reciprocal pairing (Tr4). This definition sits between the upstream constants E_passive (from MassTopology and Masses.Anchor) and the downstream yardstick and structural-mass expressions.
proof idea
This is a direct definition that multiplies the bilateral factor by the passive edge count and negates the product. It depends only on the sibling definition ledger_bilateral_factor and the imported MassTopology.E_passive; both are constant values (2 and 11) so the expression evaluates by substitution alone.
why it matters
This supplies the binary exponent B = -22 required by the lepton yardstick and the structural mass formula. It is used by lepton_B_eq, lepton_sector_is_derived, and lepton_yardstick, and by the RRF mirror theorems that compute electron_structural_mass = 2^(-22) * phi^51. The definition realizes the T9 step that forces sector constants from D = 3, the eight-tick octave, and wallpaper groups, confirming the lepton sector is parameter-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.