freudenthalCube_edgeSlotBookkeeping
plain-language theorem explainer
Concrete incidence edge-slot bookkeeping certificate for the Freudenthal six-tetrahedron unit cube. Discrete-geometry and Regge-calculus workers cite it when reindexing local edge-slot sums against global edges on this mesh. Built as a one-line application of the generic partition-to-bookkeeping constructor to the cube's edge-slot partition.
Claim. The Freudenthal triangulation of the unit cube (8 vertices, 19 edges, 6 tetrahedra along monotone paths from $(0,0,0)$ to $(1,1,1)$) carries an incidence edge-slot bookkeeping certificate: for every local weight $w$ on tetrahedron-edge slots, the sum over global edges of (flat edge length times aggregated slot weight) equals the direct sum of $w$ over the six local slots of each tetrahedron, with matching flat lengths.
background
The module fixes the standard Freudenthal decomposition of one unit cube into six tetrahedra, using the body diagonal from vertex 0 to 7. Vertices are binary coordinates $0=(0,0,0),\ldots,7=(1,1,1)$; the six tets are the monotone paths from 0 to 7. The finite triangulation record has $n_V=8$, $n_E=19$, $n_T=6$ with explicit edge and tet vertex tables.
Upstream, incidence consistency packages a global squared-edge map and the vertex-incidence check that every local edge of a tet matches the recorded global edge endpoints. The edge-slot partition then supplies a local-edge-of map with the iff that a global edge sits in a tet precisely when it is that local slot, giving uniqueness and no duplication.
IncidenceEdgeSlotBookkeeping is the certificate that summing a local edge-slot weight over global edges and tetrahedra equals summing it directly over local tetrahedral slots, with matching flat edge lengths. Its doc notes that completeness alone is not enough: exact reindexing needs the uniqueness/no-duplication recorded by the partition.
proof idea
One-line wrapper. Feed the Freudenthal cube triangulation, its incidence-consistency witness, and its edge-slot partition into the generic constructor incidenceEdgeSlotBookkeeping_of_partition. That constructor fills the sum_match field of the bookkeeping structure by reindexing along the partition's local-edge map; no further case analysis is done here.
why it matters
Closes the Freudenthal cube instance of the incidence bookkeeping interface used by first-variation Regge calculus in the geometry layer. Downstream consumers (none wired yet in the graph) can invoke sum_match to move freely between global-edge sums and per-tet six-slot sums when differentiating the Regge action on this mesh.
In the broader Recognition stack this is scaffolding for discrete 3-geometry on the eight-tick / $D=3$ side (T7–T8): a concrete, fully enumerated cube that can host curvature and action calculations without abstract incidence hypotheses. It does not itself force continuum physics; it only certifies that the standard six-tet cube is a valid bookkeeping domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.