TensorPerturbation
plain-language theorem explainer
TensorPerturbation encodes the transverse-traceless spatial metric perturbation in three dimensions for gravitational wave analysis in Recognition Science. Workers on quadratic actions for tensor modes cite it when isolating physical degrees of freedom after gauge fixing. The definition directly imposes the two algebraic constraints on the map h_TT without invoking lemmas or reductions.
Claim. A tensor perturbation is a map $h_{TT}:ℝ→M_3(ℝ)$ obeying transversality $∑_j h_{TT}(t)_{ij}=0$ for each fixed $t,i$ and tracelessness $∑_i h_{TT}(t)_{ii}=0$ for each $t$.
background
Recognition Science decomposes metric perturbations in the gravitational wave sector after fixing the transverse-traceless gauge in three spatial dimensions. The structure supplies the type carrying the two constraints that remove scalar and vector modes. Upstream results include the structure of J-cost minimization, which states that J-cost minimization is convex with unique global minimum at x=1, and the structure of Q₃ that forces exactly three spatial dimensions.
proof idea
This is a structure definition. The two fields directly encode the summation conditions for transversality and tracelessness on the tensor map; no lemmas or tactics are applied.
why it matters
The structure supplies the input type for action_quadratic_tensor, isolate_tensor_contribution and action_form_verified in the ActionExpansion module. It fills the TT projection step required by the D=3 forcing chain and supports the downstream uniqueness and decomposition statements in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.