PeriodicFreudenthalTTDecompositionTargetAtN5
plain-language theorem explainer
Packages the Track 1.D goal that every periodic edge perturbation on the N=5 Freudenthal torus splits into conformal, gauge, and transverse-traceless parts under three caller-supplied predicates. Gravity and Regge analysts cite it as the finite-edge TT decomposition interface. It is a pure existential Prop over a raw edge splitting, not a proved existence theorem.
Claim. Fix three predicates $C$, $G$, and $T$ on real-valued edge perturbations of the period-$5$ Freudenthal torus. The target asserts: there exists a raw splitting of every edge perturbation $\varepsilon$ into conformal, gauge, and TT summands such that the conformal summand always satisfies $C$, the gauge summand always satisfies $G$, and the TT summand always satisfies $T$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B only assigns a scalar potential at each vertex and averages endpoints to get edge-length changes; that conformal slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes.
Here edge data live on the typed period-5 Freudenthal torus: a perturbation is simply a real function on those edges. The raw splitting type factors any such function into three named parts (conformal/trace, gauge/longitudinal, TT). Upstream 4D edge TT analysis already defines a gauge part of the form $m_i v_j + v_i m_j$; the periodic setting lifts the same trichotomy to the finite triangulation.
The three predicates are intentionally parameters. Callers must instantiate them with the actual periodic Freudenthal conformal, gauge, and TT operators rather than with ad-hoc props.
proof idea
No proof: the declaration is a definitional abbreviation of an existential proposition. The body is the raw statement that some RawEdgePerturbationSplitting on the period-5 edge type has conformal, gauge, and TT parts lying in the three supplied predicates for every edge perturbation. Downstream lemmas discharge or transport this Prop; nothing is proved at this site.
why it matters
This is the concrete next target for Track 1.D after Session 215: a finite, checkable interface for TT decomposition on the periodic Freudenthal complex. The handoff surface Track1DTTOrthogonalSurfaceEndpoint ends by requiring that an orthogonal decomposition target imply this target, with TT represented as finite orthogonality to the periodic conformal slice and a caller-supplied gauge slice. The bridge theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_to_target already shows that the orthogonal formulation implies this Prop when the conformal and gauge predicates are the standard periodic subspaces.
In the broader Recognition gravity program, the split separates the scalar conformal ansatz from genuine shear so that eight-tick, D=3 geometric structure can eventually host TT wave modes. Constructing the actual projectors remains the open tensor-sector step; this definition only names the landing Prop those projectors must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.