Foundation Smhypercharge From Cube Su3 Squared U1 Anomaly6 Eq Zero

Anomaly cancellation

In particle physics, an anomaly is a symmetry that works at the classical level but breaks when quantum effects are included. If a gauge symmetry develops an anomaly, the theory becomes inconsistent: probabilities can turn negative, and the mathematical machinery of quantum field theory collapses. The Standard Model avoids this disaster because its particle content is arranged so that all such anomalies cancel. One of these cancellation conditions involves the hypercharge (a quantum number roughly tracking average electric charge) and the strong force's SU(3) gauge group; the condition reads 2Y_Q + Y_u^c + Y_d^c = 0, where the Y's are hypercharges of the quark doublet and the two singlet quarks.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration, su3SquaredU1Anomaly6_eq_zero, that verifies this exact cancellation. The framework models the Standard Model's hypercharges in units of one-sixth, so the quark doublet has hypercharge 1, the up-conjugate quark has -4, and the down-conjugate quark has 2. Substituting these into the anomaly condition gives 2(1) + (-4) + 2 = 0, which the declaration proves by direct computation. This is not a new physical prediction; it is a formal confirmation that the framework's representation of the known hypercharge assignments satisfies one of the consistency requirements the Standard Model must meet.

The declaration also sits inside a larger certificate, smHyperchargeCert, that bundles several such checks: the SU(2)^2 U(1) anomaly, the gravitational-U(1) anomaly, and the cubic U(1)^3 anomaly all vanish in the same integer arithmetic. Together these certify that one left-handed generation of Standard Model fermions, including the sterile neutrino, is anomaly-free. The framework's contribution here is not to derive the hypercharge values from first principles; the docstring explicitly states this is not a proof that these hypercharges are uniquely forced. Rather, the framework takes the Standard Model's known assignments and verifies, in a machine-checked way, that they satisfy the consistency conditions.

The practical consequence is a bridge between the framework's cube-completion gauge skeleton and the Standard Model's particle content. The framework has already proved the gauge group SU(3) x SU(2) x U(1) emerges from its cube completion; this declaration shows that the hypercharges attached to the known fermion multiplets are compatible with that gauge structure. It is a coherence check, not a derivation. The reader should take away that the framework can reproduce a standard consistency condition of the Standard Model with a formal proof, but it does not claim to explain why the hypercharges have the values they do.

theorem su3SquaredU1Anomaly6_eq_zero : su3SquaredU1Anomaly6 = 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

def smHyperchargeCert : SMHyperchargeCert where
  six_multiplets := weylMultiplet_count
  one_generation_16 := generationWeylStateCount_eq_16
  three_generations_b3 := threeGenerationWeylStateCount_eq_48
  su3_anomaly_zero := su3SquaredU1Anomaly6_eq_zero
  su2_anomaly_zero := su2SquaredU1Anomaly6_eq_zero
  gravitational_anomaly_zero := gravitationalU1Anomaly6_eq_zero
  cubic_anomaly_zero := cubicU1Anomaly6_eq_zero
  quark_charges := quark_doublet_charges
  lepton_charges := lepton_doublet_charges
  higgs_y6 := higgsHypercharge6_eq

What this page does not claim

This declaration does not prove the hypercharge values are uniquely forced by the framework. It does not derive the Standard Model's particle content from first principles. It does not address anomalies involving the Higgs field or higher-loop corrections.

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: