Cosmology Ewphase Transition Friedmann Coeff Pos

A positive coefficient

The Friedmann equation governs how the universe expands. In the radiation-dominated era, when the universe was a hot, dense soup of relativistic particles, it takes the form H² = (8π²/90) · G · g★ · T⁴. Here H is the Hubble rate, the fractional expansion rate of space; G is the gravitational constant; g★ counts the effective number of particle species; and T is the temperature. The coefficient 8π²/90 comes from the Stefan-Boltzmann law for radiation. The declaration friedmann_coeff_pos proves the simple fact that this coefficient is positive.

That positivity is not a deep cosmological insight; it is a sanity check. The coefficient is a product of squares and positive constants, so it must be greater than zero. The theorem is a formal, machine-checked statement that this is indeed the case. Within the Recognition Science framework, the same coefficient appears with G expressed as φ⁵/π, where φ is the golden ratio, but the positivity result itself does not depend on that substitution. The proof is a direct calculation, not a new physical law.

The importance of the declaration is not the result itself, but what it represents. It is part of a larger, machine-checked library of formal theorems. Each such theorem, however small, is a verified brick in a larger edifice. The positivity of the Friedmann coefficient is a necessary condition for the subsequent construction of the Hubble rate at the electroweak transition temperature, and for the ratio of sphaleron processes to the Hubble rate that appears in theories of baryogenesis. Without a positive coefficient, the square root needed to define the Hubble rate would be undefined, and the whole chain of reasoning would collapse.

What this declaration does not claim is equally important. It does not claim that the Friedmann equation itself is derived from Recognition Science; the equation is imported from standard cosmology. It does not claim that the numerical value of the coefficient, or the resulting Hubble rate, has been measured or compared with observation. It does not claim that the sphaleron-to-Hubble ratio, which this positivity enables, actually explains the observed baryon asymmetry of the universe. That connection, which would require a full Boltzmann transport calculation, remains an open problem. The declaration is a small, formal, and correct statement about the sign of a number, and it is scoped precisely as such.

theorem friedmann_coeff_pos : 0 < friedmann_coeff := by
  unfold friedmann_coeff
  positivity

What this page does not claim

The Friedmann equation itself is derived from Recognition Science. The numerical value of the Hubble rate at the electroweak transition has been measured or compared with observation. The sphaleron-to-Hubble ratio explains the observed baryon asymmetry of the universe.

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