dispReal
plain-language theorem explainer
Explicit real coordinates of the seven nonzero cube displacements on the Freudenthal lattice: three axis, three face-diagonal, one body-diagonal unit vectors with 0/1 entries. Gravity continuum-limit work cites it as the geometric input to the stencil moment tensor A₀ = Σ c_d d dᵀ. The body is a pure lookup table; matching to the canonical bit table is checked separately.
Claim. Define a map $D: \{0,\ldots,6\} \times \{0,1,2\} \to \mathbb{R}$ by the table of seven displacement vectors in $\mathbb{R}^3$: $e_1,e_2,e_3$, the three face diagonals $e_i+e_j$, and the body diagonal $e_1+e_2+e_3$ (entries in $\{0,1\}$).
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign: the action-level continuum limit of the frozen quadratic Regge energy on the canonical periodic Freudenthal triangulation at every side length $N>2$. The quadratic form is identified with a seven-class nearest-displacement stencil $\sum_x \sum_{d} c_d (u(x+d)-u(x))^2$, with weights $c_d=\sqrt{\ell_d^2}$ read from Hessian dual edge lengths ($\ell^2 \in {1,1,1,2,2,2,3}$).
The geometry source is the canonical nonzero positive cube displacements dispBits: seven Boolean triples for the axis, face-diagonal, and body-diagonal classes on the periodic Freudenthal torus. The Boolean-to-natural bit map sends false$\mapsto 0$, true$\mapsto 1$. The present table is the same data written as real coordinates so that moment sums and inner products live in $\mathbb{R}$ without case splits on Bool.
Local setting (module scope): tensor-first anisotropic continuum limit of the stencil; path-sum over triangulation classes remains out of scope.
proof idea
Definition by exhaustive pattern match on Fin 7 and Fin 3: each of the seven rows is the coordinate triple of one displacement class. No lemmas, no computation. The companion theorem dispReal_matches_dispBits later kernel-checks, by fin_cases and norm_num, that each entry equals the indicator of the corresponding bit in the canonical dispBits table.
why it matters
Feeds the stencil moment tensor $A_0=\sum_d c_d, d d^T$ (stencilMomentTensor) and its exact closed form $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ (stencilMomentTensor_eq), plus the sum-of-squares PSD witness stencilMomentTensor_quadratic_eq. Downstream Regge TT bridges use the same coordinates for edge midpoint geometry (slotMidTwice_eq_geometry), polarization edge coefficients (corePolEdgeCoeff_eq, polEdgeCoeff_alternatingSum), and Gate-B grounding.
In the Recognition gravity stack this is the geometric skeleton of the Freudenthal stencil identity that equates the canonical Regge Hessian quadratic form to the seven-class Dirichlet stencil for every $N>2$. It carries no free data: the table is forced by the cube's nonzero displacements, aligning with the module claim that weights and classes are derived from the Hessian incidence structure rather than postulated. Does not itself touch T0–T8 or the RCL; it is lattice geometry supporting the continuum-limit panel test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.