predicted_electron_mass
plain-language theorem explainer
predicted_electron_mass encodes the T9 formula for the electron mass in RS units as the product of structural mass and a phi correction from the gap at 1332. Researchers deriving particle masses from the phi-ladder cite this expression. The definition is a direct algebraic combination of the structural mass term with the gap adjustment.
Claim. $m_e = m_{struct} · ϕ^{g(1332) - s}$, where $m_{struct}$ is the electron structural mass from the phi-ladder, $g$ is the gap function, and $s$ is the refined shift.
background
The T9 module isolates definitions for the electron mass derivation to break import cycles. Structural mass is the yardstick scaled by phi to the adjusted rung power; the gap function is the product of closure and Fibonacci factors. Upstream, Gap45.Derivation establishes that the gap equals 45 by its main theorem, while AnchorPolicy supplies sector-specific gap computations and Mass is simply the reals.
proof idea
This is a one-line definition that multiplies the sibling electron_structural_mass by phi raised to the power of (gap 1332 minus refined_shift). It directly applies the gap definition from Gap45.Derivation and the structural mass expression without additional lemmas or reductions.
why it matters
This supplies the core expression for the T9 Electron Mass Formula, which the module's main theorems use to show the structural mass is geometrically forced. It implements the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder and connects to the forcing chain through T8. It leaves open the precise numerical match to the observed mass after residue correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.