twoCubeStrip
plain-language theorem explainer
The two-cube Freudenthal strip is the concrete 3D triangulation of two unit cubes glued on a square face: 12 vertices, 33 edges, 12 tetrahedra. It packages the local edge and tet maps into one Triangulation3D instance. Anyone proving multi-cube incidence or edge-slot partition cites this object. The body is a pure structure assembly wiring already-defined maps and the single-cube nondegenerate tet.
Claim. Let $K$ be the complex formed by two unit cubes sharing one square face, each cube Freudenthal-triangulated into six tetrahedra with matching face edges. Then $K$ is a 3D triangulation with $n_V=12$ vertices, $n_E=33$ edges, $n_T=12$ tetrahedra, with the stated edge-endpoint, tet-vertex, and edge-in-tet incidence maps, and every tetrahedron nondegenerate in the Freudenthal sense.
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 compatible face triangulation. After identifying the five shared-face edges, the global complex has twelve vertices and thirty-three edges.
Upstream, the single-cube package supplies the nineteen unique cube edges, the six tet vertex lists, the local edge-in-tet incidence table, and the nondegenerate Freudenthal tet (positive squared edge lengths and positive Cayley-Menger content). This module lifts those maps across two cubes via local-to-global edge indexing, then feeds them into the abstract Triangulation3D record.
A triangulation here is just the finite incidence data: vertex/edge/tet counts plus endpoint and membership maps. No metric embedding is required at this layer; nondegeneracy is inherited cubewise from the single-cube tet.
proof idea
Pure definitional assembly, not a tactic proof. Counts are hard-coded: twelve vertices, thirty-three edges, twelve tets. Edge endpoints, tet vertices, and edge-in-tet incidence are the module-local maps already built from the single-cube tables plus the two-cube local-edge indexing. Every tet is set to the same nondegenerate Freudenthal tet from the one-cube module. No lemmas are applied; the structure fields are filled by name.
why it matters
This is the first concrete multi-cube incidence instance beyond the one-cube sanity check. Downstream it is the carrier for incidence consistency, the edge-slot partition (local edges as a partition of global edges after face deduplication), and the edge-slot bookkeeping package built from that partition.
In the Recognition geometry stack, Freudenthal cubes are the discrete 3-space cells compatible with the eight-tick octave and the forced $D=3$ step of the forcing chain. A verified two-cube strip is the minimal test that face-gluing preserves local edge slots globally, which any larger lattice or rung-descent complex must inherit.
It does not yet prove continuum limits or physical constants; it closes the combinatorial incidence layer needed before those lifts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.