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