slotMidTwice
plain-language theorem explainer
Literal integer lookup table giving twice the midpoint coordinate of each local edge slot on the six-tetrahedron Freudenthal stencil, indexed by tetrahedron, slot, and spatial axis. Gate B bridge and Bloch-assembly proofs cite it as the frozen algebraic stand-in for the geometry-derived midpoint. Defined by exhaustive case table over Fin 6 × Fin 6 × Fin 3; no proof content.
Claim. The map $\mathrm{mid}_{2}:\{0,\ldots,5\}^{2}\times\{0,1,2\}\to\mathbb{Z}$ is the literal table whose value at tetrahedron $t$, local edge slot $f$, and coordinate $i$ equals twice the midpoint offset of that slot along axis $i$ (equivalently $2\cdot\mathrm{base\_bit}+\mathrm{disp\_bit}$).
background
This leaf module holds the heavy polynomial algebra of the Regge TT Gate B bridge (Lane C, Gate C-B) in an import-light context so that a 216-term ring normalization stays under the laptop memory guard. Everything is written as literal tables and scalars; the production geometry is identified later.
The doubled-midpoint table records, for each tetrahedron index $t\in\mathrm{Fin},6$, each of the six local edge slots $f$, and each spatial axis $i\in\mathrm{Fin},3$, the integer $2\cdot(\text{base offset})+(\text{displacement bit})$. Upstream, the geometry-derived form is exactly $2\cdot\mathrm{bit}(\mathrm{slotBaseBit},t,f,i)+\mathrm{bit}(\mathrm{slotDispBit},t,f,i)$. The main assembly grounds that form against the actual edge midpoint phase; this core file freezes the same numbers as a pure case table.
Sibling tables in the same file include the raw rational stencil weights, the slot displacement-class table, and the seven edge-class linear forms used to build the 216-term raw moment sum.
proof idea
Pure definition by exhaustive pattern match: every triple $(t,f,i)$ in $\mathrm{Fin},6\times\mathrm{Fin},6\times\mathrm{Fin},3$ is assigned a fixed integer in ${0,1,2}$. No tactics, no lemmas, no computation beyond the case tree. Downstream equality proofs discharge by fin_cases and rfl against the geometry-derived formula.
why it matters
This table is the algebraic anchor that lets Gate B work without importing the full symbol-program geometry. The algebraic closer proves entrywise equality with the production assembly midpoint (slotMidTwice_eq_core), so every later use of the core table is identified with geometry.
Downstream, bucket keys are differences of these midpoints across the two slots of a raw stencil triple; slot phases are commensurate-momentum dots with half these integers; the raw cosine evaluator then becomes the cosine of a pure slot-phase difference. Those identities feed the continuum-certificate spike bridge and the 216-term moment sum that equals the six tet blocks with free parameters.
In the RS gravity lane this is bookkeeping infrastructure for the Regge TT continuum limit, not a forcing-chain step (T0–T8). It closes the transcription gap between literal core algebra and the grounded Bloch assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.