periodicTTGramHilbertLinearMap5
plain-language theorem explainer
Transports the finite transverse-traceless Gram operator from raw TT coefficient space to Mathlib's WithLp-2 Hilbert wrapper on the 5-periodic torus. Gravity analysts cite it when they need self-adjointness or range criteria in Hilbert language. The definition is the standard conjugation of the coefficient-space Gram map by the linear equivalence to the Hilbert wrapper.
Claim. Define the real-linear endomorphism of the $\ell^2$ Hilbert wrapper of the finite periodic TT coefficient space by conjugating the coefficient-space TT Gram map with the canonical linear equivalence between the wrapper and the raw coefficient functions: $H \xrightarrow{\simeq} C \xrightarrow{G_{\mathrm{TT}}} C \xrightarrow{\simeq} H$.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge analysis. The conformal (vertex-scalar) ansatz cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes; this module isolates independent edge perturbations and the elementary rectangle obstruction.
The finite TT data live as coefficient functions on the 5-periodic torus. For Mathlib's inner-product and range theorems one wraps that space as WithLp 2, written here as the periodic TT coefficient Hilbert space. The raw coefficient type stays the public surface elsewhere; the wrapper is only a transport layer.
Upstream, a coefficient-space TT Gram linear map already acts on the raw functions. A linear equivalence identifies the Hilbert wrapper with that function space, so operators can be moved back and forth without changing the geometric content.
proof idea
Pure definition by linear-map composition. Push a Hilbert vector to coefficient space via the equivalence, apply the existing coefficient-space TT Gram map, then pull back by the inverse equivalence. No algebraic identity is proved here; the body is exactly that conjugation.
why it matters
Gives the Hilbert-side presentation of the finite TT Gram operator needed for Mathlib self-adjointness and Fredholm-range arguments. Downstream, symmetry of this transported map is proved, and the fixed finite TT Gram range criterion is discharged: a load orthogonal to the Gram kernel lies in the range of the self-adjoint Gram operator.
In the Recognition gravity track this is scaffolding for the shear/TT sector beyond the conformal ansatz, toward genuine weak-field tensor modes on the periodic Regge complex. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is linear-algebra infrastructure inside the gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.