ledger_bilateral_factor
plain-language theorem explainer
The bilateral ledger factor is the natural number 2, encoding the doubling from reciprocal pairing symmetry in the recognition ledger. Researchers deriving lepton sector constants from D=3 cube geometry cite this factor to fix the binary exponent at B = -22. The definition is a direct constant assignment with no computation or reduction steps.
Claim. The bilateral factor is the natural number $2$, arising from reciprocal pairing (Tr4) that doubles the passive edge count in the ledger.
background
In the T9 electron mass module, lepton sector constants are derived from cube geometry at spatial dimension D=3. Passive field edges equal 11, computed as total cube edges (12) minus one active edge per tick. The bilateral factor of 2 scales the binary gauge exponent as B = -(2 * 11) = -22, with the doubling traced to ledger reciprocal pairing. Upstream structures on ledger factorization and phi-forcing supply the J-cost convexity and 8-tick local dynamics that justify the pairing symmetry. Spectral emergence confirms the resulting 24 chiral fermion flavors from D * 2^D.
proof idea
This is a one-line definition that directly assigns the constant 2 to represent the bilateral doubling factor from reciprocal pairing.
why it matters
This definition supplies the bilateral factor to lepton_B, lepton_B_eq, and lepton_sector_is_derived, establishing that all lepton sector constants are forced by D=3 cube geometry and wallpaper groups without free parameters. It closes the derivation chain from T8 spatial dimensions through the passive edge count to the electron baseline rung. The parent theorems confirm the sector is parameter-free and derived from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.