ell_baseline
plain-language theorem explainer
The baseline offset definition assigns integer values to each fermion sector for initializing mass rung calculations: 2 for leptons, 0 for neutrinos, 4 for up and down quarks, and 1 for electroweak. Mass ladder modelers in Recognition Science cite it when constructing generation-dependent spectra from the phi-ladder. The definition is realized by exhaustive pattern matching on the Sector cases.
Claim. Define the baseline length function by cases: 2 on the lepton sector, 0 on neutrinos, 4 on up quarks, 4 on down quarks, and 1 on the electroweak sector.
background
The module introduces generation step constants via sector-dependent generation torsion. Each fermion sector draws two consecutive values from the cyclic chain V+F-C=13, E_pass=11, F=6, V=8 that partition N_3=55. The legacy convention retained here applies universal torsion {0,11,17} for all charged fermions and is accurate only for leptons; quarks require the sector-dependent variant.
proof idea
The definition is implemented as a direct case analysis on the input sector value, returning the corresponding fixed integer in each branch.
why it matters
This baseline is invoked inside compute_rung and compute_rung_sdgt to initialize the rung before adding the generation step. It supplies the legacy rung constructor step in the mass motif. In the Recognition framework it anchors the yardstick * phi^(rung - 8 + gap(Z)) mass formula on the phi-ladder for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.