lepton_yardstick
plain-language theorem explainer
lepton_yardstick defines the lepton sector yardstick Y as the product of the binary gauge power 2 to the power of lepton_B, the coherent energy E_coh equal to phi to the minus five, and phi raised to the geometric origin lepton_R0. Researchers assembling the electron mass on the phi-ladder in Recognition Science cite this definition when forming the structural mass. It is a direct algebraic combination of the precomputed parameters B equals negative twenty-two and R0 equals sixty-two.
Claim. $Y = 2^{B} E_coh phi^{R_0}$, where $B$ is the lepton binary gauge and $R_0$ is the geometric origin rung.
background
The T9 Electron Mass Definitions module isolates core parameters for the electron mass derivation to break import cycles. E_coh is defined as the coherent energy scale phi to the minus five. lepton_B evaluates to negative twenty-two from the bilateral factor times the passive mass topology. lepton_R0 evaluates to sixty-two from four fermion sectors, seventeen wallpaper groups, and the octave adjustment from the baseline rung of two.
proof idea
This is a one-line definition that multiplies the binary power using lepton_B, the coherent scale E_coh, and the phi exponent lepton_R0. It relies directly on the sibling definitions of lepton_B, lepton_R0, and E_coh.
why it matters
This yardstick supplies the scale factor that enters the downstream structural mass definition m_struct equals lepton_yardstick times phi to the power of electron_rung minus eight. It supports the forced theorem electron_structural_mass_forced, which reduces the full expression to two to the negative twenty-two times phi to the fifty-one. In the Recognition Science framework it implements the mass formula yardstick times phi to the power of rung minus eight on the phi-ladder, with the eight-tick octave implicit in the rung calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.