pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Masses.RungConstructor.Basic

show as:
view Lean formalization →

This module supplies the canonical species and sector definitions that anchor the mass framework. Particle physicists building phi-ladder spectra for the twelve Standard Model fermions cite it to fix the basic objects before rung construction begins. It consists entirely of four definitions (Species, Sector, sectorOf, tildeQ) with no theorems or proofs.

claimThe module introduces the canonical species set $S$ for the twelve fermions, the sector map $sectorOf: S → Sector$, and the charge function $tildeQ$, together with the auxiliary type $Sector$, as the entry point for mass construction on the phi-ladder.

background

The module sits inside the Masses domain and imports the RSBridge.Anchor module. That upstream module supplies the twelve Standard Model fermions (Fermion), the charge-indexed integer $Z_i = tildeQ^2 + tildeQ^4$ (with an extra +4 for quarks), the gap display function $F(Z) = ln(1 + Z/φ)/ln(φ)$, and the anchor-scale mass $massAtAnchor$. The present module then defines the canonical species and sectors that label these objects for rung construction.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into the downstream Motif module, which uses them to introduce Sector-Dependent Generation Torsion (SDGT) and the cyclic chain V+F-C=13 → E_pass=11 → F=6 → V=8. The module thereby supplies the basic species objects required by the Recognition Science mass formula that places each fermion on the phi-ladder via rung and gap(Z).

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)