Q_tilde_up
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.