periodicTTNormalEquationResidual5
plain-language theorem explainer
Defines the residual edge perturbation after removing the span of conformal vertex-delta and longitudinal gauge generators under a combined coefficient projector on the finite periodic Freudenthal torus. Gravity analysts working the TT/shear split cite it as the concrete remainder that should be orthogonal to those generators. The body is a thin adapter that splits the combined projector and hands both halves to the existing longitudinal residual.
Claim. Given a coefficient map $P$ from edge perturbations on the typed periodic Freudenthal edges to real coefficients indexed by the combined normal-equation index (conformal vertex indices plus longitudinal gauge indices), and an edge perturbation $\varepsilon$, the residual is the edge field obtained by subtracting the conformal and longitudinal reconstructions determined by $P(\varepsilon)$ from $\varepsilon$.
background
Track 1.D isolates the tensor/shear sector of weak-field edge-length variations on a finite periodic Freudenthal triangulation. The conformal ansatz of Track 1.B only averages vertex potentials onto edges, so it cannot carry pure shear or transverse-traceless modes. Edge perturbations here are real functions on the typed periodic edges PeriodicEdge5.
The combined normal-equation index is a sum type: conformal generators labeled by vertices of the periodic torus cell, plus fixed longitudinal vertex-vector (gauge) generators. A coefficient projector assigns one real coefficient to each such generator for a given edge field.
Upstream, periodicLongitudinalCoefficientResidual5 already forms the residual after subtracting conformal and longitudinal projections separately. The present definition packages those two projectors as the two summands of a single combined projector, matching the finite linear-algebra problem left by the TT decomposition track.
proof idea
Definitional wrapper, not a proof. It feeds periodicLongitudinalCoefficientResidual5 two curried projectors extracted from the combined map: conformal coefficients via periodicTTNormalEquationConformalCoeff5 (coeffProjector ε) and gauge coefficients via periodicTTNormalEquationGaugeCoeff5 (coeffProjector ε), then applies that residual to the same edge field $\varepsilon$. No algebraic identity is proved at this site; equalities live in the sibling theorems that unfold the residual.
why it matters
This residual is the TT remainder in the finite normal-equation split: after conformal and longitudinal pieces are removed, what is left is the candidate shear/TT component. Downstream, PeriodicTTLongitudinalCoefficientSolutionData5 states the coefficient solve with no separate TT projector, taking the residual as the TT part. PeriodicTTNormalEquationSolutionData5 packages the single-system normal equations for the concrete finite TT split.
Sibling theorems pin the algebra: the residual equals input minus the combined generator-map reconstruction, and its inner product against any generator equals load minus Gram. That is the discrete normal-equation identity needed before claiming orthogonality or uniqueness of the TT projection on the periodic cell. In the broader Recognition gravity track it is scaffolding for covering modes the pure conformal ansatz cannot reach, not a continuum GR theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.