PeriodicTTCoeffHilbertSpace5
plain-language theorem explainer
Finite TT coefficient vectors on the period-5 torus are packaged as an L2 Hilbert space via Mathlib's WithLp wrapper. Gravity workers cite it when moving Gram-range and Fredholm arguments onto standard inner-product machinery without changing the public coefficient API. The body is a one-line type synonym.
Claim. Write $\mathrm{PeriodicTTCoeffHilbertSpace}_5$ for the space of period-5 transverse-traceless coefficient vectors equipped with the $\ell^2$ (WithLp 2) Hilbert structure on the underlying finite real function space of coefficients.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge model. Track 1.B's conformal ansatz puts one scalar at each vertex and averages to edges; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction.
The raw TT coefficient type remains an ordinary finite function space so that public data surfaces stay elementary. Mathlib's range and self-adjoint theorems for finite-dimensional operators, however, expect an $L^p$ Hilbert wrapper. WithLp 2 supplies exactly that structure on the same underlying vector space: the $\ell^2$ inner product and the associated norm topology, with no change to coefficient indexing on the period-5 torus.
Upstream geometry (periodic Freudenthal torus, Regge first variation, hinge-aware zero modes) fixes the discrete TT basis whose coefficients this space holds. The wrapper is only a presentation change for analysis.
proof idea
One-line abbreviation: the Hilbert space is defined to be Mathlib's WithLp 2 applied to the raw finite TT coefficient function space. No proof obligations; the synonym inherits the inner-product space instance from Mathlib.
why it matters
This type is the carrier for the finite TT Gram analysis on the period-5 torus. Downstream, the linear equivalence to the raw coefficient space transports the Gram operator onto the Hilbert wrapper, and the proved range/Fredholm criterion uses that wrapper so a load orthogonal to the Gram kernel lies in the operator range (finite-dimensional self-adjoint fact).
In the Recognition gravity track this is scaffolding for the shear sector that conformal vertex potentials cannot reach: pure TT edge modes needed for weak-field waves. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is local linear-algebra infrastructure so later continuum or census limits can quote Mathlib Hilbert theorems cleanly while keeping public TT data as plain functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.