periodicTTCoeffHilbertEquiv5
plain-language theorem explainer
Canonical real-linear equivalence identifying the L2 Hilbert wrapper of the finite TT coefficient space with the raw function space of coefficients on the normal-equation index set. Gravity-track proofs cite it to move the TT Gram operator and its inner product into Mathlib's finite Hilbert API without changing public coefficient data. It is the standard WithLp linear equivalence at p = 2.
Claim. There is a canonical $\mathbb{R}$-linear equivalence between the $L^2$ Hilbert-space wrapper of the finite transverse-traceless coefficient space and the raw coefficient space (real functions on the combined conformal-plus-longitudinal normal-equation index set).
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. Vertex scalars induce only averaged edge-length strains and cannot represent pure shear, so they miss transverse-traceless weak-field modes. This module isolates independent edge perturbations and sets up finite normal equations for conformal plus longitudinal pieces on a periodic 5-structure.
The raw coefficient space is the real function space on the finite normal-equation index set. The Hilbert wrapper is Mathlib's WithLp 2 packaging of that same finite-dimensional space, imported so that inner-product and range theorems apply without rewriting public TT data surfaces. The present abbreviation is the bridge between those two presentations.
proof idea
One-line definitional wrapper: apply Mathlib's WithLp.linearEquiv at $p=2$ over $\mathbb{R}$ to the raw coefficient space. No additional algebraic work; the equivalence is the standard forgetful/rewrap linear equivalence between a finite-dimensional real vector space and its $L^2$ Hilbert packaging.
why it matters
Downstream, the equivalence transports the TT Gram operator into the Hilbert wrapper, identifies the wrapper inner product with the coefficient-space dot product, and feeds the symmetry proof for the transported Gram map. It is also the conversion used in the finite TT Gram range/Fredholm criterion: a load orthogonal to the Gram kernel lies in the range of the self-adjoint Gram operator, stated as theorem-level data on the fixed finite model.
In the broader Recognition gravity scaffold this is infrastructure, not a forcing-chain step: it lets the shear/TT sector reuse Mathlib Hilbert facts while keeping coefficient surfaces as ordinary functions, supporting the program that pure shear (hence TT gravitational-wave content) sits outside the conformal vertex ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.