step_up_gen1
Up-quark generation one receives the step value 13 in the sector-dependent generation torsion. This constant feeds cumulative torsion sums for up-type fermions when building mass rungs. Researchers constructing sector-specific ladders cite it to separate up-quark spans from lepton and down-quark spans. The value is introduced by direct assignment from the cube vertex plus face count minus one.
claimThe first-generation step for up quarks is defined as the integer 13, satisfying $V + F - C = 13$ where $V=8$ is the vertex count of the three-dimensional cube, $F=6$ is the face count, and $C=1$ is the correction term.
background
The module defines sector-dependent generation torsion (SDGT) via a cyclic chain of four constants: V+F-C=13, E_pass=11, F=6, V=8. Up quarks employ the consecutive pair summing to 24, leptons employ 11+6=17, and down quarks employ 6+8=14. These three spans partition the total $N_3 = 2D^D + 1 = 55$ for $D=3$ (see SectorDependentTorsion). V is the vertex count $2^D$ of the D-dimensional binary cube. F is the face count of the same cube. The construction replaces the legacy universal torsion retained only for backward compatibility with leptons.
proof idea
The declaration is a direct definition that assigns the integer 13. No lemmas are invoked and no tactics are used; the body is a literal constant encoding the arithmetic V + F - C.
why it matters in Recognition Science
The constant supplies the initial value for up quarks inside tau_sdgt, the canonical cumulative generation torsion function. It completes the SDGT model that distinguishes the three fermion sectors inside the mass rung constructor. The assignment aligns with the D=3 geometry of the cube and the eight-tick octave structure of the Recognition framework.
scope and limits
- Does not derive the integer 13 from J-cost or the phi fixed point.
- Does not compute any rung position on the phi-ladder.
- Does not apply to lepton or down-quark sectors.
- Does not contain the proof that the three spans sum to N_3=55.
Lean usage
match sector, gen with | .UpQuark, 1 => step_up_gen1 | _, _ => 0formal statement (Lean)
60def step_up_gen1 : ℤ := 13 -- V + F - C = 8 + 6 - 1