freudenthalCube_edgeSlotPartition
plain-language theorem explainer
The Freudenthal six-tetrahedron cube carries a unique local-to-global edge-slot partition with no duplicated slots. Anyone building incidence bookkeeping or first-variation Regge data on this triangulation cites this structure. It packages the concrete local-edge table and discharges the membership equivalence by the exhaustive Fin-case lemma relating edge-in-tet to that table.
Claim. There is an incidence edge-slot partition for the Freudenthal cube triangulation ($8$ vertices, $19$ edges, $6$ tetrahedra) relative to its incidence-consistency data: a map sending each tetrahedron index and local edge slot to a global edge, such that a global edge occupies a given local slot in a tetrahedron if and only if it equals that map value (unique assignment, no duplication).
background
The module fixes 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)$. Vertices are binary coordinates $0..7$; the six tets are the monotone paths from $0$ to $7$. The triangulation record has $n_V=8$, $n_E=19$, $n_T=6$, with explicit edge and tet vertex tables.
Incidence consistency already records a global square-edge map and the vertex-support condition for edges inside tets. Separately, localEdgeOf is the chosen lookup: for each tet index and each of its six local edge slots, a global edge in $0..18$. The companion lemma states that edgeInTet e τ = some f if and only if $e$ equals that lookup at $(τ,f)$, proved by exhaustive fin_cases on all three finite indices.
An edge-slot partition is the structure that packages such a lookup together with that membership equivalence, guaranteeing each local slot points at exactly one global edge and that the inverse reading of the incidence table recovers the same assignment.
proof idea
Structure instance, not a deep argument. The local-edge field is filled by the existing concrete lookup table. The only proof obligation is the membership equivalence; it is discharged in one step by applying the already-proved exhaustive case lemma edgeInTet_iff_localEdgeOf after introducing the three finite indices $e$, $τ$, $f$.
why it matters
This is the partition half of the incidence bookkeeping stack for the Freudenthal cube. The immediate consumer is the edge-slot bookkeeping definition, which builds full bookkeeping from any such partition via the generic constructor incidenceEdgeSlotBookkeeping_of_partition. That bookkeeping is the combinatorial substrate for first-variation and Regge-action work on the six-tet cube (the module imports the Regge first-variation geometry layer).
In the broader Recognition geometry chain, a clean edge-slot partition is what lets discrete curvature and deficit bookkeeping run without double-counting shared faces or edges when the cube is the local chart. It does not itself force $D=3$ or the eight-tick octave; those live upstream in the forcing chain. It closes the "unique/no-duplication local edge-slot" claim stated in the doc-comment for this concrete triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.