lepton_yardstick
plain-language theorem explainer
The lepton yardstick supplies the base scale Y for the lepton sector by multiplying the binary gauge 2^B, the coherent energy E_coh, and the geometric offset phi^R0. Researchers deriving electron masses from Recognition Science geometry cite this as the anchor for structural mass on the phi-ladder. The definition is a direct product of three constants obtained from cube geometry and wallpaper tiling.
Claim. The lepton yardstick is the real number $Y = 2^{B} E_coh phi^{R_0}$, where $B = -22$ is the lepton sector binary gauge, $E_coh = phi^{-5}$ is the coherent energy scale, and $R_0 = 62$ is the lepton sector geometric origin.
background
The T9 module isolates core definitions for the electron mass to break import cycles. Cube geometry in D=3 gives 12 edges total, one active per tick, and 11 passive edges; the binary gauge B is then minus twice that passive count, yielding -22. The offset R0 equals four times the 17 wallpaper groups minus the octave adjustment from baseline rung 2, producing 62. The coherent energy is defined as phi to the power of minus the coherence exponent, which evaluates to phi^{-5}.
proof idea
This is a definition that directly multiplies the three sibling constants: the binary gauge lepton_B, the coherent energy E_coh, and the geometric offset lepton_R0. No lemmas or tactics are applied; the body is the explicit product expression.
why it matters
This definition anchors the structural mass m_struct = lepton_yardstick times phi to the power of (electron_rung minus 8), which downstream results reduce to 2^{-22} phi^{51}. It realizes the T9 step that forces lepton constants from D=3 cube geometry, passive edge count 11, and wallpaper groups 17. The parent theorems electron_structural_mass and electron_structural_mass_forced use it to confirm geometric forcing of the mass scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.