Cosmology Ewphase Transition Hubble Sq At Ew Pos

The Hubble rate at the electroweak scale

In the standard cosmological picture, the early universe was a hot, dense plasma of elementary particles. As it expanded and cooled, it passed through a series of phase transitions, akin to water freezing into ice. One of these, the electroweak phase transition, occurred when the universe was about 10^-12 seconds old and had a temperature around 100 GeV, or roughly a trillion degrees. At this moment, the electromagnetic and weak nuclear forces, which are unified at higher energies, separated into the distinct forces we observe today. This transition is a key ingredient in the theory of electroweak baryogenesis, a proposed mechanism for how the observed excess of matter over antimatter in the universe came to be.

A central quantity in this epoch is the Hubble rate, H, which measures how fast the universe is expanding. In the radiation-dominated era, the Friedmann equation relates this expansion rate to the energy density of the plasma. The energy density, in turn, depends on the temperature T and the number of effective relativistic degrees of freedom, g*, which counts the particle species present. The standard formula is H² = (8π³/90) · G · g* · T⁴, where G is Newton's gravitational constant. This equation is a foundational result of modern cosmology, and its derivation from Einstein's field equations is a well-established result in general relativity.

In Recognition Science, a framework that derives physical structure from a formal calculus of recognition events, this standard cosmological formula is implemented as a formal definition. The declaration hubble_sq_at_ew is that definition: it sets H² at the electroweak temperature to be exactly the product of the Friedmann coefficient, the framework's value for G, the standard g* of 106.75, and the fourth power of the temperature. The companion theorem, hubble_sq_at_ew_pos, proves that this quantity is strictly positive. The proof is a simple consequence of the positivity of each individual factor: the Friedmann coefficient, the gravitational constant, the effective degrees of freedom, and the fourth power of a positive temperature are all positive. This result is machine-checked, meaning it has been verified by a computer program to follow from the definitions and axioms of the framework's formal library.

The positivity of H² is a sanity check, not a profound discovery. It confirms that the framework's implementation of the standard cosmology is internally consistent and that the defined quantity is physically meaningful, since a negative or zero expansion rate squared would be unphysical. The framework's library shows that this positive quantity can then be used to construct a dimensionless ratio, the sphaleron-to-Hubble ratio, which is a measure of how efficiently certain particle interactions, sphalerons, could erase a matter-antimatter asymmetry. This ratio is itself proven to be positive, and it forms the basis of a proposed washout efficiency factor.

However, it is important to be precise about what this declaration does not claim. It does not connect this positive Hubble rate to the framework's separate, Planck-matched expression for the final baryon asymmetry, η_B. That expression is a different, standalone result. The washout factor built from hubble_sq_at_ew is explicitly labeled as a scaffold, a positive-definite placeholder for a future, genuine calculation. A real connection between the sphaleron rate and the final matter-antimatter asymmetry would require a full Boltzmann transport calculation through the phase transition, a task that remains open. The theorem hubble_sq_at_ew_pos is therefore a small, verified piece of a much larger puzzle, confirming the consistency of one step without claiming the whole journey is complete.

theorem hubble_sq_at_ew_pos : 0 < hubble_sq_at_ew := by
  unfold hubble_sq_at_ew
  exact mul_pos (mul_pos (mul_pos friedmann_coeff_pos G_rs_pos) g_star_ew_pos)
    (pow_pos T_ew_pos 4)

/-- H² at T_EW in RS-native units, with the T⁴ factor INCLUDED:
    H² = friedmann_coeff · G_rs · g★ · T_EW⁴.
    (The 2026-06-25 review caught the earlier omission of T⁴; this
    definition now matches the header formula exactly.) -/
def hubble_sq_at_ew : ℝ := friedmann_coeff * G_rs * g_star_ew * T_ew ^ 4

/-- The fixed g★ = 106.75 used at T_EW equals the high-temperature
    evaluation of the g_star(T) threshold step function: the constant is a
    function value, not a free-standing number. -/
theorem g_star_ew_matches_threshold_fn :
    g_star_ew = ((GStarThresholds.g_star 200 : ℚ) : ℝ) := by
  rw [GStarThresholds.g_star_high]
  norm_num [g_star_ew]

What this page does not claim

This theorem does not connect the positive Hubble rate to the framework's separate expression for the final baryon asymmetry η_B. The washout efficiency factor built from this theorem is a scaffold, not a thermal washout calculation. The theorem does not prove that the electroweak phase transition is first order or that baryogenesis actually occurred.

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: