Maldacena's consistency relation (eqs. 4.5–4.7): as
ProvedMaldacena2003.squeezed_limit_consistency_relationLet , , real, and . Let be the leading slow-roll three-scalar correlator of eqs. (4.5)–(4.6), the scalar power spectrum (2.20), and the scalar tilt (2.22). Then, as through pairs for which is a momentum triangle with positive sides,
In words: when one momentum is much smaller than the other two, the three-point function of equals times the product of the two-point functions, . This is the single-field consistency relation, eq. (4.7), recovered from the general formula (4.5)–(4.6).
Formalization Note , , the factor is dropped, and the horizon-crossing times , are identified at leading order in slow roll. The limit is taken in within the momentum-triangle set; momentum conservation forces .
import Mathlib import Definitions.Def_Maldacena2003_InflationDefs open Filter Topology
namespace Maldacena2003
theorem squeezed_limit_consistency_relation (ρd φd φdd k : ℝ)
(hρ : 0 < ρd) (hφ : φd ≠ 0) (hk : 0 < k) :
Tendsto
(fun p : ℝ × ℝ => zetaBispectrum ρd φd φdd k p.1 p.2
/ (zetaPowerSpectrum ρd φd k * zetaPowerSpectrum ρd φd p.2))
(𝓝[{p : ℝ × ℝ | IsMomentumTriangle k p.1 p.2}] (k, 0))
(𝓝 (-scalarTilt ρd φd φdd)) := by sorry
end Maldacena2003Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.