compute_rung
plain-language theorem explainer
The legacy rung constructor assigns integer rungs to particle species by adding a generation-dependent torsion to a sector baseline for fermions and returning the electroweak baseline for bosons. Researchers constructing mass spectra in the Recognition Science framework cite this definition when verifying lepton and neutrino rungs against the universal torsion set. The implementation uses direct pattern matching on the species constructor to select the appropriate baseline and tau function.
Claim. The rung assignment function maps each particle species $s$ to an integer $r(s) = b + t$, where $b$ is the sector baseline and $t$ is the generation torsion. For a fermion in sector $s$ with generation index $g$, $b$ is the baseline of $s$ and $t$ equals the charged torsion or neutrino torsion according to sector. For the bosons $W$, $Z$, $H$ the value is the electroweak baseline.
background
In the Recognition Science mass construction, rungs label positions on the phi-ladder that enter the mass formula yardstick times phi to the power of (rung minus 8 plus gap). The module distinguishes the legacy universal torsion set {0, 11, 17} for charged fermions from the sector-dependent generation torsion (SDGT) whose cyclic values are V+F-C=13, E_pass=11, F=6, V=8. The supplied module documentation states that the legacy convention is retained only for backward compatibility and is accurate solely for leptons and neutrinos.
proof idea
The definition is realized by exhaustive pattern matching on the Species inductive type. For fermion cases it extracts the sector and generation index then branches on whether the sector is Neutrino to add the corresponding tau torsion to the baseline; boson cases return the electroweak baseline directly. No lemmas are invoked; the computation is purely structural.
why it matters
This definition supplies the rung values consumed by the matching theorems in RungConstructor.Proofs, such as match_boson_H which verifies the assignment for H and the down-quark matches. It fills the legacy rung constructor step in the mass formula pipeline, connecting to the eight-tick octave and D=3 dimensions in the forcing chain. The module documentation notes that for quarks the SDGT variant should be used instead, leaving an open refinement for full quark compatibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.