twoCubeStrip_edgeSlotPartition
plain-language theorem explainer
Packages the two-cube Freudenthal strip as an incidence edge-slot partition: each local tetrahedral edge slot maps to a chosen global edge, and a global edge sits in a tetrahedron at that slot exactly when it equals the chosen representative. Anyone building discrete Regge bookkeeping on multi-cube Freudenthal complexes cites this. Proof is a structure instance whose biconditional field is a one-line appeal to the native-decided local-edge equivalence.
Claim. The two-cube strip triangulation (12 vertices, 33 edges, 12 tetrahedra), already equipped with incidence-consistency data, admits an incidence edge-slot partition: there is a map sending each tetrahedron $\tau$ and local edge index $f\in\{0,\ldots,5\}$ to a global edge such that a global edge $e$ lies in $\tau$ at slot $f$ if and only if $e$ equals that chosen representative.
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes sharing one square face, each decomposed into six Freudenthal tetrahedra with compatible face triangulation. After deduplicating the five shared-face edges one obtains a global complex with 12 vertices, 33 edges, and 12 tetrahedra.
An incidence edge-slot partition packages a choice of global edge for every local tetrahedral edge slot together with the equivalence that edge-in-tet membership holds exactly when the global edge is that chosen representative. The strip already supplies the local-edge map and the finite-case equivalence (proved by native decision), plus an incidence-consistency witness that records square-edge globals and vertex-incidence of edges in tets.
This is the first concrete multi-cube incidence instance beyond the single-cube Freudenthal sanity check.
proof idea
Structure instance, not a deep argument. The localEdgeOf field is filled by the existing strip-level local-edge map (global edge representative for each tet and local slot). The required biconditional is discharged by introducing the edge, tetrahedron, and slot indices and applying the already-proved strip theorem that edge-in-tet membership equals equality with the local representative; that theorem itself is a native decision over the finite index types.
why it matters
Direct input to the strip's edge-slot bookkeeping definition, which applies the generic constructor that turns a partition into full incidence bookkeeping. That bookkeeping is the discrete scaffolding for Regge-action first-variation identities on multi-cube Freudenthal complexes. In the Recognition geometry stack this confirms that shared-face edge deduplication preserves the local-to-global edge-slot partition, the first multi-cube check past the one-cube case. It does not touch the forcing chain (T0–T8), phi-ladder masses, or continuum limits, but it is a concrete geometric prerequisite for discrete curvature and action calculations on Freudenthal lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.