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

Q_tilde_up

show as:
view Lean formalization →

The definition assigns the integer 4 to the up-sector integerized charge, obtained as the absolute value of six times the up-quark fractional charge two-thirds. Researchers deriving forced generation orderings from sector-dependent torsion cite this constant to quantify the asymmetry that excludes equal-span configurations. The assignment is a direct numerical definition with no lemmas or reductions applied.

claimThe up-sector integerized charge is defined by $Q_{tilde up} := 4$, encoding the absolute value $|6 times (2/3)|$.

background

The SDGT Forcing module shows that sector-dependent generation torsion is forced by three constraints: a partition sum of three overlapping consecutive-pair spans equaling 55, lepton uniqueness fixing the middle pair at 11 and 6, and charge asymmetry between up and down sectors. Q_tilde_up supplies the numerical value 4 for the up sector, with the down-sector counterpart equal to 2. The module imports AlphaDerivation and SectorDependentTorsion to anchor the step values in prior Q3 cell counts.

proof idea

The declaration is a direct definition that assigns the natural number 4, with the attached comment tracing its origin to the scaled up-quark charge.

why it matters in Recognition Science

This constant supplies the input for the charge asymmetry argument inside the SDGT Forcing Theorem, which selects the unique ordering 13, 11, 6, 8. It is invoked by the downstream theorems charges_distinct and larger_charge_larger_span to establish that the larger charge magnitude receives the larger span. The result closes the exclusion of ordering B and leaves open the first-principles derivation of the four step values from the Recognition functional equation.

scope and limits

formal statement (Lean)

 121def Q_tilde_up : ℕ := 4      -- |6 × 2/3| = 4

used by (2)

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