step_gen2_charged
plain-language theorem explainer
The integer 6 is fixed as the second-generation step constant for charged leptons in the sector-dependent torsion chain. It enters the cumulative sums that set rung positions on the phi-ladder for mass assignments. The definition is a direct literal with no computation or external lemmas.
Claim. The second-generation step constant for charged fermions is the integer $6$.
background
The Motif module encodes Sector-Dependent Generation Torsion (SDGT) via a cyclic chain of cube-cell counts: V+F-C=13, E_pass=11, F=6, V=8. Each fermion sector consumes two consecutive values from this cycle, and the three resulting spans partition N_3 = 2D^D + 1 = 55. The value 6 is the F entry and supplies the second increment for leptons under the legacy convention.
proof idea
Direct definition as the integer literal 6; no tactics or upstream lemmas are invoked.
why it matters
Supplies the F=6 entry required by the SDGT chain that partitions N_3 and feeds the phi-ladder mass formula. It is used by tau_charged (legacy lepton torsion) and tau_sdgt (canonical lepton case for gen >= 2). The constant therefore participates in the rung construction that ultimately yields the observed fermion mass spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.