Pith. sign in
module module moderate

IndisputableMonolith.Physics.MassTopology

show as:
view Lean formalization →

Defines the mass-topology ledger quantities used across the lepton sector: total and passive edge counts, the cube-derived wallpaper weight W, ledger fractions, and the base plus radiative mass shifts. Electron-mass and lepton-generation modules import these as geometric inputs. The file is a definition layer assembling constants from the cubic ledger and alpha seed, not a theorem pack.

claimMass-topology primitives on the cubic ledger: total edge count $E_{\mathrm{total}}$, passive edge count $E_{\mathrm{passive}}$, wallpaper weight $W$, ledger fraction, base shift, second- and third-order corrections, radiative correction, and refined shift. These feed the $\varphi$-ladder mass formulas for leptons.

background

Recognition Science places particle masses on a $\varphi$-ladder whose rungs are fixed by ledger geometry in $D=3$ (forcing step T8). The cubic ledger supplies combinatorial edge counts; passive edges and face data assemble an endogenous wallpaper weight $W$, later compared to the crystallographic constant in the mass-path sufficiency route.

This module sits downstream of Constants, Alpha, and AlphaDerivation. The alpha construction supplies the seed $4\pi\cdot 11$ and $\varphi$-dressing from cube combinatorics; the exact infrared $\alpha^{-1}(0)$ remains an open boundary condition. Mass topology reuses that geometric vocabulary (edges, passive structure, fractions) to define the shift and correction terms that enter lepton mass formulas.

Named objects introduced here include $E_{\mathrm{total}}$, $E_{\mathrm{passive}}$, $W$, ledger fraction, base shift, order-2/3 corrections, radiative correction, and refined shift. Downstream electron-mass docs state that lepton sector constants are derived from cube geometry rather than fitted freely.

proof idea

This is a definition module, not a theorem pack. It assembles named real-valued (or natural) quantities from cube edge combinatorics and imported RS constants, then packages the base shift and radiative correction hierarchy used by the mass path. No forcing proof lives here; necessity and sufficiency arguments are deferred to importers such as ElectronMass.Necessity and WallpaperSufficiencyMassPath.

why it matters in Recognition Science

Parent consumers are ElectronMass.Defs and Necessity (T9 electron mass forced from T8 ledger quantization and geometric constants), LeptonGenerations.Defs (T10), LeptonCoefficientPerturbation (small-strain $J$-cost expansion at $\varepsilon=\alpha$), and WallpaperSufficiencyMassPath. The last formalizes that canonical mass-path formulas are unchanged when the imported crystallographic wallpaper_groups is replaced by the endogenous $W_{\mathrm{from_cube}}=E_{\mathrm{passive}}+F$ at $D=3$.

Without a single place for $E_{\mathrm{total}}$, $E_{\mathrm{passive}}$, $W$, and the shift/correction ladder, the lepton mass chain would re-encode cube geometry in every file and break import-cycle discipline. The module therefore anchors the geometric side of the mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) before necessity theorems claim the electron mass is forced.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)