axisWitnessEndpointUnitPotential_apply
plain-language theorem explainer
On the 5×5×5 periodic cubic witness lattice, the axis-endpoint unit potential evaluates to 1 exactly at the two distinguished axis endpoints and to 0 at every other vertex, after transport through the canonical Fin encoding. Gravity workers instantiating the six-tet cubic Dirichlet model cite this when collapsing potential lookups to vertex predicates. The proof unfolds the potential definition and rewrites equalities by injectivity of the vertex Fin equivalence.
Claim. Let $v$ be a vertex of the periodic cubic lattice of size $5\times 5\times 5$. Write $\iota$ for the canonical equivalence from finite indices to vertices. Then the axis-endpoint unit potential at $\iota^{-1}(v)$ equals $1$ if $v=(1,0,0)$ or $v=(2,0,0)$, and equals $0$ otherwise.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it only supplies the witness data and the reduction lemmas that make the target well-formed.
Periodic cubic vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. The witness lattice fixes $N_x=N_y=N_z=5$. The canonical finite encoder vertexFinEquiv identifies every such vertex with a Fin index of the right cardinality; its inverse is the map appearing in the statement.
The two axis witness endpoints are the concrete vertices $(1,0,0)$ and $(2,0,0)$. The axis-endpoint unit potential is the vertex potential on the encoded torus that is defined to be $1$ precisely on the Fin-indices of those two endpoints and $0$ elsewhere.
proof idea
One-line unfold-and-rewrite. Unfold the definition of the axis-endpoint unit potential, which is already an if-then-else on equality of Fin indices with the two encoded endpoints. Then rewrite those equalities using injectivity of the inverse vertex Fin equivalence, converting index equalities into vertex equalities with the two concrete endpoints. No arithmetic or lattice geometry is required.
why it matters
The immediate parent is the one-line identification of this potential with the axis-endpoint characteristic function axisWitnessEndpointXi, obtained by rewriting through the present lemma and reflexivity. That identification is part of the witness package that connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet target.
In the broader gravity chain the module sits downstream of the periodic Freudenthal torus geometry and the Regge cubic lattice limit, and upstream of any claim that a concrete finite-difference Dirichlet action on this witness matches the physical model. The lemma itself is pure bookkeeping, but without it the potential cannot be evaluated at geometric vertices, so the Dirichlet instance cannot be discharged on the witness lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.