slotDispClass
plain-language theorem explainer
Literal lookup table assigning each local edge slot of each tetrahedron type to one of seven displacement classes on the periodic Regge lattice. Gravity analysts cite it whenever the Bloch/TT stencil folds edge polarizations through class coefficients. The body is a pure pattern-match table on Fin 6 × Fin 6, with no proof obligations.
Claim. A fixed map $\mathrm{slotDispClass}:\{0,\ldots,5\}\times\{0,\ldots,5\}\to\{0,\ldots,6\}$ sending tetrahedron type $t$ and local edge slot $f$ to the displacement class of that edge in the periodic geometry (cell-independent by construction of the local-edge embedding).
background
This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the Regge TT Bloch symbol. The sympy diagnostic showed that the stencil-only constant block does not vanish under the reported TT witness, while the assembled block (hinge minus stencil residual) does.
On the periodic triangulation there are six tetrahedron types and six local edge slots per tet. Edges fall into seven displacement classes (the classes that polEdgeCoeff E d indexes). The class assigned to slot $f$ of type $t$ is independent of the cell; it is the geometry that the actual periodic identification induces via localEdgeOf.
slotDispClass is the grounded literal table of that assignment. Downstream bridges prove it coincides with the core table used in Gate B (slotDispCore_eq).
proof idea
No proof: the declaration is a total pattern-match definition on Fin 6 → Fin 6 → Fin 7. Each of the 36 pairs $(t,f)$ is mapped to a concrete class in Fin 7 by exhaustive case clauses. Equality with the core table is discharged later by fin_cases and rfl in slotDispCore_eq.
why it matters
Every raw stencil weight and the assembled constant block route edge polarizations through this table: rawTripleWeight and assembledConstantBlock both evaluate polEdgeCoeff E (slotDispClass t f). Gate B bridges (slotDispCore_eq, corePolEdgeCoeff_eq) identify the core linear forms with these grounded classes, so the moment fold is not an ad-hoc relabeling.
That identification feeds the zero-mode headline: at the TT witness the hinge/edge-diagonal block cancels the recorded stencil residual, and the Schlaefli-reduced assembled constant block vanishes. Without a fixed, cell-independent class table, the hinge-aware cancellation and the relative-minus assembly convention (assembled = hinge - Sigma_Gcc) would not be pinned in the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.