Cosmology Inflation Efficient Reheating

The Reheating Step

Cosmic inflation is the proposed period of exponential expansion in the first fraction of a second after the Big Bang. It solves classic puzzles: why the universe looks flat, why distant regions have the same temperature, and why magnetic monopoles are not observed. The standard mechanism uses a scalar field, the inflaton, slowly rolling down a potential energy hill. When the field reaches the bottom, it oscillates and decays, producing the hot bath of particles that becomes the observable universe. That final step is reheating.

In Recognition Science, the framework models the inflaton potential directly as its cost function, a measure of how far a system is from its preferred state. The cost function is J(x) = (x + 1/x)/2 - 1, which has its minimum at x = 1. The framework's declaration efficient_reheating states that oscillations around this minimum decay into particles. In plain terms: once the field reaches its lowest cost, the leftover motion converts into the particles that populate the universe. The declaration is a theorem in the framework's machine-checked library of formal theorems, but its proof is a placeholder: the body of the theorem is the constant True, meaning the statement is asserted rather than derived from a physical model.

The classical picture of reheating is well established in cosmology. After inflation, the inflaton field oscillates about the minimum of its potential. These oscillations decay through parametric resonance and perturbative processes, transferring energy to standard model particles. The framework's declaration captures the endpoint of this process, not the dynamics. It does not specify the reheating temperature, the decay rate, or the coupling between the inflaton and other fields. The Reheating structure in the library only records that a temperature exists and is positive, without deriving its value.

What the declaration does establish is a consistency statement: within the framework, the end of inflation is not a separate assumption but a consequence of the same cost function that drives the expansion. The field rolls down, reaches the minimum, and the oscillations decay. This is a structural claim about the framework's internal logic, not a quantitative prediction about the early universe. The framework's own predictions for observable quantities, such as the spectral index and tensor-to-scalar ratio, are separate definitions that match current measurements, but the reheating declaration itself makes no numerical claim.

/-- The inflaton potential in RS is just the J-cost. -/
noncomputable def inflatonPotential (φ : ℝ) (hφ : φ > 0) : ℝ := Jcost φ

/-- **THEOREM (Efficient Reheating)**: The inflaton couples to SM fields,
    allowing efficient energy transfer after inflation. -/
theorem efficient_reheating :
    -- Oscillations around φ = 1 decay into particles
    True := trivial

/-- **THEOREM (Efficient Reheating)**: The inflaton couples to SM fields,
    allowing efficient energy transfer after inflation. -/
theorem efficient_reheating :
    -- Oscillations around φ = 1 decay into particles
    True := trivial

/-- After inflation ends, the inflaton oscillates around φ = 1
    and decays into Standard Model particles. -/
structure Reheating where
  /-- Reheating temperature. -/
  temperature : ℝ
  /-- Temperature is positive. -/
  temp_pos : temperature > 0

What this page does not claim

The declaration does not prove that reheating actually occurs in the physical universe; it is a formal statement within the framework. The declaration does not specify the reheating temperature, decay rate, or any particle physics coupling. The declaration does not derive the spectral index or tensor-to-scalar ratio; those are separate definitions in the same library.

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