IndisputableMonolith.Physics.ElectronMass
Barrel module for the T9 electron-mass sector: it re-exports the core ladder definitions and the necessity argument that the electron mass formula is forced from ledger quantization and cube geometry. Downstream lepton and quark work imports here rather than the split submodules. The page also records hypothesis-driven numeric bounds on the electron residue once a structural mass window and the observed electron mass are fixed.
claimModule collecting the T9 electron-mass package: definitions of the electron rung and residue on the $\varphi$-ladder, the necessity claim that the electron mass formula is forced from ledger quantization (T8) and geometric sector constants, and hypothesis-driven bounds $r_e \in (-20.7063,-20.7058)$ when the structural mass lies in $(10856,10858)$ and $m_{\mathrm{obs}}=0.510998950$.
background
Recognition Science places particle masses on a $\varphi$-ladder whose yardstick and rung offsets are fixed by earlier forcing steps (T5–T8). The electron is the reference charged lepton at a low integer rung; its mass is written as yardstick times $\varphi$ to a power involving rung, an eight-tick shift, and a gap term in atomic number.
ElectronMass.Defs isolates the T9 definitions (rung, residue, structural mass, sector constants) so that import cycles stay broken. Those lepton-sector constants are not free parameters: the Defs module states they come from cube geometry along the first-principles chain into sector constants.
ElectronMass.Necessity then argues that the electron mass formula itself is forced once T8 ledger quantization and those geometric constants are in place. The module-level note records a concrete numeric window: with structural mass in $(10856,10858)$ and $m_{\mathrm{obs}}=0.510998950$, the electron residue is forced into $(-20.7063,-20.7058)$, presently under explicit hypotheses rather than a fully closed proof.
proof idea
This is an aggregation module, not a single theorem. It imports Mathlib plus the two split submodules Defs and Necessity, and surfaces sibling objects such as residue bounds, gap-minus-shift bounds, and the electron-mass ledger hypothesis. Argumentative content lives in Necessity (forcing of the mass formula from T8 and geometry) and in the hypothesis-tagged numeric bound lemmas; the barrel itself only re-exports that structure for downstream physics modules.
why it matters in Recognition Science
T9 is the charged-lepton anchor of the RS mass ladder: once the electron residue and mass formula are fixed, heavier sectors are read as rung offsets from that reference. NeutrinoSector (T14) imports this module to place neutrinos on the deep ladder far below the electron rung $R_e=2$. QuarkMasses (T12) imports it when building the quarter-ladder quark spectrum against PDG targets.
In the broader chain, the necessity half ties electron mass back to T8 (ledger quantization) and the geometric constants that descend from the eight-tick octave and $D=3$. The residue window is still hypothesis-driven, so this module is also the natural place where closing those numeric hypotheses would harden the parameter-free core before neutrino and quark work cite it.
scope and limits
- Does not itself prove the electron mass formula; necessity lives in the imported Necessity submodule.
- Does not discharge the hypotheses behind the numeric electron-residue window.
- Does not derive neutrino or quark masses; those modules only import this barrel.
- Does not claim a parameter-free closed value of alpha or the full PDG lepton spectrum.