Foundation Smgauge Algebra Hyper Gen Count

The hypercharge generator

The Standard Model of particle physics describes three of the four known forces using symmetry groups. Each group comes with a fixed number of force carriers, called gauge bosons. The strong force, based on the group SU(3), has eight gluons. The weak force, based on SU(2), has three bosons: the W plus, W minus, and Z. The hypercharge force, based on the group U(1), has exactly one carrier, the B boson, which mixes with the neutral weak boson to produce the photon and the Z. The number of generators of a Lie group equals the number of its force carriers, and for U(1) that number is one.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration named hyper_gen_count that proves this count. In plain terms, the declaration establishes that the generator count for the hypercharge factor in the framework's model of the Standard Model gauge algebra is exactly 1. This is not a new physical measurement; it is a formal proof inside the framework's library that its own definition of the hypercharge factor, built from the formula N² for the number of generators of U(N) with N=1, evaluates to 1. The proof is a direct computation, checked by the machine, with no unproved assumptions and no axioms beyond the standard logical ones.

The declaration is one piece of a larger certificate that the framework assembles for the Standard Model gauge group. The full certificate, named SMGaugeAlgebraCert, bundles together the generator counts for all three factors: 8 for the strong force, 3 for the weak force, and 1 for the hypercharge force, summing to 12 total gauge generators, which matches the empirical count in the Standard Model. The certificate also records that there are exactly three gauge factors, matching the cube-automorphism three-layer decomposition that the framework uses to derive the group structure. The hyper_gen_count declaration is the specific theorem that pins down the hypercharge contribution to this total.

What the declaration does not claim is just as important as what it proves. It does not claim that the hypercharge force itself has been measured to have one carrier; that is an empirical fact of the Standard Model, not a theorem. It does not claim that the framework has derived the full gauge group structure from first principles; that structural-rank certificate is honestly tagged as started, not completed. And it does not claim that the identification of the cube-automorphism decomposition with the Standard Model gauge group is itself proved; that identification is a structural prediction, with a stated falsifier: any RS-derived gauge group with the same cube-automorphism rank decomposition must have exactly 12 generators, and any deviation would falsify the identification.

theorem hyper_gen_count : factorGenCount .hyperY = 1 := by decide

theorem sm_total_gen_count : smTotalGenCount = 12 := by decide

/-- SM gauge-algebra certificate. -/
def smGaugeAlgebraCert : SMGaugeAlgebraCert where
  strong := strong_gen_count
  weak := weak_gen_count
  hyperY := hyper_gen_count
  total := sm_total_gen_count
  factor_count := factor_count

What this page does not claim

The declaration does not prove that the hypercharge force has one carrier as an empirical measurement. The declaration does not derive the full Standard Model gauge group structure from first principles. The declaration does not prove that the cube-automorphism decomposition is the Standard Model gauge group; that identification remains a structural prediction.

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/SMGaugeAlgebra.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: