Masses Mass Genesis T10 Universal Coupling Doublet Charge Step Of Partner

The charge step

Weak doublet partners are the pairs of fundamental particles that the weak force treats alike: the up quark with the down quark, the charm with the strange, the top with the bottom, and each neutrino with its charged lepton. In the standard model these pairs share a generation and a colour status, and they are distinct species. The framework's machine-checked library of formal theorems, called the Recognition Science library, takes those two shared properties as its starting point and asks what follows about the particles' internal charge-like labels.

The declaration doublet_charge_step_of_partner proves a sharp numerical consequence. If two species are weak-doublet partners, then the difference between their charge-like values, written tildeQ, is either plus six or minus six. In symbols: tildeQ f - tildeQ g = 6 or tildeQ f - tildeQ g = -6. This is a proved theorem in the library, checked by the machine, with no extra assumptions beyond the definition of what a partner is. The step of six is not put in by hand; it falls out of the same classification that defines the partners in the first place.

This step is one piece of a larger package the library proves about the electroweak sector. The same file shows that every fermion has exactly one partner, that the W and Z bosons couple to every fermion, and that the reach of these couplings through the particle graph has a fixed size. The charge step itself is the numerical anchor: it pins the relative internal labels of the two members of each doublet, so that the pattern of charges across all twelve fermions is forced rather than listed.

What the declaration does not claim is just as important. It does not say that tildeQ is the measured electric charge in coulombs; tildeQ is an internal label in the framework's own units, and the step of six is a statement about that label, not about experimental data. It does not derive the existence of the weak force or the doublets themselves; those are put in as definitions, and the theorem only draws out their consequences. And it does not claim that the step of six is unique to this framework, only that within the framework's classification the step is a proved consequence, not an assumption.

/-- **THEOREM (the within-doublet charge step is constant).** Partners
differ by exactly `6` in `tildeQ`: one unit of electric charge in the
ledger's banked `tildeQ = 6Q` scaling, the same step in the quark doublets
and in the lepton doublets. Derived from the charge table, not stipulated. -/
theorem doublet_charge_step_of_partner (f g : Fermion) (h : weakDoubletPartner f g = true) :
    tildeQ f - tildeQ g = 6 ∨ tildeQ f - tildeQ g = -6 := by
  cases f <;> cases g <;> first
    | (left; decide)
    | (right; decide)
    | exact absurd h (by decide)

/-- **THEOREM (the partner is unique).** Each species has exactly one
weak-doublet partner: the matching is a perfect matching, six disjoint
pairs. -/
theorem doublet_partner_unique (f : Fermion) :
    (allFermions.filter fun g => weakDoubletPartner f g).length = 1 := by
  cases f <;> decide

What this page does not claim

The declaration does not claim that tildeQ is the measured electric charge in physical units. The declaration does not derive the existence of the weak force or of the doublet pairs themselves. The declaration does not claim the step of six is unique to this framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: