axisWitnessEndpointUnitPotential
plain-language theorem explainer
Unit conformal potential on the canonical 5×5×5 periodic Freudenthal torus that equals 1 exactly at the two axis-witness endpoints and 0 on every other vertex. Gravity and Regge-lattice workers cite it as the endpoint-unit test field for axis-displacement fiber sums and as the counterexample potential that falsifies the per-disp mixed closed-form target at class 0. The body is a pointwise indicator on Fin-indexed vertices via the canonical vertex equivalence.
Claim. On the canonical encoded periodic Freudenthal torus of size $5\times 5\times 5$, the vertex conformal potential $\phi:\mathrm{Fin}(n_V)\to\mathbb{R}$ defined by $\phi(i)=1$ if $i$ is the Fin-index of either axis witness endpoint (the lattice point $(1,0,0)$ or its partner), and $\phi(i)=0$ otherwise.
background
This module packages exact theorem obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free. The ambient geometry is the canonical encoded periodic Freudenthal torus at witness sizes $N_x=N_y=N_z=5$ with fixed positive spacings, built from the canonical periodic endpoint incidence.
A vertex potential on a finite 3D triangulation $K$ is a map $\mathrm{Fin}(K.n_V)\to\mathbb{R}$ (conformal values at vertices). Vertices of the periodic lattice are identified with a concrete Fin type via the canonical finite encoder vertexFinEquiv. The two support points are the axis witness endpoints, the first of which is the lattice vertex $(1,0,0)$.
Downstream lemmas rewrite evaluation of this potential back to ordinary Vertex coordinates and equate it with the named endpoint indicator field used in explicit fiber pair summands and flat edge-length directional derivatives.
proof idea
Definitional, not a proof. The body is the pointwise function that returns 1 when the Fin index equals the image under vertexFinEquiv.symm of either axis witness endpoint, and 0 otherwise. No lemmas are invoked; later apply theorems recover the Vertex-coordinate form by dsimp and injectivity of the equivalence.
why it matters
This is the standard endpoint-unit test field for the axis-displacement fiber calculus on the physical six-tet cubic instance. Immediate consumers include the apply and apply-equals-xi evaluation lemmas, the identification of tet-vertex potentials with the xi indicator, and the reduction of explicit pair summands and flat edge-length directional derivatives to local closed forms.
It is also the counterexample potential in the negative result that the per-disp explicit-fiber mixed closed-form target fails at axis class 0: the global endpoint-unit fiber sum is $-4$, forcing LHS $4$ against RHS $0$. In the broader Recognition gravity stack it sits inside the Regge cubic lattice / Freudenthal length-chain scaffolding that feeds Dirichlet-type action targets, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.