axisWitnessFlatEdgeLengthDir_zero_of_xi_zero
plain-language theorem explainer
If both endpoints of a local Freudenthal edge have vanishing axis-witness scalar field, the directed flat edge length on that edge is zero. Gravity auditors cite it when clearing non-axis stencil contributions in the six-tet cubic Dirichlet instance. The proof is definitional unfold plus simplification on the two endpoint hypotheses.
Claim. Let $(\tau,s)$ be a local Freudenthal pair (tetrahedron index and edge-slot in $\mathrm{Fin}\,6\times\mathrm{Fin}\,6$) and let $k\in\{0,\ldots,5\}$ label a tetrahedron edge. If the axis-witness field $\xi$ equals $0$ at both vertices of edge $k$ in the matching witness cell, then the directed flat edge length of that edge is $0$.
background
This module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A FreudenthalLocalPair is a finite table entry $(\tau,s)\in\mathrm{Fin},6\times\mathrm{Fin},6$ left after the periodic-cell base-offset equation is isolated. Tetrahedron vertices come from the six-tet Freudenthal cube triangulation; edges are the standard six pairs on $\mathrm{Fin},4$ (edge $0=(0,1)$, ..., edge $5=(2,3)$). Vertices are placed on the witness lattice by addVertexBits from a matching cell chosen per local pair.
The axis-witness endpoint field $\xi(v)$ is the indicator that is $1$ only on two distinguished axis endpoints and $0$ elsewhere. The directed flat edge length is the local length functional built from those endpoint values; this lemma records its vanishing off the axis support.
proof idea
Term/tactic hybrid, three lines. Unfold the definition of the directed flat edge length, then simplify with the two hypotheses that $\xi=0$ at both edge endpoints. No external lemmas are required beyond the definitional equations of the length functional and the endpoint field.
why it matters
Inside the gravity domain, the physical six-tet cubic Dirichlet instance must match a finite-difference Dirichlet target on the encoded periodic Freudenthal torus. Axis-witness edges carry the nontrivial displacement; all other local edges must contribute zero directed length so the stencil collapses to the axis channel.
This lemma is the elementary vanishing step for that collapse: once both endpoints lie off the two axis endpoints, the length term drops. It sits among sibling facts about canonical Hessians, periodic edge stencils, and nonnegativity of Dirichlet actions. No downstream consumers are recorded yet; it is local scaffolding for the instance audit table rather than a cited parent theorem. Framework-wise it is pure discrete geometry (Regge/Freudenthal lattice), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.