periodicConformalLogSubspace5_endpoint_form
plain-language theorem explainer
Any edge perturbation on the 5×5×5 periodic torus that lies in the conformal log-strain subspace is realized by endpoint averaging of a single real vertex potential. Gravity and discrete-geometry workers cite it when converting the abstract conformal membership predicate into concrete endpoint formulas. The proof unpacks the subspace witness and transports the encoded conformal strain across the typed edge/vertex equivalences.
Claim. Let $c$ be a real-valued edge perturbation on the $5\times 5\times 5$ periodic Freudenthal 3-torus. If $c$ belongs to the conformal log-strain subspace, then there exists a vertex potential $\varphi$ on the typed torus vertices such that for every edge $e$ with endpoints $u,v$, one has $c(e)=(\varphi(u)+\varphi(v))/2$.
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector of Regge-type data on the concrete $N=5$ periodic Freudenthal 3-torus. The vertex-conformal ansatz assigns one real scalar $\xi$ per vertex and induces the log-strain $(\xi(u)+\xi(v))/2$ on each edge ${u,v}$ (the map packaged as conformalEdgeLogStrain / conformalStrainLinearMap in the imported TensorShearSector module).
On this torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image is a proper subspace of the full edge-perturbation space. Membership in that image is recorded by the predicate PeriodicConformalLogSubspace5: $c$ is the image, under the canonical encoded-to-typed edge map, of a conformal log-strain built from some encoded vertex potential.
The present statement rewrites that membership in purely typed coordinates: the same $c$ is the endpoint average of a typed vertex potential $\varphi:V\to\mathbb{R}$. The rewrite uses the periodic edge/vertex equivalences and the identity that the encoded edge's two vertices match the typed edge's endpoints.
proof idea
Term-mode unpacking of the subspace witness. From hc : PeriodicConformalLogSubspace5 c one obtains an encoded potential $\xi$ with $c$ definitionally equal to the encoded conformal strain of $\xi$. The typed potential is $\varphi(v)=\xi(\mathrm{symm},v)$ under the periodic vertex equivalence. After unfolding the encoded-to-typed edge map and conformalEdgeLogStrain, a single rewrite periodicTorus5_edgeVerts_symm_eq_endpoints identifies the two encoded vertices of each edge with the typed endpoints, yielding $c(e)=(\varphi(u)+\varphi(v))/2$ pointwise.
why it matters
This is the bridge from the abstract conformal-subspace predicate to the concrete endpoint arithmetic used throughout the shear analysis. Downstream, rectangleShearFace5_inner_conformal_eq_zero invokes it so that the face-shear inner product against any conformal $c$ becomes a four-term telescope $(\varphi_A+\varphi_B)+(\varphi_D+\varphi_C)-(\varphi_B+\varphi_C)-(\varphi_A+\varphi_D)=0$, proving orthogonality of the explicit shear witness to the whole conformal slice. Likewise xUniformStrain5_not_conformal_typed instantiates the four endpoint averages on the unit square, reads off horizontal strain $1$ and vertical strain $0$, and applies the rectangle obstruction to conclude non-conformality.
In the broader Recognition gravity stack this supports the claim that the edge-tensor sector is strictly larger than the conformal ansatz on the eight-tick / $D=3$ Freudenthal lattice (T7–T8 landmarks), supplying the dimension gap and explicit shear complement needed for the Seven-Gaps lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.