periodicTTOperatorBilinear5
plain-language theorem explainer
Defines the real bilinear form pairing two periodic edge perturbations through an arbitrary edge-space operator: the left argument is dotted against the operator applied to the right, via the finite periodic-edge inner product. Anyone comparing Regge TT Hessians to lattice Lichnerowicz operators on the five-cell torus cites this as the common energy surface. The body is a one-line abbreviation of that pairing.
Claim. For an operator $T$ on real-valued perturbations of the typed periodic Freudenthal edges, and for edge perturbations $\varepsilon,\eta$, set $B_T(\varepsilon,\eta) := \langle \varepsilon,\, T\eta \rangle_5$, where $\langle\cdot,\cdot\rangle_5$ is the finite periodic-edge inner product.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the periodic Freudenthal triangulation. The conformal (vertex-scalar) ansatz of Track 1.B cannot carry pure shear, so independent edge-length perturbations are needed for transverse-traceless modes.
A periodic edge perturbation is simply a real function on the typed periodic edges (PeriodicEdge5 → ℝ). The companion inner product periodicEdgeInnerProduct5 is the finite $\ell^2$ pairing on that edge space. Given any linear (or merely set-theoretic) operator on edge perturbations, the natural energy pairing is the inner product of the first field against the image of the second.
This is the concrete matrix surface on which the Regge TT Hessian stencil and the lattice Lichnerowicz stencil are compared pointwise on TT modes.
proof idea
Pure definitional abbreviation: the bilinear form is declared equal to periodicEdgeInnerProduct5 ε (op η). No lemmas are invoked; the body is a single application of the already-defined finite periodic-edge inner product to the left field and the operator image of the right field.
why it matters
This pairing is the common language for every Track 1.D Hessian–Lichnerowicz comparison. Downstream, periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5 states that operator equality on longitudinal TT modes implies equality of the two bilinears; coefficient-certificate variants (origin-column, translated, relative-translated) reduce to the same surface. Quadratic TT energy identities are the diagonal case $\varepsilon=\eta$.
The master handoff endpoint Track1DTTHessianLichnerowiczBilinearReductionEndpoint is literally the universal quantification of this equality for matched Regge and lattice operators. In the broader RS gravity program it is the finite-edge avatar of the second-variation energy that must match continuum Lichnerowicz theory once the eight-tick / $D=3$ lattice is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.