pith. sign in
module module moderate

IndisputableMonolith.Relativity.GW.ActionExpansion

show as:
view Lean formalization →

The ActionExpansion module expands the gravitational wave action to quadratic order in tensor perturbations on an FRW background. It isolates the tensor contribution and defines kinetic and gradient coefficients for the effective wave action. Researchers deriving modified propagation speeds or GW constraints would cite these expansions. The module consists of targeted definitions that build the quadratic form without a central theorem.

claimThe module defines the quadratic tensor action $S^{(2)}[h_{ij}^{TT}]$ obtained by expanding the full action around the FRW metric, together with the kinetic coefficient $K$ and gradient coefficient $G$ such that the second-order action takes the form $S^{(2)} = 1/2 int a^3 (K dot h_{ij}^2 - G (nabla h_{ij})^2) d^4x$.

background

This module sits inside the gravitational wave sector of the Recognition Science relativity development. It imports the FRWMetric for the background cosmology, Fields for the underlying field content, Geometry for the metric perturbations, and TensorDecomposition for the transverse-traceless gauge $h_{ij}^{TT}$. The sibling definitions action_quadratic_tensor, expand_action_around_FRW, isolate_tensor_contribution, kinetic_coefficient, gradient_coefficient, and action_form_verified supply the concrete objects that perform the expansion and extract the quadratic terms.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the quadratic action for tensor modes that is imported by the parent Relativity.GW module and by PropagationSpeed. The GW module aggregates this expansion to obtain the effective wave equation and the speed modification $c_T^2 = 1 + O(alpha_C)$. It therefore completes the step that converts the background action into the tensor wave operator used for propagation analysis.

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)