lepton_B
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical electron mass value.
- Does not address higher lepton generations or quark sectors.
- Does not incorporate electromagnetic coupling constants.
- Does not prove the equality B = -22; that is a separate theorem.
formal statement (Lean)
91def lepton_B : ℤ := -((ledger_bilateral_factor : ℤ) * (MassTopology.E_passive : ℤ))
proof body
Definition body.
92
93/-- PROOF: lepton_B evaluates to -22. -/