Pith. sign in
theorem

periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_finiteGeneratorData

proved
show as:
module
IndisputableMonolith.Gravity.TensorShearSector
domain
Gravity
line
1619 · github
papers citing
none yet

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.