Masses Mass Genesis T10 Universal Coupling

The universal coupling theorem

In the standard model of particle physics, the W and Z bosons are the carriers of the weak force, the interaction responsible for radioactive decay. A fermion, a class of particle that includes quarks and leptons, couples to these bosons if it participates in that interaction. For decades, the pattern of which fermions couple to which boson has been a measured fact, encoded in the Standard Model but not derived from a deeper principle.

The Recognition Science framework treats this pattern as a consequence of its own structure. The framework's ledger, a discrete record of recognition events, classifies fermions by generation and colour status. From this classification alone, the framework defines a weak-doublet partner: two distinct fermions that share a generation and a colour status. The module T10UniversalCoupling.lean proves that this definition is not empty. Its central theorem, universal_coupling_package, establishes a bundle of results: every fermion in the ledger has exactly one such partner, every fermion couples to both the W and Z bosons, and the derived coupling pattern exactly matches the declared one.

The proof is a finite check. The ledger contains a fixed list of fermions, and the theorems derived_w_universal and derived_z_universal verify by case analysis that each one, from the up quark to the tau neutrino, satisfies the coupling condition. The result weakCharge_sm_pattern then reproduces the familiar Standard Model assignment: up-type quarks and neutrinos carry weak charge +1, down-type quarks and charged leptons carry -1. The module also proves that the W boson's reach, measured in the framework's channel and cell counts, is exactly 2 and 3, matching the electroweak yardstick equation that anchors the framework's scale.

What this establishes in plain language is that the weak force's universal coupling is not an input but an output. The framework models the Standard Model's coupling pattern as a forced consequence of its ledger structure, with no free parameters and no imported assumptions. The proof is machine-checked, meaning every step is verified by a computer against the framework's axioms. This is a derivation within the framework, not a measurement; the framework claims to explain why the pattern holds, not merely to describe it.

/-- **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 (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

/-- **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 (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

/-- **THEOREM (the declared Z coupling was forced).** -/
theorem declared_z_eq_derived (f : Fermion) :
    GaugeCarrier.couples .zBoson f = derivedZCouples f := by
  cases f <;> decide

/-- **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

What this page does not claim

This derivation does not predict the numerical values of fermion masses. The proof does not establish that the Standard Model is the only possible physical theory consistent with the ledger. The module does not derive the existence of the Higgs boson or its role in mass generation.

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: