Eq. (4.9): $f = \frac56$ for equilateral triangles and $f\to0$ in the squeezed limit

Proved

Maldacena2003.shapeF_equilateral_and_squeezed

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

cosmologyinflationmathematical-physics

Let $k>0$ and let $f$ be the shape function of eq. (4.9).

For the equilateral triangle, $f(k,k,k)=\frac56$ .
As $(k_2,k_3)\to(k,0)$ through pairs for which $(k,k_2,k_3)$ is a momentum triangle with positive sides, $f(k,k_2,k_3)\to0$ .

These are the two extreme values of $f$ described after (4.9). Since $f$ is homogeneous of degree zero, the second item is the statement that $f\to0$ "when two sides become much larger than the third".

Formalization Note The squeezed limit is a limit in $\mathbb R^2$ within the momentum-triangle set.

Preamble

import Mathlib
import Definitions.Def_Maldacena2003_InflationDefs
open Filter Topology

Formal statement

namespace Maldacena2003

theorem shapeF_equilateral_and_squeezed (k : ℝ) (hk : 0 < k) :
    shapeF k k k = 5 / 6 ∧
      Tendsto (fun p : ℝ × ℝ => shapeF k p.1 p.2)
        (𝓝[{p : ℝ × ℝ | IsMomentumTriangle k p.1 p.2}] (k, 0)) (𝓝 0) := 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), p. 18, sentence after eq. (4.9)

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

Eq. (4.9): f=56f = \frac56f=65​ for equilateral triangles and f→0f\to0f→0 in the squeezed limit

Eq. (4.9): $f = \frac56$ for equilateral triangles and $f\to0$ in the squeezed limit