PeriodicTTOrthogonal5
plain-language theorem explainer
Defines the finite-N=5 transverse-traceless condition on periodic edge perturbations: orthogonality, under the discrete edge inner product, to both the vertex-conformal log-strain slice and a caller-supplied gauge slice. Gravity Track 1.D cites it as the working TT predicate before projectors exist. The body is a two-conjunct Prop, not a proved statement.
Claim. Fix a gauge-potential type $G$ and a linear gauge map $\mathrm{gauge}: G \to (\mathrm{PeriodicEdge}_5 \to \mathbb{R})$. An edge perturbation $\varepsilon$ is TT-orthogonal when $\langle \varepsilon, c \rangle_5 = 0$ for every $c$ in the periodic conformal log-strain subspace, and $\langle \varepsilon, g \rangle_5 = 0$ for every $g$ in the image of $\mathrm{gauge}$, where $\langle \cdot, \cdot \rangle_5$ is the finite sum $\sum_e \varepsilon(e)\,\eta(e)$ over typed periodic Freudenthal edges.
background
Track 1.D opens the tensor/shear sector that Track 1.B's conformal ansatz cannot reach. The conformal ansatz puts one scalar potential at each vertex and induces edge-length changes by averaging endpoints; that scalar slice misses pure shear and therefore cannot carry transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones on the periodic Freudenthal torus at $N=5$.
Edge data live in $\mathrm{PeriodicEdge}_5 \to \mathbb{R}$. The conformal log subspace consists of those edge fields that arise as encoded conformal edge log-strains of some vertex potential. The gauge subspace is not fixed in this file: it is the image of a parameter map $\mathrm{gaugeMap}$, so the longitudinal/diffeomorphism discretization stays open. Orthogonality uses the plain finite inner product $\sum_e \varepsilon(e),\eta(e)$.
proof idea
Definitional, not a proof. The predicate is the conjunction of two universal statements: (i) vanishing inner product against every edge field in the periodic conformal log-strain subspace; (ii) vanishing inner product against every edge field in the supplied gauge image. Both conjuncts quantify over $\mathrm{PeriodicEdgePerturbation}_5$ and discharge via the subspace membership Props already defined upstream. No tactics or lemmas fire at this declaration.
why it matters
This is the working meaning of TT in the finite periodic setting before any projector is constructed. Downstream, the honest decomposition target requires a splitting whose third summand satisfies this predicate for every input edge field; the master-theorem handoff endpoint packages the zero field as TT-orthogonal and reduces the full TT decomposition target to that orthogonal splitting. A concrete longitudinal specialization freezes the gauge map and reuses the same Prop as the longitudinal TT subspace; generator-orthogonality lemmas then promote finite spanning checks to full TT membership. In the RS gravity track this is the discrete stand-in for the continuum TT gauge condition that isolates shear/GW content from conformal and diffeomorphism junk on the eight-tick / $D=3$ lattice side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.