up_rung_gen1
plain-language theorem explainer
The definition sets the baseline rung for the first up-quark generation to 4 via direct exponentiation. Mass ladder calculations and generation-ordering results cite this value as the starting point for up-sector rungs. The definition evaluates 2 raised to (3 minus 1) with no additional lemmas.
Claim. The baseline rung for the first up-quark generation is defined as $2^{3-1}$.
background
Sector-Dependent Generation Torsion defines generation rungs as integers placed on the phi-ladder for the mass formula yardstick times phi to the power (rung minus 8 plus gap). The module verifies that cell counts {13, 11, 6, 8} satisfy algebraic constraints including cyclic chains and partition of 2D^D + 1 = 55, with up quarks assigned the pair {13, 11} as a data-supported hypothesis. The exponent 3 in the definition ties to the derived D = 3 condition where W = 2V + 1 equals N0 only in three spatial dimensions.
proof idea
This is a direct definition that evaluates the natural-number exponentiation 2^(3-1) to obtain 4. No upstream lemmas are invoked.
why it matters
The value supplies the base case for the up-generation-ordering theorem that establishes 4 < 17 < 28 and for the equality check that confirms the rung equals 4. It anchors the up-sector mass ladder within the eight-tick octave structure of the forcing chain. The module records that the specific quark rung assignments remain hypotheses identified from data rather than forced from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.