electron_structural_mass
plain-language theorem explainer
The structural mass of the electron is the lepton yardstick multiplied by phi to the power of the electron rung minus eight. Researchers deriving particle masses in the Recognition Science framework cite this definition when assembling the predicted electron mass or evaluating alphaG scores. It is realized as a direct one-line expression that substitutes the rung value of two and the yardstick formula involving E_coh.
Claim. The structural mass $m_{struct}$ is defined by $m_{struct} = Y · ϕ^{r-8}$, where $Y = 2^B · E_{coh} · ϕ^{R_0}$ is the lepton yardstick and $r = 2$ is the electron rung.
background
The T9 Electron Mass Definitions module isolates core quantities for the electron mass derivation to break import cycles. The lepton yardstick is the sector scale factor $2^B · E_{coh} · ϕ^{R_0}$. The electron rung is fixed at 2, marking the baseline for the first-generation lepton on the phi-ladder. This structural mass implements the general mass formula yardstick times phi to the power of rung minus 8. The upstream electron_rung definition states that the electron rung equals 2 as the baseline for generation 1 leptons, while lepton_yardstick supplies the explicit scale using the coherence energy.
proof idea
This is a one-line definition that multiplies the lepton yardstick by phi raised to the power of the electron rung minus 8. It applies the sibling definitions of lepton_yardstick and electron_rung directly with no additional lemmas.
why it matters
This definition supplies the structural mass component used by the alphaG prediction theorems in the AlphaGScoreCard module, including alphaG_pred_eq and row_alphaG_pred_eq. It fills the T9 step in the electron mass derivation, realizing the phi-ladder mass formula yardstick · ϕ^(rung-8) and linking to the eight-tick octave through rung indexing. It supports closure of native-unit predictions for constants such as alphaG.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.