twoCubeStrip_edgeSlotBookkeeping
plain-language theorem explainer
Packages the two-cube Freudenthal strip into a full incidence edge-slot bookkeeping certificate: local tetrahedral edge-slot sums match global edge sums with consistent lengths. Anyone working first-variation or Regge action on multi-cube triangulations cites this as the smallest nontrivial multi-cube instance. One-line application of the generic partition-to-bookkeeping constructor.
Claim. The two-cube Freudenthal strip triangulation $K$ (two unit cubes sharing a face, $n_V=12$, $n_E=33$, $n_T=12$), together with its incidence-consistency certificate, admits an incidence edge-slot bookkeeping structure: for every local weight $w$, the sum over global edges of (global edge length times aggregated slot weight) equals the direct sum over tetrahedra and their six local edge slots.
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes sharing one square face, each split into six Freudenthal tetrahedra with compatible face triangulation. After deduplicating the five shared-face edges one obtains a global triangulation $K$ with 12 vertices, 33 edges and 12 tets.
Incidence consistency records a global square-edge map and the vertex-incidence check that every local tet edge sits on the claimed global edge. An edge-slot partition then supplies a local-to-global edge map localEdgeOf with the iff that a global edge meets a tet exactly when it is the image of one of that tet's six slots.
IncidenceEdgeSlotBookkeeping is the certificate needed downstream for Regge first variation: summing a local edge-slot weight over global edges and tets equals summing it directly over local slots, with matching flat edge lengths. Existence of a global edge per slot comes from consistency; uniqueness/no-duplication is what the partition supplies.
proof idea
One-line wrapper. Apply the generic constructor incidenceEdgeSlotBookkeeping_of_partition to three already-built objects: the triangulation twoCubeStrip, its incidence-consistency certificate, and the edge-slot partition twoCubeStrip_edgeSlotPartition. That constructor fills the sum_match field by reindexing the double sum through the partition's local-to-global bijection on slots.
why it matters
This is the first concrete multi-cube incidence bookkeeping instance beyond the single-cube sanity check. The module doc states the goal explicitly: prove the global local-edge-slot partition after deduplicating the five shared face edges, then package it as bookkeeping.
In the Recognition geometry stack, Regge-action first variation needs exactly this certificate so that discrete curvature variations can be rewritten as sums over local tet edge slots without double-counting shared faces. The two-cube strip is the minimal place where shared-face edge identification is nontrivial; closing bookkeeping here validates the incidence API before larger Freudenthal complexes.
No downstream consumers are wired yet in the graph (used_by empty), so the declaration presently anchors the multi-cube side of the incidence layer rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.