Prove2Me

Eq. (2.8): eliminating the torsion from the motion equation (2.4)

Proved
PereiraGuimaraesElko.motion_eq_2_8

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

cosmologymathematical-physicsordinary-differential-equations

Let κ,H,h,Φ,Φ˙,Φ¨,V′\kappa,H,h,\Phi,\dot\Phi,\ddot\Phi,V' be real numbers (instantaneous values of the Hubble rate, the torsion function, the field, its first two time derivatives and dV/dΦdV/d\Phi). Assume the torsion relation (2.5), h=−18κ2Φ21+κ2Φ2/8Hh=-\frac18\frac{\kappa^2\Phi^2}{1+\kappa^2\Phi^2/8}H. Then

Φ¨+3HΦ˙+V′−34(H+h)2Φ=0(2.4)\ddot\Phi+3H\dot\Phi+V'-\frac34(H+h)^2\Phi=0\qquad(2.4)

holds if and only if

Φ¨+3HΦ˙+V′−34 H2Φ(1+κ2Φ2/8)2=0.(2.8)\ddot\Phi+3H\dot\Phi+V'-\frac34\,\frac{H^2\Phi}{(1+\kappa^2\Phi^2/8)^2}=0.\qquad(2.8)

The last term of (2.8) is the torsion-induced friction-like term that distinguishes the Elko equation from the scalar-field equation (1.3).

Formalization Note Pointwise in time, so stated for real numbers. The converse direction, also true, is included.

Preamble
import Mathlib
Formal statement
namespace PereiraGuimaraesElko

theorem motion_eq_2_8 (κ H h Φ Φdot Φddot dV : ℝ)
    (h25 : h = -(1 / 8) * (κ ^ 2 * Φ ^ 2 / (1 + κ ^ 2 * Φ ^ 2 / 8)) * H) :
    Φddot + 3 * H * Φdot + dV - 3 / 4 * (H + h) ^ 2 * Φ = 0 ↔
      Φddot + 3 * H * Φdot + dV - 3 / 4 * (H ^ 2 * Φ) / (1 + κ ^ 2 * Φ ^ 2 / 8) ^ 2 = 0 := by
  sorry

end PereiraGuimaraesElko
Source
S. H. Pereira and T. M. Guimarães, "From inflation to recent cosmic acceleration: the fermionic Elko field driving the evolution of the universe", JCAP 09 (2017) 038, https://doi.org/10.1088/1475-7516/2017/09/038 (arXiv:1702.07385), p. 5, Eqs. (2.4), (2.5), (2.8)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph