twoCubeStrip_incidenceConsistent
plain-language theorem explainer
Incidence consistency for the two-cube Freudenthal strip packages global squared edge lengths, vertex recovery for edges in tetrahedra, local-to-global length matching, completeness of local edge slots, and the Schläfli identity on each tet. Multi-cube Regge or discrete-geometry bookkeeping on this complex cites it as the incidence hypothesis. The construction is a thin structure instance reusing the strip's incidence lemmas and the single-cube Freudenthal Schläfli closed form.
Claim. The two-cube Freudenthal strip satisfies incidence consistency: squared lengths of global edges are given by the strip edge-length table; whenever a global edge appears as a local edge of a tetrahedron, its endpoints match that tetrahedron's edge vertices (up to order) and its squared length equals the local squared length; every local edge slot of every tetrahedron is realized by some global edge; and each tetrahedron obeys the Schläfli closed-form identity of the unit-cube Freudenthal tetrahedron.
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. The aim is a global local-edge-slot partition after deduplicating the five shared-face edges, the first concrete multi-cube incidence instance beyond the one-cube sanity check.
Incidence consistency is the structure linking global edges to tetrahedra. It supplies a global squared-edge map, a proof that edge-in-tet incidences recover the correct vertex pairs, equality of local and global squared lengths on those incidences, surjectivity of local edges onto the six slots of each tet, and the Schläfli identity on each tet. Upstream, the single-cube Freudenthal triangulation already gives a nondegenerate tet with positive squared edges and matching incidence theorems; the strip re-establishes the analogous vertex and length facts on its own edge and tet index sets.
proof idea
The definition is a structure instance for incidence consistency on the two-cube strip. The global squared-edge field is the strip's existing edge-length table. Three incidence fields are one-line wrappers: each introduces the relevant edge, tet, and local-slot indices and applies the strip theorems on vertex recovery for edges in tets, local-to-global squared-length equality, and completeness of local edges. The Schläfli field applies the closed-form Schläfli identity to the imported nondegenerate unit-cube Freudenthal tetrahedron, for every tet index of the strip.
why it matters
This instance is the incidence hypothesis required by the strip's edge-slot partition and the subsequent edge-slot bookkeeping definition. Those objects establish the global local-edge-slot partition after shared-face deduplication, which the module presents as the first multi-cube incidence instance beyond the one-cube check. In the Recognition geometry stack this is concrete substrate for discrete curvature and Regge-type bookkeeping on Freudenthal triangulations. It is not a forcing-chain step (T0–T8) and does not touch RCL, phi, or the alpha band; it closes the multi-cube incidence interface needed before larger complexes can be treated uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.