edgeInTet_vertices
plain-language theorem explainer
When a global edge of the two-cube Freudenthal strip occupies a local edge slot of one of its twelve tetrahedra, the edge endpoints match that slot's two vertices up to orientation. Multi-cube Regge incidence proofs cite this as the vertex-agreement half of incidence consistency. The argument rewrites incidence through the local-edge bijection, then exhausts the twelve-by-six cases by simplification.
Claim. Let $e$ range over the $33$ global edges of the two-cube Freudenthal strip and $\tau$ over its $12$ tetrahedra. If the incidence map sends $(e,\tau)$ to local edge slot $f\in\{0,\ldots,5\}$, then the two endpoints of $e$ equal the two vertices of slot $f$ inside $\tau$, up to order.
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes sharing a square face, each cut into six Freudenthal tetrahedra with matching face triangulation. After deduplicating the five shared-face edges one obtains $33$ global edges and $12$ tetrahedra.
Incidence is recorded by a partial map from a global edge and a tetrahedron to a local edge slot $f\in\mathrm{Fin},6$. The companion map sends each tetrahedron and local slot to the corresponding global edge. Local slots themselves carry a fixed pair of vertex indices inside the standard tetrahedron (via the Regge foundation edge-vertex table); each tetrahedron also has an absolute vertex embedding into the strip.
The single-cube precursor already proves the same vertex-agreement statement for $19$ edges and $6$ tetrahedra. The two-cube version is the first multi-cube instance of that lemma, needed before one can package a full IncidenceConsistent record for the strip.
proof idea
Apply the local characterization of incidence: the hypothesis that the incidence map returns slot $f$ is equivalent to the global edge equaling the local-edge-of map at $(\tau,f)$. Substitute that equality for the edge variable. Exhaust $\tau\in\mathrm{Fin},12$ and $f\in\mathrm{Fin},6$ by fin_cases, then simplify the endpoint equalities against the concrete tables for local edges, global edge endpoints, tetrahedron vertex embeddings, and the foundation edge-vertex pairs. Every case reduces to a propositional identity.
why it matters
This lemma is the vertex half of the IncidenceConsistent interface for three-dimensional Regge scaffolds: local tetrahedral edge slots must agree with global edge endpoints up to orientation. It is plugged directly into the strip's incidence-consistency record, which is the first concrete multi-cube instance beyond the one-cube sanity check.
Downstream, the same field is required by the single-cube consistency package, by the canonical periodic Freudenthal torus construction, and by the identity that hinge measure under a conformal vertex potential equals the local square-root edge length of an incident slot. Those identities feed nonlinear Hessian and Schläfli arguments on the triangulation. In the broader framework this sits inside the $D=3$ spatial geometry forced by the T8 step of the forcing chain, supplying the discrete incidence substrate for Regge-type action calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.