step_down_gen2
plain-language theorem explainer
step_down_gen2 supplies the constant 8 for the second down-generation step in the SDGT chain. Mass-ladder constructions for down quarks cite this value when accumulating torsion from the cyclic cell counts V+F-C=13, E_pass=11, F=6, V=8. The definition is a direct assignment of 2^D evaluated at the spatial dimension D=3.
Claim. The second down-generation step constant equals $8$, which is $2^D$ for spatial dimension $D=3$.
background
The Motif module defines sector-dependent generation torsion constants that form the cyclic chain V+F-C=13, E_pass=11, F=6, V=8. Each fermion sector consumes two consecutive values: down quarks use {F=6, V=8} for a total of 14. These constants feed the cumulative torsion tau_sdgt that partitions N_3=55 and supplies rung increments for the mass formula.
proof idea
One-line definition that assigns the integer 8, obtained by evaluating the vertex count V(D) := 2^D at D=3 from the spatial dimension result.
why it matters
The constant is consumed by tau_sdgt to produce sector-dependent cumulative generation torsion for down quarks. It instantiates the D=3 outcome of the unified forcing chain (T8) and closes the cyclic step chain that partitions N_3. Downstream mass constructions rely on this value to set the correct torsion increments before phi-ladder scaling is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.