decomposition_unique_holds
Uniqueness of the transverse-traceless decomposition for tensor perturbations follows from the structure of TensorPerturbation. Researchers analyzing gravitational wave modes on FRW backgrounds would cite this to confirm that equal TT components force identical perturbations. The proof proceeds by case analysis on the two instances, substitution of the shared h_TT equality, and reflexivity.
claimFor any two tensor perturbations $tp_1$ and $tp_2$, if their transverse-traceless components satisfy $tp_1.h_{TT} = tp_2.h_{TT}$ then $tp_1 = tp_2$.
background
The TensorDecomposition module defines tensor perturbations via the structure TensorPerturbation carrying a transverse-traceless metric component $h_{TT}$. The upstream definition decomposition_unique states that this component uniquely determines the full perturbation object. The result sits inside the Relativity.GW treatment of cosmological perturbations, importing the FRWMetric and Geometry modules to handle background expansions and spatial decompositions.
proof idea
One-line wrapper that applies the definition of decomposition_unique: introduce the two perturbations and the equality hypothesis, perform case splits on both, simplify the hypothesis, substitute to equate the structures, and conclude by reflexivity.
why it matters in Recognition Science
The theorem discharges the uniqueness property for TT tensor modes in the gravitational-wave sector. It closes the definition of decomposition_unique inside the Relativity.GW section and supports consistent mode counting in the eight-tick octave framework. No downstream theorems yet reference it, leaving open its use in explicit waveform propagation results.
scope and limits
- Does not prove existence of a TT decomposition.
- Does not construct the projection operator onto transverse-traceless tensors.
- Does not extend to scalar or vector perturbation sectors.
- Does not address residual gauge freedom after the TT condition is imposed.
formal statement (Lean)
33theorem decomposition_unique_holds : decomposition_unique := by
proof body
Term-mode proof.
34 intro tp1 tp2 h
35 cases tp1; cases tp2; simp at h; subst h
36 rfl
37
38
39end GW
40end Relativity
41end IndisputableMonolith