local_sqEdge_eq_global
plain-language theorem explainer
If a global edge of the two-cube Freudenthal strip sits in local slot f of tetrahedron τ, its global squared length equals the canonical Freudenthal local squared length at f. Anyone building multi-cube incidence consistency or Regge hinge measures cites this. The proof recovers the edge from the incidence map, then exhausts the twelve tets and six slots by simplification.
Claim. Let $E\cong\mathrm{Fin}\,33$ be the global edges of the two-cube strip and $T\cong\mathrm{Fin}\,12$ its tetrahedra. If the incidence map sends global edge $e$ and tetrahedron $\tau$ to local slot $f\in\{0,\ldots,5\}$, then the squared length of the standard Freudenthal tetrahedron at slot $f$ equals the global squared length of $e$.
background
The module builds the smallest nontrivial multi-cube Freudenthal complex: two unit cubes sharing a face, each split into six Freudenthal tetrahedra, with shared-face edges deduplicated to 33 global edges and 12 tets.
A Freudenthal tetrahedron carries a fixed local squared-edge 6-tuple (three unit steps, two face diagonals, one body diagonal). The incidence map edgeInTet returns some f precisely when global edge $e$ occupies local slot $f$ of tet $\tau$. The companion bijection states that this holds iff $e$ equals the local-to-global edge map at $(\tau,f)$.
The single-cube ancestor already equates local and global squared lengths under incidence; this strip-level statement reuses the same local squared-edge table while indexing the larger edge and tet sets.
proof idea
Apply the incidence bijection to turn edgeInTet e τ = some f into e = localEdgeOf τ f, then substitute. Exhaust τ : Fin 12 and f : Fin 6 by fin_cases, and simplify against the definitions of the local-edge map, the standard Freudenthal tet, its squared-edge table, and the strip's global squared-edge function. Every case reduces to a numerical identity of squared lengths.
why it matters
Incidence consistency for the two-cube strip packages this equality (via the shared globalSqEdge field and vertex-incidence lemmas) so that every local slot carries the correct metric length. Downstream, the periodic torus incidence builder, the edge-slot partition structure used in first-variation bookkeeping, and the conformal hinge-measure identity all require that local squared lengths match global ones on incident pairs. Without this match, Regge action derivatives and Hessian terms would mix inconsistent edge data across cube boundaries. It is the first multi-cube instance of the local-global length lock beyond the one-cube sanity check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.