globalSqEdge
plain-language theorem explainer
Assigns squared Euclidean length to each of the 33 global edges in the two-cube Freudenthal strip (values in {1,2,3}). Anyone building incidence-consistent Regge data or checking local-to-global edge matching cites this table. It is a pure case table on Fin 33 with an absurd branch past index 32.
Claim. A function $E \to \mathbb{R}$ on the $33$ global edges of the two-cube strip that returns the squared length of each edge: $1$ for axis edges, $2$ for face diagonals, and $3$ for space diagonals (with the out-of-range branch impossible).
background
The module builds the smallest nontrivial multi-cube Freudenthal complex: two unit cubes sharing a square face, each split into six Freudenthal tetrahedra with matching face triangulation. After deduplicating the five shared-face edges one obtains a global edge set $E \simeq \mathrm{Fin},33$.
Squared edge length is the natural discrete metric input for Regge calculus and for the incidence-consistency interface. The single-cube precursor already defines an analogous table on $\mathrm{Fin},19$ ("Squared length of each global edge"). Here the table is extended to the strip geometry so that every local tetrahedron edge slot can be compared to a unique global squared length.
Values $1,2,3$ are exactly the squared Euclidean lengths of axis edges, face diagonals, and space diagonals inside the unit cube lattice.
proof idea
Pure definition by exhaustive pattern match on the edge index $0..32$, each clause a numeric literal in ${1,2,3}$. The residual constructor $\langle n+33,h\rangle$ is discharged by absurd plus omega, so the function is total on $\mathrm{Fin},33$. No lemmas are invoked.
why it matters
This table is the metric half of twoCubeStrip_incidenceConsistent, which packages the strip as an IncidenceConsistent complex. Downstream, local_sqEdge_eq_global proves that every occupied local edge slot of a Freudenthal tetrahedron carries the same squared length as the corresponding global edge. The same pattern feeds the single-cube incidence package and, by analogy, the canonical periodic torus incidence data and concrete Regge edge-pair weights.
In the Recognition geometry stack this is the first multi-cube metric instance beyond the one-cube sanity check, so later continuum or torus limits can trust that squared lengths are globally coherent across shared faces. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it supplies discrete edge data those continuum arguments eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.