periodicConformalLogSubspace5_spanned_by_encodedVertexGenerators
plain-language theorem explainer
Any periodic edge perturbation on the 5×5×5 Freudenthal torus that lies in the vertex-conformal log-strain subspace is a linear combination of the encoded vertex delta generators, with coefficients given by the underlying vertex potential. Gravity workers building the Track 1.D TT projector cite this for the conformal half of the finite-generator data. The proof unpacks the subspace witness and reduces by ring simplification.
Claim. Let $c$ be a real-valued perturbation of the edges of the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. If $c$ lies in the periodic conformal log-strain subspace (i.e., $c$ is the edgewise conformal log-strain of some vertex potential $\xi$), then there exist real coefficients $(\mathrm{coeff}_v)$, one per torus vertex, such that for every edge $e$, $c(e)=\sum_v \mathrm{coeff}_v\, g_v(e)$, where $g_v$ is the encoded conformal generator attached to vertex $v$.
background
Track 1.D separates pure shear (tensor) edge perturbations from the older Track 1.B conformal ansatz. The conformal ansatz assigns one scalar potential to each vertex and induces edge-length variations by averaging endpoint potentials; that scalar slice cannot represent pure shear, so it cannot cover transverse-traceless gravitational-wave modes by itself.
PeriodicTorus5 is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. A PeriodicEdgePerturbation5 is simply a real function on its typed edges. The predicate PeriodicConformalLogSubspace5 c asserts that $c$ equals the image of some vertex potential $\xi$ under the composition of conformal edge log-strain with the encoding map into periodic edge perturbations.
The generators in the conclusion are the images of the standard delta potentials at each vertex under that same conformal-log-strain encoding. The claim is that those finitely many generators already span the whole conformal log subspace.
proof idea
Term-mode proof. Destructure the subspace hypothesis to obtain a vertex potential $\xi$ with $c$ definitionally equal to the encoded conformal log-strain of $\xi$. Take the coefficient vector to be $\xi$ itself. For an arbitrary edge, unfold the definitions of the encoded vertex generators, the delta potentials, the encoding map, and conformal edge log-strain. The resulting finite-sum identity is discharged by simp with the ring lemmas Finset.mul_sum, Finset.sum_add_distrib, div_eq_mul_inv, mul_add, mul_assoc, and mul_comm. No external geometric lemma is required beyond definitional expansion.
why it matters
This theorem supplies the conformal half of the finite-generator TT projector data on the $N=5$ torus. Downstream, PeriodicTTFiniteGeneratorProjectorData5 packages conformal and gauge spanning families together with projectors whose TT residual is orthogonal to every generator; the conformal span clause is exactly this result. The master-handoff theorem track1D_conformal_generator_span_endpoint_holds is a one-line alias of the present statement, consumed by Track 7 as the conformal-generator span endpoint.
In the broader Recognition scaffold, Track 1.B already forced the vertex-scalar conformal slice; Track 1.D must still isolate the shear complement so that transverse-traceless modes are reachable. Fixing a concrete finite spanning set for the conformal log subspace is the first half of that projector construction. The gauge (longitudinal/diffeomorphism) half remains a parameter: the file does not yet choose a discretization of the gauge operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.