toPotential
plain-language theorem explainer
Maps a real-valued field on the periodic cubic lattice vertices to the triangulation's finite-index vertex potential by pullback along the canonical Fin equivalence. Gravity stencil and Hessian identities cite it whenever vertex data must enter Regge quadratic forms. The body is a one-line composition with the vertex indexing equivalence.
Claim. Given a real field $u$ on the periodic cubic vertices $\mathrm{Fin}\,N\times\mathrm{Fin}\,N\times\mathrm{Fin}\,N$, define the associated vertex potential on the canonical periodic Freudenthal triangulation by $(Tu)(i)=u(\iota(i))$, where $\iota$ is the canonical equivalence from the finite index set $\mathrm{Fin}\,n_V$ onto the lattice vertices.
background
The module is Stage 1 of panel-locked Test G in the QG full-theory campaign: exact general-$N$ stencil identity for the frozen quadratic energy on the canonical Freudenthal family (action-level continuum limit; path-sum pillar still red).
Periodic cubic vertices are triples in $\mathrm{Fin},N^3$. The canonical periodic Freudenthal triangulation packages those vertices, periodic edges, and tets into a finite Triangulation3D skeleton. Its vertex count $n_V$ is the cardinality of that product; the canonical finite encoder vertexFinEquiv is the equivalence $\mathrm{Fin},n_V\simeq$ lattice vertices.
A vertex potential on a triangulation $K$ is simply a map $\mathrm{Fin},K.n_V\to\mathbb{R}$. Regge Hessian quadratic forms and Dirichlet edge energies take that finite-index type, so lattice fields must be transported before they enter those functionals.
proof idea
One-line definition: send each finite index $i$ to the lattice value of $u$ at the image of $i$ under the canonical vertex equivalence. No lemmas; pure composition of $u$ with vertexFinEquiv.
why it matters
Bridge between lattice fields and the triangulation API used by every Stage-1 identity. Downstream, hessianQuadratic_canonical_eq_freudenthalStencil and freudenthal_stencil_identity feed toPotential N u into the canonical Regge Hessian so the frozen quadratic form equals the seven-class stencil $\sum_x\sum_d c_d(u(x+d)-u(x))^2$ with weights $\sqrt{\ell_d^2}\in{1,1,1,\sqrt{2},\sqrt{2},\sqrt{2},\sqrt{3}}$. The same transport appears in scaledCanonicalEnergy, the edge-stencil equality, and Regge TT-symbol preflight (conformal tet squared edges, deficit angles, frozen identification).
Without this encoder, lattice $u$ cannot sit in VertexPotential, and the derived (not postulated) stencil continuum limit cannot be stated. It is scaffolding glue for the tensor-first anisotropic action limit, not a physics claim itself; $D=3$ and the Freudenthal family are already fixed upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.