rung_sdgt
plain-language theorem explainer
The rung_sdgt definition supplies the integer rung index on the phi-ladder for a particle given its Anchor sector and string name. Mass calculators in Recognition Science invoke it to build the exponent in the discrete mass formula yardstick times phi to the power of rung minus eight plus gap. The implementation is a direct pattern match on the four cases of the Anchor.Sector inductive type, delegating to sector-specific tables.
Claim. For sector $s$ and particle identifier $n$, the SDGT rung selector $r_{sdgt}(s,n)$ returns the integer ladder position given by the lepton table when $s$ is Lepton, the up-quark table when $s$ is UpQuark, the down-quark table when $s$ is DownQuark, and the boson table when $s$ is Electroweak.
background
Recognition Science assigns particle masses to discrete positions on the phi-ladder via the formula yardstick times phi raised to (rung minus 8 plus gap(Z) plus shift). The Anchor.Sector inductive type partitions particles into Lepton, UpQuark, DownQuark, and Electroweak cases. Upstream structures include the Lepton inductive from CubeFaceUniversality and the of structure from NucleosynthesisTiers that organizes nuclear densities on phi-tiers; cost definitions from ObserverForcing and MultiplicativeRecognizerL4 supply the underlying J-cost for recognition events.
proof idea
The definition is a direct pattern match on the sector parameter. The Lepton case calls Integers.r_lepton on the name; the UpQuark case delegates to rung_sdgt_up; the DownQuark case delegates to rung_sdgt_down; and the Electroweak case calls Integers.r_boson. No lemmas are applied; the body is a one-line wrapper that performs case analysis on the inductive sector type.
why it matters
This selector supplies the rung argument to predict_mass_sdgt, which assembles the full mass prediction m equals yardstick times phi to the power of (r_sdgt minus 8 plus gap plus cross-sector shift). It fills the discrete rung lookup step inside the AnchorPolicy module and supports the phi-ladder mass formula that follows from the self-similar fixed point T6 and the eight-tick octave T7. The cross-sector shift term encodes the edge-layer cost in the cube partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.