pith. machine review for the scientific record. sign in
def definition def or abbrev high

step_up_gen2

show as:
view Lean formalization →

This definition assigns the integer 11 to the E_pass generation step in the sector-dependent torsion chain for up-type quarks. Mass spectrum constructors on the recognition manifold would cite it when placing the second rung for up quarks. The assignment follows directly from the difference between the D-cube edge count and the active edge count per tick.

claimThe second-generation up-quark step constant equals the integer 11, obtained as the difference between the edge count of the three-dimensional cube and the active edge count per fundamental tick.

background

The module introduces sector-dependent generation torsion (SDGT) for fermion sectors. The four step values form a cyclic chain V+F-C=13 to E_pass=11 to F=6 to V=8, with each sector taking two consecutive values that partition N_3 = 2D^D +1 =55. Upstream, the edge count is given by E(D) = D * 2^(D-1) and the active edge count per tick is A=1.

proof idea

The definition is a direct constant assignment. The inline comment derives the value as the difference E minus A using the upstream edge count and anchor definitions.

why it matters in Recognition Science

It supplies the E_pass slot to tau_sdgt, the canonical cumulative generation torsion for all fermion sectors. This supports rung construction for masses on the phi-ladder and aligns with the eight-tick octave in the unified forcing chain.

scope and limits

formal statement (Lean)

  61def step_up_gen2 : ℤ := 11   -- E_pass = E - A = 12 - 1

proof body

Definition body.

  62
  63/-- Down-quark generation steps: {F=6, V=8}. HYPOTHESIS. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.