projection_operator_TT
plain-language theorem explainer
The declaration defines the proposition asserting existence of a projection operator P that extracts the transverse-traceless component of a metric perturbation at initial time in three spatial dimensions. Gravitational wave modelers in the Recognition Science setting would cite it to guarantee that tensor modes can be isolated from arbitrary h inputs. The definition is realized directly as an existential statement over maps from 3x3 real matrices to the h_TT field of a TensorPerturbation structure.
Claim. There exists a map $P: (Fin 3 → Fin 3 → ℝ) → (Fin 3 → Fin 3 → ℝ)$ such that for every input $h$ there exists a TensorPerturbation $tp$ satisfying $P(h) = tp.h_{TT}(0)$, where TensorPerturbation requires $h_{TT}$ to obey the transverse and traceless conditions.
background
The TensorDecomposition module works in the linearized gravity sector on a flat or FRW background. Its central structure TensorPerturbation packages a time-dependent spatial tensor $h_{TT}: ℝ → (Fin 3 → Fin 3 → ℝ)$ together with the two algebraic constraints: transverse (row sums vanish) and traceless (trace vanishes). These conditions select the two physical degrees of freedom of a gravitational wave in three spatial dimensions, the number forced by the eight-tick octave in the UnifiedForcingChain. Upstream structures supply the surrounding Recognition Science scaffolding: PhiForcingDerived encodes the convex J-cost whose minimum at unity underpins uniqueness of decompositions, while SpectralEmergence fixes the gauge content and DAlembert.LedgerFactorization calibrates the underlying J functional.
proof idea
The declaration is a pure definition whose body is the existential quantifier itself. No tactics or lemmas are invoked; it simply asserts that some map P recovers the zero-time slice of an instance of TensorPerturbation. The surrounding module imports supply the Fin 3 indexing and the TensorPerturbation record, but the definition performs no reduction or application of upstream results.
why it matters
This definition supplies the existence interface needed for any subsequent uniqueness statement (decomposition_unique) in the same module, thereby anchoring the gravitational-wave sector to the three-dimensional spatial structure required by T8. It sits downstream of the ledger-factorization and phi-forcing machinery that guarantee convexity of J, yet currently has no recorded downstream uses. The declaration therefore closes a scaffolding gap between the abstract forcing chain and concrete tensor-mode extraction, leaving open the question of an explicit coordinate formula for P.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.