slotMidTwice_eq_geometry
plain-language theorem explainer
On each tetrahedral edge slot of a periodic Freudenthal cell, the tabulated doubled midpoint equals twice the slot base bit plus the actual edge displacement, coordinatewise. Gravity analysts assembling Regge TT Bloch sums cite this when converting discrete midpoints into geometric phases. The proof is exhaustive case analysis on the six tetrahedra, six faces, and three axes, discharged by norm_num.
Claim. For every nonzero lattice size $N$, every cell vertex in the $N\times N\times N$ torus, every tetrahedral edge slot $(t,f)\in\{0,\ldots,5\}^2$, and every coordinate $i\in\{0,1,2\}$, the real value of the doubled-midpoint table entry divided by two equals the base bit of that slot plus half the $i$-th component of the displacement of the chosen global edge of the cell.
background
This module is the C-DAG1 finite-cell assembly stage for Regge transverse-traceless gravity. Cosine evaluators are built from integer phase keys on Bloch buckets, independently of quadratic moment machinery. Periodic wrapping of local edges is handled by an explicit integer-turn phase decomposition plus cosine periodicity.
A Freudenthal cube triangulation assigns to each local tetrahedral edge slot a global edge via localEdgeOf. Each such edge carries a base bit (the unwrapped cube-vertex contribution along a coordinate) and a displacement vector. The doubled-midpoint table records, as an integer, twice the geometric midpoint coordinate of that slot; the present identity says that table is exactly the base bit plus half the true displacement, coordinate by coordinate.
Upstream geometry supplies the local-edge lookup and the bit/displacement extractors on the periodic Freudenthal torus. The eight-tick phase infrastructure is present in the dependency cone but is not invoked in this identity itself.
proof idea
Pure finite case split. The three indices $t$, $f$, and $i$ each range over a finite type of cardinality at most six, so fin_cases expands the goal into a finite list of concrete numerical equalities. Each residual goal is closed by norm_num after unfolding the definitions of the doubled-midpoint table, the slot base and displacement bits, the cube vertex and displacement bits, the local-edge map (both the cell-level and triangulation-level versions), the cube edge base/displacement tables, the vertex and displacement bit extractors, the bit coercion to reals, and the real displacement projector. No inductive argument or external lemma application is required.
why it matters
The sole downstream consumer is the exact phase decomposition for every cell, including periodic seams: the wrapped edge-midpoint phase equals the cell Bloch angle plus the slot phase minus $2\pi$ times an integer wrap count. That decomposition needs the midpoint table to match geometry coordinatewise so that the residual is an integral number of turns and cosine periodicity applies.
In the broader Regge TT Bloch assembly, this identity is the bridge from the discrete slot tables to the geometric displacement that enters the commensurate-momentum phase. It supports the module claim that, for every side length and non-aliased commensurate wave vector, the normalized canonical finite value equals the raw bucket-fiber Bloch fold. No continuum certificate or spike module is involved; the result stays inside the finite-cell C-DAG1 stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.