edgeInTet_vertices
plain-language theorem explainer
If a global cube edge sits in a Freudenthal tetrahedron at local slot f, its two endpoints equal the tetrahedron's images of that local edge's endpoints, up to swap. Incidence bookkeeping for the six-tet cube cites this to discharge the vertex-matching field of IncidenceConsistent. The proof is exhaustive case analysis on the finite edge, tet, and slot indices, closed by simplification of the lookup tables.
Claim. Let $e\in\{0,\ldots,18\}$ index a global edge of the Freudenthal cube, $\tau\in\{0,\ldots,5\}$ a tetrahedron, and $f\in\{0,\ldots,5\}$ a local edge slot. If the incidence map sends $(e,\tau)$ to $\mathrm{some}\,f$, write $(v_1,v_2)$ for the global endpoints of $e$ and $(a,b)$ for the standard local endpoints of slot $f$. Then either $\mathrm{tetVerts}_\tau(a)=v_1$ and $\mathrm{tetVerts}_\tau(b)=v_2$, or the two equalities hold with $v_1$ and $v_2$ swapped.
background
The module builds the standard Freudenthal decomposition of the unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are binary labels $0..7$; the six tets are the monotone paths from $0$ to $7$.
Global geometry is tabulated: edgeVerts lists the $19$ distinct undirected edges as pairs in $\mathrm{Fin},8\times\mathrm{Fin},8$; tetVerts sends each tet index and local vertex slot in $\mathrm{Fin},4$ to a cube vertex; edgeInTet is the partial incidence map from a global edge and tet to a local edge slot in $\mathrm{Fin},6$ when the edge belongs to that tet.
Local edge endpoints come from the shared Regge foundation table edgeVertices on $\mathrm{Fin},6$. The present statement is the orientation-aware compatibility between those local endpoints, pushed forward by tetVerts, and the global edgeVerts pair. It is exactly the first structural obligation in the IncidenceConsistent interface used throughout the 3D Regge scaffold.
proof idea
Pure finite exhaustion. The tactic block runs fin_cases on the global edge index $e:\mathrm{Fin},19$, the tet index $\tau:\mathrm{Fin},6$, and the local slot $f:\mathrm{Fin},6$, then simplifies the hypothesis edgeInTet e τ = some f and the goal against the concrete lookup definitions of edgeInTet, edgeVerts, tetVerts, and ReggeRigorousFoundation.edgeVertices. Non-incident triples are eliminated by the hypothesis; each surviving triple reduces to a propositional equality of cube vertices that simp closes. No intermediate lemmas are invoked.
why it matters
This is the cube-level witness for the vertex-matching field of IncidenceConsistent. Downstream, freudenthalCube_incidenceConsistent installs it verbatim so the six-tet cube becomes a fully consistent Triangulation3D. The same pattern is copied by the two-cube strip and by periodic Freudenthal tori (canonicalPeriodicIncidenceConsistent_of_endpoint).
Once incidence is consistent, hinge measures under conformal rescaling reduce to local squared edge lengths (hingeMeasureUnderConformal_eq_local_sqrt_of_incident), which feeds the nonlinear Hessian and first-variation analysis of the Regge action. In the broader Recognition geometry stack this is scaffolding for discrete curvature and Schläfli identities on the eight-tick / $D=3$ lattice, not a forcing-chain step itself, but a prerequisite for any Regge-based continuum limit arguments built on Freudenthal cubes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.