charges_distinct
The theorem asserts that the integerized up-sector charge differs from the down-sector charge. Researchers modeling sector-dependent generation torsion cite it to establish that up and down sectors must occupy unequal positions in the span ordering. The proof reduces to a direct numerical check of the constants 4 and 2 via the native decision procedure.
claim$4 ≠ 2$, where the integerized up-sector charge is defined as $|6 × 2/3| = 4$ and the down-sector charge as $|6 × 1/3| = 2$.
background
In the SDGT Forcing module the integerized charges appear as constant definitions: Q_tilde_up equals 4 from the absolute value of six times two-thirds, and Q_tilde_down equals 2 from six times one-third. These constants enter the charge-asymmetry argument that forces unequal end spans once the four step values {13, 11, 6, 8} have been fixed by the partition constraint summing to N₃ = 55 and the lepton-uniqueness condition selecting the middle pair {11, 6}. The module proves that the sector-dependent generation torsion is forced rather than merely compatible with the three listed constraints.
proof idea
The proof is a one-line wrapper that invokes native_decide on the inequality between the two constant definitions.
why it matters in Recognition Science
This declaration completes the charge-asymmetry step inside the SDGT Forcing Theorem, which selects the unique ordering (13, 11, 6, 8) once |Q̃_up| ≠ |Q̃_down| is granted. It thereby supports the claim that the assignment of sectors to the four steps is forced. The four step values themselves remain open for derivation from a single principle, as noted in the module documentation. The result aligns with the Recognition Science framework by using charge asymmetry to enforce distinct sectors within the eight-tick octave structure.
scope and limits
- Does not derive the integer charge values from a deeper principle.
- Does not compute the numerical span lengths 24 and 14.
- Does not address the origin of the step values {13, 11, 6, 8}.
- Does not extend the asymmetry argument to other particle families.
formal statement (Lean)
124theorem charges_distinct : Q_tilde_up ≠ Q_tilde_down := by native_decide
proof body
Term-mode proof.
125
126/-- The larger charge gets the larger span.
127 |Q̃_up| = 4 > |Q̃_down| = 2, so span_up = 24 > span_down = 14. -/