periodicTTGramLinearMap5
plain-language theorem explainer
Packages the finite TT Gram operator (combined conformal plus longitudinal generators on the 5-periodic torus) as an ℝ-linear endomorphism of raw coefficient functions. Gravity/Regge workers cite it when moving from pointwise Gram evaluation to Mathlib linear-map and Hilbert-space APIs. Linearity is checked by distributing sums and scalars through the Gram double sum.
Claim. On the finite coefficient space of the combined conformal-plus-longitudinal normal equations for the 5-periodic TT sector, the map sending a coefficient vector $c$ to the Gram vector whose $i$-th entry is $\sum_j c_j\,\langle g_j,g_i\rangle$ is an $\mathbb{R}$-linear endomorphism of that space.
background
Track 1.D separates pure edge shear from the Track 1.B vertex-conformal ansatz. The conformal slice cannot represent transverse-traceless gravitational-wave modes; this module builds the tensor/shear normal equations on a periodic Freudenthal torus.
Coefficient space is the finite type of real functions on the combined conformal-plus-longitudinal index set. The Gram apply sends coefficients $c$ to $\sum_j c_j$ times the periodic edge inner product of generators $j$ and the output index. The Gram vector is that apply, reified as a coefficient function.
The present declaration only promotes that vector-valued Gram action to a Mathlib LinearMap on the raw function space, before the WithLp 2 Hilbert wrapper is attached.
proof idea
Definitional packaging: toFun is the already-defined Gram vector. Additivity: after funext on the output index, unfold Gram vector and Gram apply, then simp with pointwise addition, add_mul, and Finset.sum_add_distrib. Homogeneity: same unfold, rewrite scalar through the finite sum via Finset.mul_sum, then ring on each summand. No external lemmas beyond Pi/Finset arithmetic.
why it matters
Bridge from combinatorial Gram data to operator language inside the tensor/shear scaffold. Downstream, the Hilbert-transported Gram map is this map conjugated by the coefficient Hilbert equivalence; symmetry of that Hilbert operator and the proved finite TT Gram range/Fredholm criterion (loads orthogonal to the kernel lie in the range) both depend on having a genuine linear map. In the broader RS gravity track this is scaffolding for weak-field TT modes beyond the conformal potential, not yet a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.