axisWitnessEndpointUnitPotential_apply_eq_xi
plain-language theorem explainer
On the 5×5×5 witness torus, the axis-endpoint unit potential, evaluated at the canonical Fin index of a vertex v, equals the explicit endpoint indicator ξ(v). Anyone wiring Freudenthal axis-displacement counterexamples or tet-vertex potentials to the Dirichlet instance cites this. The proof is a one-line rewrite of the apply lemma followed by definitional equality.
Claim. For every periodic vertex $v$ on the witness lattice $N_x=N_y=N_z=5$, the axis-endpoint unit potential at the canonical finite index of $v$ equals $\xi(v)$, where $\xi(v)=1$ if $v$ is either distinguished axis endpoint and $\xi(v)=0$ otherwise.
background
This module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it supplies the concrete witness data and identities needed to plug the torus scaffold into that target.
Vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. The map vertexFinEquiv is the canonical equivalence between those vertices and a single finite index type of matching cardinality. The witness sizes are fixed at $N_x=N_y=N_z=5$.
The axis-endpoint unit potential is a vertex potential on the encoded torus that is $1$ exactly on the two distinguished axis endpoints and $0$ elsewhere. The companion function $\xi$ is the same indicator written directly on the vertex type. An upstream apply lemma already evaluates the potential after transporting a vertex through the inverse Fin equivalence and recovers that indicator.
proof idea
Term-mode proof in two steps. Rewrite by the apply lemma, which states that the unit potential at the inverse Fin index of $v$ equals the if-then-else that is $1$ on the two axis endpoints and $0$ otherwise. That right-hand side is definitionally identical to $\xi(v)$, so rfl closes.
why it matters
The identity lets downstream arguments treat the Fin-indexed unit potential and the vertex-level indicator $\xi$ interchangeably on the axis-endpoint witness. It feeds the private lemma equating tet-vertex potentials to $\xi$, and the two negative results that the per-disp explicit-fiber mixed identity and the flat-unfolded mixed hinge-deficit target both fail at axis class $0$ on this endpoint-unit counterexample (fiber sum $-4$ forces LHS $4$ while RHS is $0$).
In the gravity stack this is scaffolding glue inside the physical six-tet cubic Dirichlet instance: it keeps the Freudenthal axis-displacement counterexamples aligned with the encoded periodic torus so the model obligations stay exact rather than schematic. It does not itself settle the physical Dirichlet equality; it only makes the witness potential usable in those failure and identification lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.