classDisp_ne_zero

This module builds the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes given by the nonzero displacement vectors in ${0,1}^4$, indexed by Fin 15 via bit masks $d.val+1$. Each class $d$ has a Boolean bit test for coordinate $i$, a real displacement $D_d$ with entries $0$ or $1$ according to those bits, and a natural Hamming weight equal to the number of set bits among the four coordinates.

The weight is already known to be strictly positive for every $d$ (by exhaustive case split on Fin 15). The displacement is the real-valued 0/1 lift of the same mask, so nonvanishing of $D_d$ is the geometric counterpart of that positive weight. The local campaign uses these classes for plane-wave midpoint loading and a provisional finite quadratic aggregate with all-ones weights; true 4D Regge Hessian weights remain open.

Argue by contradiction. Assume $D_d = 0$. Componentwise vanishing plus the definition of the displacement forces each of the four class bits to be false. Unfolding the Hamming weight as the sum of the four bit indicators then yields weight zero. That contradicts the prior positivity theorem on the weight (proved by fin_cases and decide). Hence $D_d \neq 0$.

Nonzero displacements are the first integrity check on the 15-class packaging that feeds plane-wave class coefficients, squared-length factors, and the provisional finite TT quadratic. Without it, a zero mask could silently enter sums such as $\sum_d (D^T H D)^2$ or the gauge-load identity $D^T(\mathrm{gauge})D = 2(m\cdot D)(v\cdot D)$. The module explicitly does not claim true Regge weights, Einstein-Hilbert recovery, or full edge-TT decomposition; this lemma only locks the combinatorial skeleton those later steps will reuse. No downstream theorem yet depends on it, so it is infrastructure for the next kernel-checked increments in the 4D QG campaign.