periodicConformalLogSubspace5_iff_encodedConformal
plain-language theorem explainer
On the N=5 periodic Freudenthal 3-torus, membership of a typed periodic edge perturbation in the vertex-conformal log-strain subspace is equivalent to the encoded edge map being conformal. Anyone moving shear witnesses between typed and encoded presentations cites this bridge. The proof is a two-sided constructor: unpack the witness potential and transport equality by funext across the mutually inverse edge encodings.
Claim. Let $c$ be a periodic edge perturbation on the $N=5$ Freudenthal 3-torus. Then $c$ lies in the typed conformal log-strain subspace if and only if its image under the canonical edge encoding is a conformal edge perturbation of the torus complex $K$ (i.e., arises as $(\xi_u+\xi_v)/2$ for some vertex potential $\xi$).
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector beyond the pure conformal ansatz. 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}$. That image is a proper linear subspace of the full edge-perturbation space.
On the concrete $5\times5\times5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal range has rank at most 125 and cannot fill the 875-dimensional edge space. Two coordinate presentations of the same edge data are in play: a typed periodic edge perturbation and an encoded edge perturbation of the complex $K$, related by mutually inverse reindexing maps along the canonical edge equivalence of the torus.
The conformal predicate itself is membership in the range of the linear map sending vertex potentials to edge log-strains. This lemma identifies the typed conformal subspace with that encoded predicate.
proof idea
Bidirectional constructor on the biconditional.
Forward: from a typed witness $\langle\xi,\mathrm{rfl}\rangle$, rebuild the encoded conformal certificate as $\langle\xi,_\rangle$ and discharge the pointwise equality by funext plus simp unfolding the two encoding maps (they cancel).
Reverse: from an encoded certificate $\langle\xi,h_\xi\rangle$, rebuild the typed witness as $\langle\xi,_\rangle$. Apply congrFun of $h_\xi$ at the inverse edge equivalence, then simpa with the same two encoding maps to recover the typed equality on every edge.
No external lemmas beyond the encoding definitions and function extensionality.
why it matters
The module's deliverable is an explicit shear complement to the conformal ansatz on the N=5 torus. Downstream, the encoded non-conformality theorems for the rectangle face shear and the uniform x-strain both reduce to their typed counterparts by applying the reverse direction of this equivalence (see rectangleShearFace5Encoded_not_conformal and xUniformStrain5Encoded_not_conformal).
Without the bridge, the typed obstruction (no vertex potential reproduces the +1/+1/-1/-1 square pattern, or the uniform x-strain) would not automatically yield the encoded IsConformalEdgePerturbation negation used by the rest of the edge-tensor sector. In the broader RS gravity lane this seals that the conformal slice is a proper subspace and that concrete tensor shear modes exist on the eight-tick-compatible 3-torus geometry (T7/T8 landmarks: period $2^3$, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.