Cosmology Gstar Derivation Bosonic Dof Eq

Counting the bosonic states

In the standard model of particle physics, the energy density of the hot early universe depends on how many particle states are in thermal equilibrium. The effective count of relativistic degrees of freedom, g*, is written as a sum of a bosonic part and a fermionic part, the latter weighted by 7/8. The bosonic part, called g_b, equals 28 in the standard high-temperature regime above the electroweak phase transition, where all gauge bosons are massless.

The declaration bosonic_dof_eq in the framework's machine-checked library of formal theorems proves that this bosonic count is exactly 28. The proof is a direct enumeration: the gauge group SU(3) × SU(2) × U(1) has 8 + 3 + 1 = 12 generators, each carrying two polarizations, giving 24 gauge degrees of freedom. The Higgs sector, one complex doublet, contributes 4 real scalar degrees of freedom. The sum is 24 + 4 = 28, verified by exact rational arithmetic with a closing computation.

This is not a new physical measurement. The number 28 is standard in cosmology textbooks. What the declaration adds is a formal derivation inside the framework's library, replacing a hand-entered constant with a counted result. The same module derives the fermionic count 90 and, with the 7/8 fermion weight, the full g* = 106.75, expressed as the exact rational 427/4. A bridge theorem shows this derived value equals the one used in the framework's baryon asymmetry module.

In Recognition Science, this counting is said to be forced by the Q₃ chord-cube content, a structural claim about the framework's internal geometry. The declaration itself, however, only establishes the arithmetic of the standard model particle content. It does not derive the standard model from first principles, nor does it prove that the universe must contain exactly these particles. It takes the particle content as given and verifies the resulting count.

/-- Bosonic count is the standard 28. -/
theorem bosonic_dof_eq : bosonic_dof = 28 := by
  unfold bosonic_dof gauge_dof gauge_generators gauge_polarisations higgs_dof
  decide

/-- Total gauge-boson DOF above the EW phase transition. -/
def gauge_dof : ℕ := gauge_generators * gauge_polarisations

/-- Higgs sector: one complex `SU(2)` doublet, real components count
    once.  Above the EW transition the Higgs is a 4-component complex
    doublet (2 complex components × 2 real parts each = 4 DOF). -/
def higgs_dof : ℕ := 4

/-- `g_⋆ = 28 + (7/8) × 90 = 28 + 78.75 = 106.75 = 427/4`. -/
theorem g_star_derived_eq : g_star_derived = (427 : ℚ) / 4 := by
  unfold g_star_derived fermion_boltzmann bosonic_dof gauge_dof
         gauge_generators gauge_polarisations higgs_dof
         fermionic_dof quark_dof charged_lepton_dof neutrino_dof
         n_quark_flavours n_colours n_spin_states n_particle_antiparticle
         n_charged_leptons n_neutrino_flavours
  norm_num

What this page does not claim

The declaration does not prove the standard model particle content is necessary. The declaration does not derive the 7/8 fermion weight; that is a separate theorem. The declaration does not establish any physical measurement of g*.

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/Cosmology/GStarDerivation.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: