canonicalPeriodicTypedEdgeLocalEdgeOfWitness
plain-language theorem explainer
Geometric witness that a typed periodic edge equals the translated local Freudenthal edge of a given cell/tetrahedron pair at some local edge slot. Discrete-gravity and Regge-lattice workers cite it when filtering angle-sum stars by incidence. The body is a one-line existential over Fin 6 equating the edge to the translated local edge map.
Claim. For positive lattice sizes $N_x,N_y,N_z$, a periodic edge $e$ and a periodic tetrahedron $(\mathrm{cell},t)$, the witness holds iff there exists a local edge slot $f\in\{0,\ldots,5\}$ such that $e$ equals the translated local Freudenthal edge of $(\mathrm{cell},t)$ at slot $f$.
background
This module packages the exact theorem 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 periodic edge is a positive-displacement edge on the torus, given by a base vertex and one of seven cube displacements. A periodic tetrahedron is a pair consisting of a cubic cell vertex and one of the six Freudenthal tets inside that cell.
The translated local-edge map sends a cell, a tet index, and a local slot $f\in\mathrm{Fin},6$ to a global periodic edge by adding the cube-edge base offset to the cell and taking the cube-edge displacement. Upstream cube triangulation fixes the chosen global edge for each local tet edge slot; the two-cube strip and periodic torus lift that choice by translation.
proof idea
Definitional predicate only. The body is the existential $\exists f:\mathrm{Fin},6$ such that the typed edge equals the translated local Freudenthal edge of the cell/tet pair at slot $f$. No lemmas are applied; a separate decidable instance unfolds the definition and inherits decidability from equality on periodic edges and finiteness of the slot type.
why it matters
Supplies the geometric incidence filter used by the local-edge-of filtered edge-angle-sum target: the purely geometric finite-star form whose remaining work classifies which translated local Freudenthal edges equal a given typed periodic edge. Downstream, that filtered target implies the slot-witness filtered angle-sum target, and an equivalence theorem identifies this witness with the slot-witness form of typed incidence. The decidable instance lets Finset filters run on it. Together these close packaging steps toward the physical six-tet cubic Dirichlet model on the encoded periodic Freudenthal scaffold, linking discrete Regge/lattice geometry to the Dirichlet action target without claiming the continuum identity yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.