dispBits
plain-language theorem explainer
Enumerates the seven nonzero positive orthant displacements of the unit cube as Boolean triples: the three axis steps, three face diagonals, and the space diagonal. Anyone building periodic Freudenthal edges, tetrahedron local edges, or the seven-class gravity stencil cites this table. It is a pure case table with no proof obligations.
Claim. The map $d \mapsto (\delta_x,\delta_y,\delta_z)$ from $\{0,\ldots,6\}$ to $\{\mathrm{true},\mathrm{false}\}^3$ lists every nonzero positive cube displacement: $(1,0,0)$, $(0,1,0)$, $(0,0,1)$, $(1,1,0)$, $(1,0,1)$, $(0,1,1)$, and $(1,1,1)$.
background
The module builds a typed periodic Freudenthal torus: vertices on an $N_x\times N_y\times N_z$ lattice with wrap-around, edges as positive cube displacements from a base vertex, and tetrahedra from the standard cube triangulation. The goal is the global incidence/edge-slot partition needed by the nonlinear Regge first-variation theorem, without yet fixing a concrete finite mesh encoder.
In the binary cube labeling, each local vertex offset is a triple of bits. Dropping the origin leaves exactly seven positive displacements. Those seven classes are the combinatorial skeleton of every local edge in the periodic model and of the seven-weight stencil used in the Freudenthal energy analysis (weights $1$, $\sqrt{2}$, $\sqrt{2}$, $\sqrt{3}$ on the axis, face-diagonal, and space-diagonal steps).
Sibling helpers (bit, addBit, addBits, vertexBits) implement coordinate-wise Boolean arithmetic on lattice vertices; this table is the fixed list of nonzero summands those helpers apply.
proof idea
No proof: a definition by exhaustive pattern match on Fin 7. Each constructor is a literal Boolean triple. Downstream lemmas that need agreement with real coordinates (dispReal_matches_dispBits) simply fin_cases on the same seven indices and norm_num against this table.
why it matters
This is the canonical index set for positive-displacement periodic edges: PeriodicEdge stores a base vertex and a Fin 7 displacement drawn from this table. Endpoint and tetrahedron-incidence theorems (localEdgeOf_endpoints_match_tetVerts and related) reduce edge geometry to looking up these bits and adding them (mod period) to the base.
On the gravity side, the seven-class stencil and its moment-tensor identities (stencil_inner_sum_witness, scaledCanonicalEnergy_eq_scaled_stencil, dispReal) treat the same seven directions as the discrete derivative support. Matching real coordinates to these bits (dispReal_matches_dispBits) guarantees the analytic stencil is not free data.
In the broader Recognition geometry stack this is scaffolding for $D=3$ Freudenthal/Regge discretizations on the periodic torus, isolating the remaining finite encoder into Fin nV/Fin nE/Fin nT while locking the local cube combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.