PeriodicTTCoeffSpace5
plain-language theorem explainer
Defines the real coefficient-vector space for the combined conformal and longitudinal normal equations on the five-cell periodic TT sector: maps from the normal-equation index set into the reals. Gravity and Regge analysts cite it as the raw domain for Gram operators, coefficient inner products, and the L2 Hilbert wrapper. The body is a one-line type abbreviation.
Claim. Write $V$ for the finite index set of the combined conformal-plus-longitudinal normal equations on the five-cell periodic transverse-traceless sector. The coefficient space is the real function space $V \to \mathbb{R}$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity in the Recognition scaffold. Track 1.B's conformal ansatz puts one scalar potential at each vertex and averages endpoints to get edge-length changes; 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 for the conformal ansatz.
On the five-cell periodic torus geometry, the TT normal equations mix conformal and longitudinal constraints. Their discrete index set labels the free coefficients of those equations. The present abbreviation is simply the real vector space of all assignments of those coefficients: functions from that index set into $\mathbb{R}$. Downstream, Mathlib's WithLp 2 wrapper turns the same carrier into a finite-dimensional Hilbert space without changing the public TT data surfaces.
proof idea
Definitional abbreviation only: the carrier is identified with the function type from the combined normal-equation index set into the reals. No lemmas or tactics are invoked.
why it matters
This type is the raw domain for the entire coefficient-level TT linear algebra in the file. It feeds the $L^2$ Hilbert wrapper, the linear equivalence between wrapper and raw functions, the Gram operator as a linear map on coefficient functions, the identification of the Hilbert inner product with the coefficient dot product, and the symmetry of that dot product.
In the broader Recognition gravity track, the construction is the discrete home for shear degrees of freedom that the pure conformal ansatz cannot reach. It sits under the Regge/TT hinge analysis and the seven-gaps continuum-smearing program: once Gram operators and normal equations live on this space, one can ask which coefficient modes are pure shear versus longitudinal or conformal, and whether the discrete TT sector reproduces continuum transverse-traceless waves on the forced $D=3$ geometry and eight-tick register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.