Prove2Me

Scalar field: free field w=1w=1, frozen field w=−1w=-1

Proved
CosmologyEOS.scalar_field_limiting_cases

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologymathematical-physics

For a homogeneous scalar field with time derivative ϕ˙\dot\phi and potential energy VV, the equation of state is w=12ϕ˙2−V12ϕ˙2+Vw = \dfrac{\frac12\dot\phi^2 - V}{\frac12\dot\phi^2 + V}. Then:

  1. a free field (V=0V = 0) with ϕ˙≠0\dot\phi\neq 0 has w=1w = 1;
  2. a field with vanishing kinetic energy (ϕ˙=0\dot\phi = 0) and V≠0V\neq 0 has w=−1w=-1, i.e. it is equivalent to a cosmological constant.
Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem scalar_field_limiting_cases :
    (∀ phiDot : ℝ, phiDot ≠ 0 → scalarFieldEOS phiDot 0 = 1) ∧
    (∀ V : ℝ, V ≠ 0 → scalarFieldEOS 0 V = -1) := by
  sorry

end CosmologyEOS
Source
Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, section 'Scalar modeling'
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

With w(x,V)=x2/2−Vx2/2+Vw(x,V) = \dfrac{x^2/2 - V}{x^2/2 + V} (value 00 when the denominator is 00), the statement asserts both: (1) for every real x≠0x\ne 0, w(x,0)=1w(x,0) = 1; (2) for every real V≠0V\ne0, w(0,V)=−1w(0,V) = -1.

Human review

View graph