slotDispCore
plain-language theorem explainer
A fixed 6-by-6 lookup of slot displacement classes valued in Fin 7, used as the leaf-side geometry table in the Regge TT Gate B bridge. Gravity analysts cite it when matching the raw stencil moment fold to the continuum spike blocks. The body is a pure pattern-match table of 36 literals; no proof.
Claim. Define a function $\mathrm{slotDispCore}:\{0,\ldots,5\}\times\{0,\ldots,5\}\to\{0,\ldots,6\}$ by the explicit 36-entry table of displacement classes (row $t$, column $f$ maps to the listed class index). It is the literal stand-in for the grounded slot-displacement-class map of the periodic Regge geometry.
background
This module is the leaf algebra support for Gate C-B of the Lane C finishing charter (ReggeTTGateBBridge). It isolates the heavy polynomial algebra of the spike-convention bridge so that a 216-term ring normalization does not blow the laptop memory guard when combined with the full symbol-program import chain.
Everything here is written over literal tables and scalars. Companion tables include the rational raw-coefficient stencil weights, the doubled-midpoint table, and seven edge-class linear forms. The main bridge module later kernel-identifies each literal table with the corresponding grounded geometric object (periodic slot displacement class, edge midpoint phase, polarized edge coefficients).
The displacement class indexes which of seven edge-class linear forms multiplies a given face-pair contribution in the raw moment term. The six face indices run over the oriented faces of a 3-cube stencil; the codomain Fin 7 is the discrete edge-class label space used by the continuum certificate spike blocks.
proof idea
No proof: this is a definition by exhaustive pattern match on Fin 6 × Fin 6. Each of the 36 clauses returns a concrete Fin 7 literal. Downstream equality theorems discharge the match by fin_cases and rfl.
why it matters
Gate C-B needs a memory-safe leaf copy of the slot displacement geometry so the 216-term raw moment sum can be rewritten as the sum of six tet blocks with free parameters $s_2,s_3,p$, identically in the edge matrix $E$ and the coordinate vector $x$. This table is that leaf copy.
The parent theorem slotDispCore_eq in ReggeTTGateBBridge asserts that the table equals the grounded slotDispClass of the periodic geometry (proved by exhaustive case split). The same table feeds coreTripleTerm and the six private block identities coreBlock0_eq through coreBlock5_eq, which together assemble coreTripleSum_eq_spikeSum: the raw moment fold equals the spike block sum without ever invoking tt_continuum_certificate.
In the broader RS gravity lane this is scaffolding algebra, not a forcing-chain step (T0–T8). It closes a transcription gap between stencil combinatorics and the continuum certificate so Gate C can finish without trusted hand-copied coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.