action_quadratic_tensor
plain-language theorem explainer
Action quadratic tensor supplies a zero placeholder for the second-order contribution of transverse-traceless perturbations to the gravitational wave action. Workers expanding the Recognition Science action around FRW backgrounds would invoke this slot once the kinetic and gradient coefficients are inserted. Implementation consists of an immediate return of the floating-point constant zero that ignores the scale factor, perturbation tensor, alpha, and lag coupling.
Claim. $S_2(a,h_{TT},C_{lag}) := 0$, where $a$ is a positive scale factor, $h_{TT}$ is a transverse traceless tensor perturbation, and $C_{lag} = phi^{-5}$.
background
The ActionExpansion module expands the gravitational wave action around the FRW background. ScaleFactor is the structure holding a positive function a(t). TensorPerturbation encodes the transverse-traceless metric perturbation h_TT. Upstream C_lag is defined as phi^{-5} in EightTickResonance, while the scale function from LargeScaleStructureFromRS returns discrete powers of phi. The local setting is the quadratic expansion prior to isolating tensor contributions.
proof idea
The definition is realized by a direct assignment of the constant 0.0. No lemmas are applied; the body is a literal zero serving as a temporary stand-in for the expression that will later involve the scale factor and lag coupling.
why it matters
This definition occupies the slot for the quadratic tensor action inside the GW expansion. It is expected to support later module siblings such as action_form_verified and isolate_tensor_contribution. In the Recognition framework it connects to the eight-tick resonance through C_lag and to FRW cosmology through ScaleFactor. The zero value marks an open implementation step before the full derivation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.