Cosmology Gstar Derivation G Star Derived Eq

The derived count

In the hot, dense plasma that filled the universe before the electroweak phase transition, the expansion rate depends on how many particle species are present and relativistic. Cosmologists package that count into a single number, the effective degrees of freedom, written g⋆. For the Standard Model at those temperatures, the standard value is 106.75, a figure that appears throughout early-universe calculations such as baryogenesis.

The declaration g_star_derived_eq in the framework's machine-checked library of formal theorems proves that this number is not a free input. It derives 106.75 by explicitly counting every bosonic and fermionic helicity state in the Standard Model. The gauge bosons contribute 24 states (12 generators of SU(3)×SU(2)×U(1), each with two polarizations), the Higgs adds 4 real scalar degrees of freedom, and the fermions contribute 90 states across three generations. Bosons contribute with weight 1, fermions with weight 7/8, a factor that is itself proved as the ratio of Fermi-Dirac to Bose-Einstein energy densities. The result is the exact rational 427/4, which equals 106.75.

In Recognition Science, this derivation is presented as a consequence of the framework's forced particle content, which fixes the Standard Model's gauge group and matter spectrum. The proof is axiom-clean: it uses only exact rational arithmetic and the definitions of the particle counts, with no fitted parameters. A companion theorem, g_star_derived_eq_baryogenesis, shows that this derived value coincides exactly with the hand-entered constant used in the framework's baryon asymmetry module, replacing a postulate with a computation.

The declaration does not claim that the Standard Model itself is derived from first principles, nor that the value 106.75 is measured. The particle content, the gauge group, and the factor 7/8 are inputs or proved consequences within the framework, but the framework does not derive the existence of quarks or the electroweak symmetry group from its core axioms. The number is a derived consequence of a chosen particle spectrum, not an independent prediction.

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

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

/-- Fermion count = 72 + 12 + 6 = 90. -/
theorem fermionic_dof_eq : fermionic_dof = 90 := by
  unfold fermionic_dof
  rw [quark_dof_eq, charged_lepton_dof_eq, neutrino_dof_eq]

/-- The fermionic Boltzmann factor `7/8` is the exact ratio of the
    Fermi-Dirac to Bose-Einstein energy-density integrals.

    STATUS: THEOREM (proved downstream, not a convention). The value is
    forced by quantum statistics:
    `Cosmology.ThermalWeightSevenEighths.fermi_bose_ratio` proves
    `mellin fermiKernel 4 / mellin boseKernel 4 = 7/8`
    (i.e. `∫ t³/(eᵗ+1) / ∫ t³/(eᵗ−1) = η(4)/ζ(4) = 7/8`), and
    `fermion_boltzmann_forced` identifies this `def` with that ratio.
    That module imports this one, so the pointer here is a docstring;
    the proof is axiom-clean (Mathlib base axioms only).

    The remaining physics input is *which* species takes the `+1`
    (Fermi-Dirac) sign: the exchange sign, which RS forces via
    `Foundation.EightTick.spin_statistics_key`. -/
def fermion_boltzmann : ℚ := 7 / 8

/-- The cast of the derived rational to `ℝ` matches the existing
    `g_star : ℝ` constant in `BaryonAsymmetryDerivation`. -/
theorem g_star_derived_eq_baryogenesis :
    ((g_star_derived : ℚ) : ℝ)
      = IndisputableMonolith.Cosmology.BaryonAsymmetryDerivation.g_star := by
  rw [g_star_derived_eq]
  unfold IndisputableMonolith.Cosmology.BaryonAsymmetryDerivation.g_star
  push_cast
  norm_num

What this page does not claim

The Standard Model particle content is not derived from the framework's core axioms; it is an input. The value 106.75 is not a measurement; it is a derived consequence of the chosen particle spectrum. The declaration does not prove the existence of quarks, leptons, or the electroweak symmetry group.

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: