pith. sign in
module module moderate

IndisputableMonolith.Physics.MassTopology

show as:
view Lean formalization →

The MassTopology module supplies the total edge count of the cubic ledger Q3 together with derived ledger fractions and energy terms. Downstream lepton mass modules cite it to obtain the geometric inputs required by T9 and T10. It is a pure definition module whose contents are fixed once the Q3 vertex structure is given.

claimLet $Q_3$ be the cubic ledger. The module defines the total edge count $|E(Q_3)|$ and the associated ledger quantities $E_{ m total}$, $E_{ m passive}$, $W$, ledger_fraction, base_shift, and the first three orders of radiative correction.

background

Upstream, Constants.AlphaDerivation derives $4\pi$ from the vertex deficits of $Q_3$ via a Gauss-Bonnet identity on the cubic lattice. The present module sits inside the same geometric setting and enumerates the edges of that lattice to produce the numerical coefficients that later enter mass formulas. Sibling definitions include E_total (sum of active edge energies), ledger_fraction (edge occupancy ratio), and correction_order_n (higher-order adjustments to the base shift).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The edge count and ledger fractions defined here are imported directly by ElectronMass.Defs and LeptonGenerations.Defs (both T9/T10) and by their RRF counterparts. Those modules state that lepton masses are forced from T8 ledger quantization once the Q3 geometry is fixed; the present module closes the geometric step that supplies the required constants.

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)