PeriodicConformalLogSubspace5
plain-language theorem explainer
Predicate marking which periodic edge-length perturbations at N=5 arise from a vertex conformal potential via endpoint-averaged log-strain, pulled back to typed Freudenthal edges. Gravity-track authors cite it when cutting the pure-shear complement out of the conformal slice. Membership is existential: some vertex potential reproduces the edge field after encoded-to-periodic transport.
Claim. An edge perturbation $\varepsilon$ on the typed periodic Freudenthal edges at $N=5$ lies in the conformal log-strain subspace if there exists a vertex potential $\xi$ on the underlying triangulation such that $\varepsilon$ equals the pullback of the first-order log-length strain induced by averaging $\xi$ at the two endpoints of each edge.
background
Track 1.D separates the weak-field metric sector into a vertex-conformal slice and an independent edge/shear complement. The conformal ansatz assigns one scalar potential per vertex and induces edge-length variations by averaging endpoint potentials; that scalar slice cannot represent pure shear, hence cannot cover transverse-traceless gravitational-wave modes by itself.
A vertex potential on a finite 3D triangulation is a real assignment to vertices. Its conformal edge log-strain is the edge field $(\xi_u+\xi_v)/2$. Periodic edge perturbations at $N=5$ are real functions on typed periodic Freudenthal edges; the encoded-to-periodic map pulls finite-triangulation edge fields back to that typed indexing. The triangulation parameter on the periodic torus is the bridge ratio $K=\varphi^{1/2}$.
proof idea
Definitional predicate, not a proved theorem. Membership means $\varepsilon$ lies in the image of the composite map that sends a vertex potential $\xi$ through conformal edge log-strain and then through the encoded-to-periodic transport. The body is a single existential equality; no tactics or lemmas discharge anything.
why it matters
This is the conformal slice against which pure shear is measured in Track 1.D. Downstream, the face rectangle shear is orthogonal to every member (endpoint averages telescope around the square), giving a concrete nonzero vector in the orthogonal complement inside the 875-dimensional edge space. The typed endpoint-form rewrite and the iff with the encoded conformal predicate feed the SevenGaps edge-tensor lemmas. Master-theorem handoff endpoints use it to state that the $N=5$ conformal slice has an explicit finite spanning family, and that TT modes are finite orthogonality to this slice plus a caller-supplied gauge slice. It is the definitional hinge separating conformal from shear before projectors are built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.