PeriodicRelativeTTGeneratorOrthogonalOnTT5
plain-language theorem explainer
Names the shifted-generator orthogonality property on the five-periodic torus: every longitudinal TT edge perturbation is orthogonal, under the periodic edge inner product, to every row-frame translate of the combined conformal/longitudinal normal-equation generator. Downstream Hessian residual-kernel packs cite this Prop as a required field. Bare definition of a Prop, not a proved lemma.
Claim. For every edge perturbation $\varepsilon$ lying in the longitudinal transverse-traceless subspace on the five-periodic torus, and for every edge row and every real coefficient assignment on the TT normal-equation indices, the periodic edge inner product of $\varepsilon$ against the relative-frame normal-equation generator map at that row and coefficient is zero.
background
Track 1.D isolates pure shear (independent edge-length changes) from the Track 1.B vertex-conformal ansatz. The conformal slice cannot represent transverse-traceless gravitational-wave modes, so the tensor/shear sector needs its own generators and inner-product identities on the discrete geometry.
The five-periodic torus is the working lattice. Edge perturbations carry a periodic edge inner product. The relative-frame route packages conformal and longitudinal-gauge directions into a single normal-equation generator map, then translates that map along edge rows. Genuine TT modes must be orthogonal to every such translate before residual-kernel arguments can fire.
The module already shows that nontrivial rectangle shear need not be vertex-conformal, so the tensor sector is nonempty. This Prop records the remaining generator-orthogonality obligation on that sector.
proof idea
No proof body: the declaration is a Prop definition. It universally quantifies over longitudinal TT edge perturbations $\varepsilon$, edge rows, and coefficient maps, and asserts that the periodic edge inner product of $\varepsilon$ against the relative-frame normal-equation generator at that row vanishes. A later theorem must discharge the identity, typically by splitting each row-frame translate back into the fixed conformal and longitudinal-gauge images and using TT orthogonality to each summand.
why it matters
Required field of EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5. That structure's doc states that relative-frame translated data plus this shifted-generator orthogonality "is enough to prove the residual kernel vanishes on TT perturbations," and that "the separate orthogonality field is the exact mathematical gap left by the Regge Schläfli candidate diagnostics."
Closing the Prop completes the relative-frame route to a discrete Lichnerowicz-type residual statement in the tensor/shear sector, the piece the pure conformal ansatz cannot supply for weak-field TT modes on the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.