globalSqEdge
plain-language theorem explainer
Lookup table of squared Euclidean lengths for the nineteen global edges in the Freudenthal six-tetrahedron unit-cube triangulation. Axis edges get 1, face diagonals 2, and the body diagonal 3. Incidence-consistency and Regge-action constructions cite this as the global edge metric. Pure case split on Fin 19.
Claim. A function $\ell^2:\{0,\ldots,18\}\to\mathbb{R}$ assigning squared length to each global edge of the Freudenthal cube triangulation: $\ell^2=1$ on axis-aligned edges, $\ell^2=2$ on face diagonals, and $\ell^2=3$ on the unique body diagonal from vertex $0$ to $7$.
background
The module builds the standard Freudenthal decomposition of the unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are labeled by binary coordinates; the six tets are the monotone paths from $0$ to $7$.
Regge and discrete-Laplacian bookkeeping need a global edge metric. Squared lengths are the natural data: an axis edge of the unit cube has $\ell^2=1$, a face diagonal $\ell^2=2$, and the space diagonal $\ell^2=3$. The triangulation introduces internal edges beyond the cube skeleton, giving nineteen global edges in total.
An analogous (smaller) table appears in the two-cube-strip module. Upstream continuum-bridge material identifies weighted edge sums with a discrete Laplacian action, so this table is the concrete metric input to that identification.
proof idea
Definition by exhaustive pattern match on Fin 19. Each index is assigned a constant real (1, 2, or 3). The residual constructor ⟨n+19, h⟩ is discharged by absurd plus omega, proving no further indices exist. No lemmas are invoked; the body is a pure lookup table.
why it matters
This table is the global edge metric plugged into freudenthalCube_incidenceConsistent, which packages the Freudenthal cube as an IncidenceConsistent instance. The matching theorem local_sqEdge_eq_global proves every local tet edge length agrees with this global assignment.
The same pattern is reused for the two-cube strip and for periodic Freudenthal tori (canonicalPeriodicIncidenceConsistent_of_endpoint). Downstream Regge-action lemmas (canonicalEdgePairWeight, Dirichlet-equals-edge-stencil identities) read weights from this metric. In the Recognition geometry stack it supplies the concrete edge data underlying discrete curvature and first-variation calculations on the cube lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.