Prove2Me

Scalar field: every w∈[−1,1]w\in[-1,1] is achievable, without crossing w=−1w=-1

Proved
CosmologyEOS.scalar_field_eos_range

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

cosmologymathematical-physics

Let w(ϕ˙,V)=12ϕ˙2−V12ϕ˙2+Vw(\dot\phi,V) = \dfrac{\frac12\dot\phi^2 - V}{\frac12\dot\phi^2 + V} be the scalar-field equation of state. Then:

  1. (phantom divide) whenever the energy density 12ϕ˙2+V\frac12\dot\phi^2+V is positive, w≥−1w \ge -1;
  2. whenever additionally V≥0V\ge 0, w≤1w\le 1;
  3. every value w∈[−1,1]w\in[-1,1] is achieved by some ϕ˙\dot\phi and V≥0V\ge 0 with 12ϕ˙2+V>0\frac12\dot\phi^2+V>0.

This is the source's statement that any equation of state between the free-field value 11 and the cosmological-constant value −1-1, but not crossing the w=−1w=-1 barrier (the Phantom Divide Line), is achievable by a scalar field.

Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem scalar_field_eos_range :
    (∀ phiDot V : ℝ, 0 < phiDot ^ 2 / 2 + V → -1 ≤ scalarFieldEOS phiDot V) ∧
    (∀ phiDot V : ℝ, 0 ≤ V → 0 < phiDot ^ 2 / 2 + V → scalarFieldEOS phiDot V ≤ 1) ∧
    (∀ w ∈ Set.Icc (-1 : ℝ) 1, ∃ phiDot V : ℝ,
      0 ≤ V ∧ 0 < phiDot ^ 2 / 2 + V ∧ scalarFieldEOS phiDot V = w) := 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' (Phantom Divide Line)
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 all three of: (1) for all real x,Vx,V with x2/2+V>0x^2/2 + V > 0, w(x,V)≥−1w(x,V)\ge -1; (2) for all real x,Vx,V with V≥0V\ge 0 and x2/2+V>0x^2/2+V>0, w(x,V)≤1w(x,V)\le 1; (3) for every real w0w_0 with −1≤w0≤1-1\le w_0\le 1 there exist real x,Vx,V with V≥0V\ge 0, x2/2+V>0x^2/2+V>0 and w(x,V)=w0w(x,V) = w_0.

Human review

View graph