PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
plain-language theorem explainer
Defines the Track 1.D target proposition for a finite N=5 periodic Freudenthal edge-space split into conformal, gauge, and TT parts, with TT meaning finite orthogonality to the other two subspaces. Gravity and Regge analysts cite it as the honest decomposition goal once a gauge map is fixed. The body is a pure Prop packing: existence of a raw splitting whose three component maps land in the named subspaces for every edge perturbation.
Claim. For a type of gauge potentials and a map sending each potential to a real-valued perturbation on the typed periodic Freudenthal edges at $N=5$, the target asserts: there exists a raw edge-perturbation splitting such that, for every edge field $\varepsilon$, the conformal component lies in the periodic conformal-log subspace, the gauge component lies in the image subspace of the given gauge map, and the TT component is finitely orthogonal to both the conformal and gauge subspaces.
background
Track 1.D opens the tensor/shear sector that Track 1.B cannot reach. The conformal ansatz assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that scalar slice misses pure shear and therefore cannot carry transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
Edge fields live on the typed periodic Freudenthal edges at finite $N=5$: a perturbation is simply a real function on those edges. The decomposition language is a raw three-way split (conformal part, gauge part, TT part) together with subspace membership predicates: conformal-log membership, gauge-image membership relative to a chosen gauge map, and finite TT orthogonality to the conformal and gauge subspaces. Upstream 4D edge TT analysis already uses a gauge-part bilinear form $m_i v_j+v_i m_j$; the present target is the finite periodic analogue of that split, not a continuum Lichnerowicz projector.
proof idea
Definitional, not a proved theorem. The right-hand side is an existential Prop: a raw edge-perturbation splitting on the $N=5$ periodic edge type, plus three universal membership statements (conformal-log subspace, gauge subspace for the supplied gauge map, and finite TT orthogonality). No lemmas are applied; the declaration only packages the target that later projector-construction data must discharge.
why it matters
This is the honest Track 1.D decomposition goal: TT means finite orthogonality to conformal and gauge subspaces, and the remaining load is constructing the three projectors with membership and pointwise reconstruction. Downstream MasterTheorem handoff endpoints all reduce concrete finite data to closing this target: finite spanning-generator projector data, gauge-generator projector data after the conformal span is fixed, generator-map data that makes the gauge span automatic, and the Gram-kernel / Gram-load-image / Gram-solver chain that produces projector data and closes the TT split. In the Recognition gravity lane it is the finite $N=5$ stand-in for the classical conformal/gauge/TT decomposition of weak-field metric perturbations, needed before shear modes can feed the larger forcing and continuum handoff story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.