Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Eqs. (4.15) → (4.17): squeezed limit of ⟨γs1γs2γs3⟩\langle\gamma^{s_1}\gamma^{s_2}\gamma^{s_3}\rangle⟨γs1​γs2​γs3​⟩

Proved
Maldacena2003.threeGraviton_squeezed_limit

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

cosmologyinflationmathematical-physics

Let n^∈R3\hat n\in\mathbb R^3n^∈R3 be a unit vector and k⃗2≠0\vec k_2\ne0k2​=0, with k2=∣k⃗2∣k_2=|\vec k_2|k2​=∣k2​∣. Let ϵ1,ϵ2,ϵ3\epsilon^1,\epsilon^2,\epsilon^3ϵ1,ϵ2,ϵ3 be real symmetric traceless 3×33\times33×3 matrices with ϵ1n^=0\epsilon^1\hat n=0ϵ1n^=0, ϵ2k⃗2=0\epsilon^2\vec k_2=0ϵ2k2​=0 and ϵ3k⃗2=0\epsilon^3\vec k_2=0ϵ3k2​=0. These are the polarizations of the soft graviton and of the two hard gravitons, the latter in the limiting configuration k⃗3→−k⃗2\vec k_3\to-\vec k_2k3​→−k2​. Let ρ˙∗\dot\rho_*ρ˙​∗​ be real. Put k⃗1=tn^\vec k_1=t\hat nk1​=tn^ and k⃗3=−k⃗1−k⃗2\vec k_3=-\vec k_1-\vec k_2k3​=−k1​−k2​. Then, with BγγγB_{\gamma\gamma\gamma}Bγγγ​ the correlator (4.15),

lim⁡t→0+2t3 Bγγγ(k⃗1,k⃗2,k⃗3)  =  (ϵij2ϵij3) ρ˙∗2 12k25 2ρ˙∗2 32 ϵij1k2ik2j.\lim_{t\to0^+}2t^3\,B_{\gamma\gamma\gamma}(\vec k_1,\vec k_2,\vec k_3) \;=\; \big(\epsilon^2_{ij}\epsilon^3_{ij}\big)\,\dot\rho_*^2\,\frac{1}{2k_2^5}\,2\dot\rho_*^2\,\frac32\,\epsilon^1_{ij}k_2^ik_2^j .t→0+lim​2t3Bγγγ​(k1​,k2​,k3​)=(ϵij2​ϵij3​)ρ˙​∗2​2k25​1​2ρ˙​∗2​23​ϵij1​k2i​k2j​.

For equal hard polarizations, ϵij2ϵij3=2δs2s3\epsilon^2_{ij}\epsilon^3_{ij}=2\delta_{s_2s_3}ϵij2​ϵij3​=2δs2​s3​​, and the right-hand side is the coefficient in (4.17). The statement is the agreement of (4.15) with (4.17) in the overlapping region.

Formalization Note Mpl=1M_{pl}=1Mpl​=1, and the horizon-crossing times ∗*∗, ∗′*'∗′ are identified at leading order. The polarizations are held fixed along the limit, and the hard polarizations are taken transverse to k⃗2\vec k_2k2​, the limiting direction of ±k⃗3\pm\vec k_3±k3​.

Preamble
import Mathlib
import Definitions.Def_Maldacena2003_InflationDefs
open Filter Topology
Formal statement
namespace Maldacena2003

theorem threeGraviton_squeezed_limit (ρd : ℝ) (n k₂ : EuclideanSpace ℝ (Fin 3))
    (hn : ‖n‖ = 1) (hk₂ : k₂ ≠ 0) (ε₁ ε₂ ε₃ : Matrix (Fin 3) (Fin 3) ℝ)
    (hε₁symm : ∀ i j, ε₁ i j = ε₁ j i) (hε₁tr : Matrix.trace ε₁ = 0)
    (hε₁tv : ∀ i, ∑ j, ε₁ i j * n j = 0)
    (hε₂symm : ∀ i j, ε₂ i j = ε₂ j i) (hε₂tr : Matrix.trace ε₂ = 0)
    (hε₂tv : ∀ i, ∑ j, ε₂ i j * k₂ j = 0)
    (hε₃symm : ∀ i j, ε₃ i j = ε₃ j i) (hε₃tr : Matrix.trace ε₃ = 0)
    (hε₃tv : ∀ i, ∑ j, ε₃ i j * k₂ j = 0) :
    Tendsto
      (fun t : ℝ => 2 * t ^ 3 * threeGravitonBispectrum ρd ε₁ ε₂ ε₃ (t • n) k₂ (-(t • n) - k₂))
      (𝓝[>] 0)
      (𝓝 ((∑ i, ∑ j, ε₂ i j * ε₃ i j) * ρd ^ 2 * (1 / (2 * ‖k₂‖ ^ 5)) * (2 * ρd ^ 2) * (3 / 2)
        * ∑ i, ∑ j, ε₁ i j * k₂ i * k₂ j)) := by sorry

end Maldacena2003
Source
J. Maldacena, Non-Gaussian features of primordial fluctuations in single field inflationary models, JHEP 05 (2003) 013, https://doi.org/10.1088/1126-6708/2003/05/013 (arXiv:astro-ph/0210603), pp. 19–20, eqs. (4.15)–(4.17)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me