FreudenthalLocalPair
plain-language theorem explainer
Local Freudenthal pairs are the finite index set of (tetrahedron, edge-slot) labels inside one six-tet cubic cell. Stencil-coefficient and first-variation proofs on the periodic Freudenthal torus cite this type whenever a local edge contribution is expanded. The declaration is a pure type synonym: ordered pairs from two copies of a six-element finite type.
Claim. A local Freudenthal pair is an ordered pair $(t,s)\in\{0,\ldots,5\}\times\{0,\ldots,5\}$, where $t$ indexes one tetrahedron in the six-tet triangulation of the cube and $s$ indexes an edge-slot of that tetrahedron. This is the residual finite table after the periodic-cell base-offset equation has been isolated.
background
The ambient module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it wires the torus scaffold to the model target.
A Freudenthal cube triangulation splits the unit cube into six tetrahedra. Each tetrahedron carries a fixed roster of edge-slots. After the periodic base-offset identity is quotiented out, every local geometric contribution is labeled by one such (tet, edge-slot) pair. The type is therefore the Cartesian product of two six-point finite sets.
Upstream, the gluing layer treats a single edge as a two-vertex, one-edge bounded complex. Downstream coefficient work reindexes those edges through the local-pair table when expanding hinge measures and squared edge lengths on the five-cell periodic lattice.
proof idea
Pure abbreviation: the name is definitionally equal to the product of two Fin 6 types. No proof obligations, no lemmas applied.
why it matters
This index type is the bookkeeping spine for the axis-stencil coefficient certificates. Parent results expand one explicit-fiber local-pair contribution into six checked endpoint-slot atoms, equate a real Schläfli/local-length slot to a scaled coefficient atom after square-root cancellation, rewrite flat local edge-length derivatives at the selected fiber cell, and identify periodic displacement-squared edges with Freudenthal tet squared-edge data whenever the pair lies in the displacement fiber.
In the broader gravity chain it sits between the periodic Freudenthal torus geometry and the physical six-tet cubic Dirichlet target: every mixed-axis LHS coefficient expansion and every local-pair displacement membership argument is typed over this finite table. It does not itself close a forcing-chain landmark (T0–T8); it is scaffolding vocabulary for the Regge/Dirichlet identification on the cubic lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.