PeriodicGaugeSubspace5
plain-language theorem explainer
An edge perturbation on the N=5 periodic Freudenthal torus lies in the gauge subspace exactly when it is the image of some abstract gauge potential under a caller-supplied forward gauge map. Track 1.D authors cite this to keep the longitudinal/diffeomorphism discretization parametric while stating TT orthogonality and decomposition targets. The body is a one-line existential: membership means being in the image of that map.
Claim. Fix a type of gauge potentials and a forward map from potentials to real-valued edge perturbations on the typed periodic Freudenthal edges at $N=5$. An edge perturbation $\varepsilon$ lies in the associated gauge subspace if and only if there exists a potential $A$ with $\varepsilon$ equal to the image of $A$ under that map.
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 per vertex and averages endpoints onto edges; pure shear and transverse-traceless gravitational-wave modes sit outside that slice. This module therefore treats independent edge perturbations as the ambient space and separates conformal, gauge, and TT pieces.
PeriodicEdgePerturbation5 is simply a real function on the typed periodic Freudenthal edges at period parameter 5. The gauge slice is not hard-coded: a type of potentials and a forward operator into edge perturbations remain parameters, so the file does not yet commit to a particular longitudinal or diffeomorphism discretization.
Downstream TT language means finite orthogonality, with respect to the periodic-edge inner product, to both the conformal log-strain subspace and this supplied gauge image.
proof idea
Pure definition, not a proved theorem. The predicate is the standard image membership statement: there exists a gauge potential whose image under the supplied forward map equals the given edge perturbation. No lemmas are applied; the body is the existential equation that later spanning and projector lemmas unfold.
why it matters
This is the parametric gauge half of the Track 1.D TT package. The honest decomposition target PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 requires every edge field to split into a conformal part, a part in this gauge subspace, and a TT residual orthogonal to both. The handoff endpoint Track1DTTOrthogonalSurfaceEndpoint packages the same idea for the master theorem surface: TT is finite orthogonality to the conformal slice and a caller-supplied gauge slice, with actual projectors still to build.
Sibling lemmas show that when the map is a finite generator map (or the concrete longitudinal vertex-vector map), membership implies an explicit linear combination of those generators. Projector data structures then take this subspace as the gauge factor whose residual must be killed. In the broader RS gravity track this is scaffolding toward a weak-field shear/TT sector on the eight-tick, D=3 discrete geometry, not yet a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.