step_gen1
plain-language theorem explainer
The integer eleven supplies the E_pass value in the cyclic generation torsion chain for fermion mass rungs. Mass ladder constructors cite it when accumulating first-generation shifts for leptons and up quarks under the sector-dependent model. The declaration is a direct constant assignment with no computation or hypotheses.
Claim. The first-generation step constant equals $11$.
background
The module defines sector-dependent generation torsion via the cyclic chain V+F-C=13, E_pass=11, F=6, V=8. These four values partition N_3=55 and assign two consecutive steps to each fermion sector: up quarks use the first pair, leptons the middle pair, down quarks the last pair. The legacy universal convention {0,11,17} is retained only for backward compatibility with leptons.
proof idea
Direct constant definition assigning the integer eleven.
why it matters
This constant populates tau_charged, tau_neutrino, and tau_sdgt, which accumulate generation torsion for rung computations. It corresponds to the E_pass=11 entry in the cyclic chain, supporting the canonical sector-dependent torsion model over the legacy universal version. It closes the base layer for the mass formula yardstick times phi to the rung power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.