PeriodicTTFiniteGeneratorProjectorData5
plain-language theorem explainer
Packages finite spanning generators and three projectors that split any periodic edge perturbation into conformal, gauge, and transverse-traceless parts on the Freudenthal torus. Gravity Track 1.D cites it as the concrete proof surface for the TT orthogonal decomposition. As a structure it is pure interface data: projectors, generators, span, orthogonality, and reconstruction axioms.
Claim. A finite-generator projector package on periodic edge perturbations consists of three maps $P_c$, $P_g$, $P_{\mathrm{TT}}$ and finite families $\{c_i\}_{i\in C}$, $\{g_j\}_{j\in G}$ such that: $P_c(\varepsilon)$ always lies in the vertex-conformal log-strain subspace; $P_g(\varepsilon)$ always lies in the image of a supplied gauge map; every conformal (resp. gauge) perturbation is a real linear combination of the $c_i$ (resp. $g_j$); $P_{\mathrm{TT}}(\varepsilon)$ is orthogonal to every generator under the periodic edge inner product; and $P_c(\varepsilon)+P_g(\varepsilon)+P_{\mathrm{TT}}(\varepsilon)=\varepsilon$ pointwise on edges.
background
Track 1.D isolates the tensor/shear sector that the Track 1.B vertex-conformal ansatz cannot reach. A periodic edge perturbation is simply a real function on the typed edges of the periodic Freudenthal torus. The conformal log-strain subspace consists of those edge fields induced by averaging a vertex scalar potential (endpoint log-strains). The gauge subspace is the image of a still-parametric forward gauge map from an abstract gauge-potential type, so the file does not fix a longitudinal/diffeomorphism discretization yet.
TT is defined relative to those two slices: residual orthogonal to both under the finite periodic-edge inner product. The module already records the elementary rectangle obstruction showing pure shear is not vertex-conformal. This structure is the next concrete interface: finite spanning families plus projectors whose TT residual is orthogonal to every generator, ready for Gram-kernel and handoff reductions.
proof idea
No proof body: this is a structure (definitional interface). Inhabitants must supply the three projectors, the two finite generator families, membership of the conformal and gauge projectors in their subspaces, spanning identities expressing every conformal/gauge field as a finite real combination of generators, orthogonality of the TT projector against every generator, and the pointwise reconstruction identity. Downstream constructors (e.g. ofGaugeGeneratorData) assemble instances from thinner generator packages.
why it matters
This is the central Track 1.D proof surface for closing the weak-field TT orthogonal decomposition on the periodic torus. Downstream, MasterTheoremHandoffIntegration treats possession of such data as the finite-generator projector reduction endpoint: it is enough to build full projector data and discharge the orthogonal-decomposition target consumed by Track 7. Related endpoints reduce further to gauge-only generators or generator-map data, then to Gram-kernel criteria and load-image solvers.
In the broader Recognition scaffold it separates pure shear (tensor) modes from the scalar conformal slice forced earlier, so gravitational-wave-type TT content can sit beside the D=3, eight-tick geometric backbone without being absorbed into vertex potentials. It does not yet choose the physical gauge discretization; it only freezes the finite-generator contract those choices must meet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.