decomposition_unique
plain-language theorem explainer
Uniqueness of the transverse-traceless decomposition asserts that two tensor perturbations coincide whenever their h_TT fields match. Gravitational-wave modelers in linearized cosmology or black-hole perturbation theory cite the property to guarantee that the TT gauge is uniquely fixed by the metric data. The statement is introduced directly as a quantified proposition over the TensorPerturbation structure whose validity follows from structural equality after the equality hypothesis is substituted.
Claim. For all tensor perturbations $tp_1$ and $tp_2$, if their transverse-traceless components satisfy $h_{TT}(tp_1)=h_{TT}(tp_2)$ then $tp_1=tp_2$.
background
TensorPerturbation packages a map $h_{TT}:ℝ→(Fin 3→Fin 3→ℝ)$ together with two side conditions: transversality (the sum over one spatial index vanishes for each fixed time and remaining index) and tracelessness (the spatial trace vanishes at each time). These conditions are part of the standard decomposition of metric perturbations on an FRW background, drawing on the geometry module for the underlying spatial manifold and the FRWMetric module for the background line element.
proof idea
The declaration is a direct definition of the quantified statement. Its truth is established in the companion theorem decomposition_unique_holds by introducing the two perturbations, performing case analysis on both structures, simplifying the equality hypothesis on h_TT, substituting, and closing by reflexivity.
why it matters
The definition supplies the uniqueness claim that decomposition_unique_holds discharges. It anchors the tensor-mode sector of gravitational-wave analysis inside the Recognition framework, consistent with the three spatial dimensions forced by the eight-tick octave. No open scaffolding questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.