localEdge_complete
plain-language theorem explainer
Every local edge slot of every tetrahedron in the two-cube Freudenthal strip is hit by some global edge under the incidence map. Multi-cube incidence and Regge bookkeeping cite this surjectivity. The proof is a one-line witness: the canonical local-to-global edge choice plus the incidence biconditional.
Claim. For every tetrahedron $\tau$ among the twelve tetrahedra of the two-cube Freudenthal strip and every local edge index $f\in\{0,\ldots,5\}$, there exists a global edge $e$ among the thirty-three unique edges such that the incidence map sends $(e,\tau)$ to the local slot $f$.
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes sharing one square face, each cut into six Freudenthal tetrahedra with matching face triangulation. After identifying the five shared-face edges one has twelve tetrahedra and thirty-three global edges.
Incidence is recorded by a partial map from a global edge and a tetrahedron to a local edge slot in ${0,\ldots,5}$. A companion choice map picks, for each tetrahedron and each local slot, one canonical global edge that fills it. The one-cube triangulation already proved the same completeness statement (nineteen edges, six tetrahedra); the strip lifts the same pattern after face-edge deduplication.
proof idea
One-line wrapper. Take as witness the canonical global edge assigned to the pair $(\tau,f)$ by the local-to-global choice map. The reverse direction of the biconditional relating the incidence map to that choice map, applied to the witness and closed by reflexivity, yields the required some f incidence.
why it matters
Completeness of local edge slots is part of the incidence package that makes the two-cube strip an IncidenceConsistent triangulation. That package is reused by the one-cube consistency object, the canonical periodic Freudenthal torus (endpoint form), conformal Schläfli incidence bookkeeping for first variation of Regge action, and the general 3D triangulation consistency scaffold. In the Recognition geometry stack this is the first multi-cube check that local edge slots remain surjective after shared-face identification, a prerequisite for global Schläfli identities without caller-supplied data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.