Foundation Smhypercharge From Cube Su2 Squared U1 Anomaly6 Eq Zero

The weak anomaly check

In the Standard Model of particle physics, the weak nuclear force acts on particles through a symmetry called SU(2), and the hypercharge through U(1). A quantum field theory is only consistent if certain mathematical sums, called anomalies, vanish; otherwise the theory breaks down at high energies. One such condition, the SU(2)²U(1) anomaly, requires that the hypercharges of the particles that feel the weak force add to zero in a specific weighted way.

The declaration su2SquaredU1Anomaly6_eq_zero in the Recognition Science framework's machine-checked library of formal theorems proves this cancellation. It verifies that with the hypercharge assignments for one generation of quarks and leptons, the weighted sum equals zero exactly. The check uses hypercharges scaled by a factor of six, so the quark doublet has hypercharge 1, the lepton doublet has -3, and the calculation confirms that three times the quark value plus the lepton value is zero.

This is a necessary condition for the Standard Model to be mathematically consistent, and the framework shows it holds with no exceptions. The declaration is part of a larger effort to show that the Standard Model's structure can be expressed in the cube-completion framework, but it is not a derivation of the hypercharge values themselves. The values are taken as given from the Standard Model, and the theorem only confirms that they satisfy the anomaly condition.

What this declaration does not claim is that the hypercharges are uniquely forced by the framework. The document explicitly states this is not a proof of uniqueness. It also does not claim to derive the other anomaly conditions, though they are checked separately in the same module. The theorem is a verification of a known consistency condition, not a new physical prediction.

theorem su2SquaredU1Anomaly6_eq_zero : su2SquaredU1Anomaly6 = 0 := by
  native_decide

/-- Hypercharge in sixths: `Y6 = 6Y`. -/
def hypercharge6 : WeylMultiplet -> ℤ
  | .quarkDoublet => 1      -- Y =  1/6
  | .upConjugate => -4      -- Y = -2/3
  | .downConjugate => 2     -- Y =  1/3
  | .leptonDoublet => -3    -- Y = -1/2
  | .electronConjugate => 6 -- Y =  1
  | .neutrinoConjugate => 0 -- Y =  0

What this page does not claim

This declaration does not prove that the hypercharge values are uniquely forced by the cube-completion framework. It does not establish the vanishing of the other anomaly sums, such as SU(3)²U(1) or U(1)³. It does not make a new physical prediction beyond verifying a known consistency condition of the Standard Model.

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/Foundation/SMHyperchargeFromCube.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: