Encyclopedia Masses Masses Mass Genesis T10 Universal Coupling Universal Coupling Package

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Universal Coupling Universal Coupling Package

A single theorem in the Recognition Science library says every fermion couples to the weak bosons, and it derives that fact from a ledger of particle identities.

Verify this page

The universal coupling package

In particle physics, the weak force is universal: every known fermion, the family of matter particles that includes quarks and leptons, participates in weak interactions. The Recognition Science framework's ledger, a discrete record of recognition events, contains a theorem called universal_coupling_package that establishes this universality as a formal consequence of the framework's own classification of particles. The theorem states, in machine-checked form, that every fermion in the framework's list couples to both the W and Z bosons, the carriers of the weak force.

The framework does not import this universality from conventional physics. Instead, it derives the coupling pattern from two banked predicates: a particle's generation and its colour status. Two species are weak-doublet partners if they share a generation and a colour status and are distinct. The theorem doublet_partner_unique proves that every fermion has exactly one such partner. From this pairing, the framework defines a weak charge: a particle gets charge 1 if its partner has a higher tilde-charge, -1 if lower, and 0 otherwise. The theorem weakCharge_sm_pattern then shows the resulting charges match the Standard Model pattern: up-type quarks and neutrinos have charge 1, down-type quarks and charged leptons have charge -1.

The package's central result is that this derived coupling is universal. The theorem derived_w_universal proves every fermion couples to the W boson, and derived_z_universal proves the same for the Z boson. The framework also proves that its derived coupling functions are exactly equal to the declared gauge carrier couplings, so the derived pattern is not a separate model but the same object. The package further establishes structural facts: the W and Z channels each have reach 2, meaning they connect two distinct sectors, and cell reach 3, meaning three cells of the ledger are involved. It also proves the electroweak yardstick relation, which ties the electroweak anchor radius to these reach numbers.

What the package does not claim is equally important. It does not claim to derive the values of particle masses, the weak mixing angle, or any coupling strength constant. The universality is a statement about which particles couple, not how strongly. The framework's proof that every fermion couples to the W and Z bosons is a structural result about its classification; it does not explain why the weak force has the particular strength it does. The theorem also does not claim that the framework's particle list is complete or that it matches the observed particle spectrum beyond the twelve fermions it enumerates. Those are empirical questions the framework does not address in this package.

THEOREM universal_coupling_package · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
universal_coupling_package · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:338 
/-- **THE C15 PACKAGE.** One conjunction:

1. both derived couplings are universal (the premise, now a theorem);
2. the derived couplings coincide with the C13 declarations on every
   species (the declarations were forced);
3. the matching is perfect and unique, and colour status is the forced
   matching predicate;
4. the within-doublet charge step is constantly one unit of charge;
5. the reaches follow from the derived structure (channel `2`, cell `3`);
6. the yardstick restates premise-free (`55 = 3W + 4`);
7. the neutrino leg is forced;
8. the falsifier: decoupling is exactly partnerlessness. -/
theorem universal_coupling_package :
    (∀ f : Fermion, derivedWCouples f = true)
    ∧ (∀ f : Fermion, derivedZCouples f = true)
    ∧ (∀ f : Fermion, GaugeCarrier.couples .wBoson f = derivedWCouples f)
    ∧ (∀ f : Fermion, GaugeCarrier.couples .zBoson f = derivedZCouples f)
    ∧ (∀ f : Fermion, (allFermions.filter fun g => weakDoubletPartner f g).length = 1)
    ∧ ((allFermions.filter fun f =>
          decide (genOf f = genOf Fermion.u) && couplesToCharge f).length = 3)
    ∧ (∀ f g : Fermion, weakDoubletPartner f g = true →
        tildeQ f - tildeQ g = 6 ∨ tildeQ f - tildeQ g = -6)
    ∧ (channelReach derivedWCouples = 2 ∧ cellReach derivedWCouples = 3
        ∧ channelReach derivedZCouples = 2 ∧ cellReach derivedZCouples = 3)
    ∧ (Anchor.r0 Anchor.Sector.Electroweak
        = cellReach derivedWCouples * (Anchor.W : ℤ) + 2 * channelReach derivedWCouples)
    ∧ (weakDoubletPartner .nu1 .e = true ∧ weakDoubletPartner .nu2 .mu = true
        ∧ weakDoubletPartner .nu3 .tau = true)
    ∧ (∀ f : Fermion, derivedWCouples f = false ↔
        ∀ g : Fermion, weakDoubletPartner f g = false) :=
  ⟨derived_w_universal, derived_z_universal, declared_w_eq_derived, declared_z_eq_derived,
   doublet_partner_unique, charge_status_refinement_not_a_matching.1,
   doublet_charge_step_of_partner,
   ⟨channelReach_derived_w, cellReach_derived_w, channelReach_derived_z, cellReach_derived_z⟩,
   ew_yardstick_premise_free,
   ⟨neutrino_leg_forced.1, neutrino_leg_forced.2.1, neutrino_leg_forced.2.2.1⟩,
   w_decouples_iff_no_partner⟩
THEOREM doublet_partner_unique · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
doublet_partner_unique · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:162 
/-- **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
THEOREM weakCharge_sm_pattern · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
weakCharge_sm_pattern · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:235 
/-- **THEOREM (the derived assignment IS the Standard Model weak-isospin
pattern).** Upper members (weak charge `+1`): the up-type quarks and the
neutrinos. Lower members (`−1`): the down-type quarks and the charged
leptons. Computed from the ledger, not imported. -/
theorem weakCharge_sm_pattern :
    weakCharge .u = 1 ∧ weakCharge .c = 1 ∧ weakCharge .t = 1 ∧
    weakCharge .nu1 = 1 ∧ weakCharge .nu2 = 1 ∧ weakCharge .nu3 = 1 ∧
    weakCharge .d = -1 ∧ weakCharge .s = -1 ∧ weakCharge .b = -1 ∧
    weakCharge .e = -1 ∧ weakCharge .mu = -1 ∧ weakCharge .tau = -1 := by
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide
THEOREM derived_w_universal · derived_z_universal · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
derived_w_universal · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:217 
/-- **THEOREM (W universality, derived).** Every fermion species couples
to the W: the doublet matching is perfect (Part II). -/
theorem derived_w_universal (f : Fermion) : derivedWCouples f = true :=
  hasDoubletPartner_all f
derived_z_universal · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:222 
/-- **THEOREM (Z universality, derived).** Every fermion species couples
to the Z: every species carries a nonzero weak charge. -/
theorem derived_z_universal (f : Fermion) : derivedZCouples f = true := by
  cases f <;> decide
THEOREM declared_w_eq_derived · declared_z_eq_derived · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean
declared_w_eq_derived · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:248 
/-- **THEOREM (the declared W coupling was forced).** The C13 module's
declared universal W coupling coincides with the derived doublet coupling
on every species: the declaration carried no free content. -/
theorem declared_w_eq_derived (f : Fermion) :
    GaugeCarrier.couples .wBoson f = derivedWCouples f := by
  cases f <;> decide
declared_z_eq_derived · IndisputableMonolith/Masses/MassGenesis/T10UniversalCoupling.lean:255 
/-- **THEOREM (the declared Z coupling was forced).** -/
theorem declared_z_eq_derived (f : Fermion) :
    GaugeCarrier.couples .zBoson f = derivedZCouples f := by
  cases f <;> decide

What this page does not claim

The package does not derive the numerical values of particle masses or coupling constants. The universality theorem does not claim the framework's fermion list is complete or matches all observed particles. The framework does not explain why the weak force has its particular strength, only that it is universal.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND