periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_finiteGeneratorData
plain-language theorem explainer
Finite-generator projector data on the N=5 periodic Freudenthal torus already implies the honest conformal/gauge/TT orthogonal decomposition target. Gravity Track 1.D authors cite this when reducing the tensor-lane residual to three concrete projectors and finite spanning families. The proof is a one-line term wrapper: convert finite-generator data to plain projector data, then apply the existing projector-data closure.
Claim. Fix types of gauge potentials and finite index sets for conformal and gauge generators, together with a map sending each gauge potential to a real-valued edge perturbation on the typed periodic Freudenthal edges at $N=5$. If one is given finite-generator projector data (three projectors, finite conformal and gauge generator families, and the membership/orthogonality axioms that make the TT residual orthogonal to every generator), then the finite orthogonal decomposition target holds: every edge perturbation splits into conformal, gauge, and TT parts with the TT part orthogonal to both subspaces.
background
Track 1.D opens the tensor/shear sector that Track 1.B's vertex-conformal ansatz cannot reach. The conformal slice assigns one scalar potential per vertex and averages endpoints to edge-length variations; pure shear and transverse-traceless gravitational-wave modes lie outside that slice. This module therefore separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
Edge data live on the typed periodic Freudenthal edges at resolution $N=5$: a perturbation is simply a real function on those edges. The honest decomposition target asks for a raw splitting into conformal, gauge, and TT parts such that the conformal part lies in the periodic conformal-log subspace, the gauge part lies in the image of the chosen gauge map, and the TT part is orthogonal (in the finite inner-product sense) to both subspaces.
Finite-generator projector data is the concrete proof surface that closes that target: finite spanning families for the conformal and gauge slices, three projector maps, and axioms ensuring the TT residual is orthogonal to every generator. Spatial dimension $D=3$ (forced by T8/T9) underlies the ambient Freudenthal/Regge geometry but is not re-proved here.
proof idea
One-line term proof. First apply PeriodicTTProjectorData5.ofFiniteGeneratorData to the given finite-generator package, obtaining ordinary projector data (the three maps plus the membership and orthogonality obligations already packaged). Then feed that package into the existing closure lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_projectorData, which constructs the raw edge-perturbation splitting and discharges the three subspace membership goals. No new algebraic identities are proved at this layer.
why it matters
This is the reduction step that turns the abstract Track 1.D orthogonal-decomposition target into a finite, checkable generator-and-projector obligation. Downstream, the Master Theorem handoff consumes it as the finite-generator projector-data reduction endpoint for Track 7: once finite-generator data exist, the endpoint holds by packaging the converted projector data. The sibling gauge-generator theorem is a further specialization that fixes the conformal generators (already known to span) and only varies the gauge family, calling this result directly.
In the broader Recognition gravity program, the conformal ansatz alone cannot cover TT gravitational-wave modes; closing the finite $N=5$ conformal/gauge/TT split is the tensor-lane prerequisite before reconstruction and continuum comparison. The remaining open work named in the doc-comment is concrete rather than foundational: produce the generators, solve the projector system, and prove reconstruction. Framework landmarks $D=3$ and the eight-tick/Clifford scaffolding sit upstream in the geometry, not in this reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.