pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.GW.ActionExpansion

show as:
view Lean formalization →

This module defines the quadratic expansion of the gravitational wave action around the FRW background, isolating tensor-mode contributions via TT decomposition and extracting kinetic and gradient coefficients. Cosmologists and modified-gravity researchers cite these definitions when computing propagation speeds or confronting GW170817 bounds. The module is a pure definition block whose structure chains expand_action_around_FRW into isolate_tensor_contribution and action_quadratic_tensor, followed by coefficient extraction and form verification

claimThe quadratic tensor action around the FRW metric is $S^{(2)}[h^{TT}] = K(h^{TT}) - G(h^{TT})$, where the kinetic coefficient $K$ and gradient coefficient $G$ are obtained by expanding the full action to second order in the transverse-traceless perturbation $h_{ij}^{TT}$ and projecting onto the tensor sector.

background

The module operates inside the Relativity.GW section of the Recognition Science framework. It imports FRWMetric to supply the background scale factor and Hubble parameter, Fields for the underlying stress-energy and curvature scalars, Geometry for the metric signature and covariant derivatives, and TensorDecomposition for the transverse-traceless projection that isolates $h_{ij}^{TT}$ from scalar and vector modes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

ActionExpansion supplies the quadratic tensor action that is imported by the parent Relativity.GW module, which assembles the complete tensor perturbation theory and feeds PropagationSpeed to obtain the modified speed $c_T^2 = 1 + O(alpha_C)$. In the Recognition Science chain this step realizes the eight-tick octave (T7) and three-dimensional spatial structure (T8) for wave propagation, directly enabling the GW170817 constraints listed in the downstream module documentation.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (6)