Cosmology Entropy Per Photon Entropy Per Photon Lt

The entropy per photon

In cosmology, the entropy per photon is a dimensionless measure of how much disorder, or entropy, is carried by each photon in the universe's radiation. It is a standard input in calculations of how matter came to outnumber antimatter. The conventional value used in textbooks is about 7.04, a number that appears in many early-universe formulas.

In Recognition Science, this number is not taken as a given. A machine-checked library of formal theorems derives it from three ingredients. First, the Riemann zeta function at 3, written ζ(3), is bounded between 1.202042 and 1.202065 by splitting its infinite sum into a finite part and a telescoping tail. Second, π⁴ is bounded between 97.40900 and 97.40914 using standard bounds on π. Third, the effective number of entropy degrees of freedom, g*s, is computed as 43/11 from the Standard Model particle content: photons with 2 polarizations, electrons and positrons with 4 fermionic degrees of freedom, and 3 neutrino generations with 6 fermionic degrees of freedom, with a 7/8 weight for fermions that is itself proved from a series identity.

The combination gives the formula s/nγ = π⁴ g*s / (45 ζ(3)), which the library proves lies in the interval (7.0393, 7.0396). The declaration entropyPerPhoton_lt is the upper half of that bound: it proves the value is less than 7.0396. A companion theorem proves it is greater than 7.0393, and another shows it is within 0.0007 of 7.04, confirming the textbook constant to three significant figures.

The derivation also includes a proof that the neutrino temperature is diluted relative to photons by the cube root of 4/11, a consequence of entropy conservation when electrons and positrons annihilate. The 7/8 fermion weight and the thermodynamic integrals for fermions and bosons are proved, not assumed. What remains as model input is the particle content of the Standard Model and the two conservation hypotheses: comoving entropy conservation and free neutrino streaming.

The result matters because it replaces a bare constant with a derivation. The entropy per photon is no longer an empirical input in this framework; it follows from the particle inventory and the rules of statistical mechanics. The window (7.0393, 7.0396) is narrow enough to fix the value for practical use, and the proof is machine-checked, meaning the arithmetic and analysis are verified step by step.

/-- **THEOREM.** `s/n_γ > 7.0393`. -/
theorem entropyPerPhoton_gt : (7.0393 : ℝ) < entropyPerPhoton := by
  have hz := zeta3_lt
  have hp := pi4_gt
  have hzpos := zeta3_pos
  unfold entropyPerPhoton
  rw [lt_div_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
  nlinarith

/-- **THEOREM.** `s/n_γ < 7.0396`. -/
theorem entropyPerPhoton_lt : entropyPerPhoton < (7.0396 : ℝ) := by
  have hz := zeta3_gt
  have hp := pi4_lt
  have hzpos := zeta3_pos
  unfold entropyPerPhoton
  rw [div_lt_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
  nlinarith

/-- **THEOREM.** `s/n_γ < 7.0396`. -/
theorem entropyPerPhoton_lt : entropyPerPhoton < (7.0396 : ℝ) := by
  have hz := zeta3_gt
  have hp := pi4_lt
  have hzpos := zeta3_pos
  unfold entropyPerPhoton
  rw [div_lt_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
  nlinarith

/-- **THEOREM.** `g*s = 43/11 ≈ 3.909`. -/
theorem gStarS_eq : gStarS = 43 / 11 := by
  unfold gStarS gPhoton fermionWeight gNeutrino
  rw [dilutionCubed_eq]
  norm_num

theorem dilutionCubed_eq : dilutionCubed = 4 / 11 := by
  unfold dilutionCubed gAfter gBefore gPhoton fermionWeight gElectron
  norm_num

What this page does not claim

The particle content of the Standard Model is not derived; it is a model input. The value 7.04 is not claimed to be exact; it is rounded from the derived window. The proof does not claim that the entropy per photon is constant throughout cosmic history.

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