lepton_B_eq
plain-language theorem explainer
The lepton sector binary exponent evaluates to -22 from the passive field edge count of 11 in three-dimensional cube geometry. Researchers computing the electron structural mass on the phi-ladder cite this equality to fix the binary scaling factor before applying the rung offset. The proof is a term-mode simplification that unfolds the relevant edge and ledger definitions then normalizes the resulting arithmetic.
Claim. The lepton sector binary exponent satisfies $B_Lepton = -22$.
background
The module derives lepton sector constants from cube geometry with D=3. Cube edges are defined by cube_edges(d) := d * 2^(d-1), so cube_edges(3) = 12. Active edges per tick equal 1 by the atomic tick rule, and passive field edges are then cube_edges(d) - 1 = 11. The binary exponent is constructed as B_pow(Lepton) = -(2 * E_passive) where E_passive is the passive edge count of 11, yielding -22. The local setting states that these constants are forced by D=3, the passive edge count, wallpaper groups equal to 17, and the eight-tick octave structure.
proof idea
The proof is a term-mode one-line wrapper. It applies simp only to unfold lepton_B, ledger_bilateral_factor, MassTopology.E_passive, passive_field_edges, cube_edges, and active_edges_per_tick, then invokes norm_num to evaluate the arithmetic to -22.
why it matters
This equality supplies the binary exponent required by the downstream theorem electron_structural_mass_forced, which reduces the structural mass to 2^(-22) * phi^51. It closes the derivation step from cube geometry and the eight-tick octave to the lepton yardstick on the phi-ladder. The result is cited in lepton_yardstick_eq_explicit to eliminate the B factor during explicit yardstick computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.