periodicTTGramHilbertLinearMap_isSymmetric5
plain-language theorem explainer
The finite transverse-traceless Gram operator, once transported to Mathlib's Hilbert-space wrapper on the five-periodic coefficient space, is symmetric (self-adjoint for the real inner product). Gravity analysts working the tensor/shear sector cite this to justify Fredholm/range arguments for TT loads. The proof reduces both sides of the inner-product identity via the Hilbert-coefficient equivalence and invokes the already-proved coefficient-space self-adjointness.
Claim. The linear map given by the finite TT Gram operator on the $L^2$ Hilbert wrapper of the five-periodic TT coefficient space is symmetric: for all coefficient vectors $x,y$ in that Hilbert space, $\langle Ax, y\rangle = \langle x, Ay\rangle$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity. The older conformal ansatz puts one scalar potential at each vertex and averages endpoints to get edge-length changes; that scalar slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations from vertex-conformal ones and builds a finite TT Gram operator on a five-periodic torus geometry.
The object here is that Gram operator after transport to Mathlib's WithLp 2 Hilbert wrapper on the raw TT coefficient function space. The linear equivalence periodicTTCoeffHilbertEquiv5 identifies the Hilbert wrapper with the bare coefficient space; the companion identity equates the Hilbert inner product with the coefficient-space normal-equation inner product. Upstream, the Gram operator is already known to be self-adjoint on the raw coefficient space (periodicTTNormalEquationGram_selfAdjoint5). Mathlib's LinearMap.IsSymmetric is the standard real self-adjointness predicate used by later range/Fredholm lemmas.
proof idea
Term-mode proof of LinearMap.IsSymmetric. Fix Hilbert vectors $x,y$. Unfold the transported Gram map (composition of the coefficient Gram map with the Hilbert equivalence and its inverse). After simp on comp_apply and LinearEquiv.coe_coe, rewrite each side of the desired inner-product equality by the identity that Hilbert inner products equal coefficient inner products under the equivalence. Both sides become instances of the coefficient-space normal-equation inner product, and the already-proved coefficient Gram self-adjointness finishes the argument.
why it matters
Self-adjointness of the transported finite TT Gram operator is the Hilbert-space input needed for the finite-dimensional range criterion. Downstream, periodicTTGramRangeCriterionData5_proved packages the Fredholm fact that a load orthogonal to the Gram kernel lies in the range of this self-adjoint operator; its proof builds a Hilbert load via the same equivalence and relies on symmetry established here.
In the broader Recognition gravity track this closes a scaffolding step toward treating pure shear and TT wave modes that the conformal (scalar) ansatz cannot reach. It does not yet touch continuum limits, continuum Lichnerowicz operators, or the forcing-chain landmarks (T5–T8), but it is the finite discrete self-adjointness lemma those continuum lifts will quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.