lepton_yardstick_eq_explicit
plain-language theorem explainer
The theorem equates the lepton yardstick defined from sector parameters to its explicit form after substitution of derived constants. Physicists deriving first-generation lepton masses in Recognition Science would cite it to confirm the scale factor before phi-ladder application. The proof is a direct simplification that unfolds the definitions and replaces B, E_coh, and R0 with their evaluated values.
Claim. The lepton yardstick defined by $Y = 2^B E_0 phi^{R_0}$ equals the explicit expression obtained by substituting the derived values $B = -22$, $E_0 = phi^{-5}$, and $R_0 = 62$.
background
In the T9 Electron Mass Definitions module the lepton yardstick is the sector scale factor for the electron. It is constructed as the product of the bilateral ledger factor $2^B$, the coherence energy $E_0$, and the phi-powered rung offset $phi^{R_0}$. The module derives these inputs from three-dimensional cube geometry: passive edge count fixes $B = -22$, wallpaper groups and octave structure fix $R_0 = 62$, and the coherence exponent fixes $E_0 = phi^{-5}$.
proof idea
The term proof applies simp only to the definitions of lepton_yardstick and lepton_yardstick_explicit together with the equality theorems lepton_B_eq, lepton_R0_eq, and E_coh_eq. These substitutions reduce both sides to the identical explicit expression $2^{-22} phi^{-5} phi^{62}$, after which reflexivity closes the goal.
why it matters
The result verifies internal consistency of the lepton yardstick inside the electron mass derivation chain. It supplies the verified scale for the structural mass formula $m_struct = Y phi^{r-8}$ and anchors the T9 steps that link D = 3, the eleven passive edges, and the eight-tick octave to the phi-ladder. No downstream theorems are listed, indicating this equality is a terminal consistency check within the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.