decompose_perturbation
plain-language theorem explainer
The declaration states that every symmetric 3-by-3 real matrix representing a spatial metric perturbation admits an additive split into a transverse-traceless tensor drawn from TensorPerturbation, a scalar trace, and a symmetric vector term. Gravitational-wave analysts working in linearized gravity on a three-dimensional spatial slice would cite it when isolating radiative degrees of freedom from gauge modes. The definition is realized by a direct existential quantifier over the TensorPerturbation structure together with scalar and vector data.
Claim. For any $h : (Fin 3) → (Fin 3) → ℝ$, there exist a transverse-traceless tensor field $h^{TT}$ (satisfying the divergence-free and traceless conditions of TensorPerturbation), a scalar $s ∈ ℝ$, and a vector $v : Fin 3 → ℝ$ such that $h_{ij} = h^{TT}_{ij} + s δ_{ij} + (v_i + v_j)$.
background
In the Recognition Science treatment of gravitational waves, spatial metric perturbations live on the three-dimensional spatial slice fixed by T8. The structure TensorPerturbation packages a time-dependent tensor that is required to be transverse (sum over one index vanishes) and traceless (diagonal sum vanishes) at every time; its h_TT component at t=0 supplies the radiative part in the present definition. Upstream structures on PhiForcingDerived and SpectralEmergence supply the J-cost convexity and the SU(3)×SU(2)×U(1) gauge content that together enforce D=3, while the imported FRWMetric supplies the background on which the perturbation h is defined.
proof idea
The definition is a direct existential wrapper: it asserts the existence of an instance of TensorPerturbation whose h_TT field at time zero, together with a scalar and a vector, reproduces the input h exactly. No external lemmas are invoked; the body simply packages the transverse and traceless conditions already declared inside TensorPerturbation.
why it matters
This definition supplies the basic mode decomposition required for separating tensor, vector, and scalar sectors in gravitational-wave analyses inside the Recognition framework. It precedes uniqueness statements such as decomposition_unique in the same module and supports the eight-tick octave dynamics on the three-dimensional spatial slice (T8). No open questions are closed here, but the declaration completes the interface between arbitrary perturbations and the TT sector used for wave propagation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.