weight
plain-language theorem explainer
Hamming weight of a D=3 cell configuration: the number of set bits among the eight cube vertices. Used wherever bulk support size matters (record-kernel weight bounds, face-flip invisibility at weight 4, crystal coherence scores). Defined by counting true vertex bits over Fin 8.
Claim. For a full-cell configuration $c$ (one recognition bit on each of the $8=2^3$ vertices of the forced $D=3$ cube, packed as an element of $\{0,\ldots,255\}$), the weight is $\mathrm{wt}(c)=\#\{i\in\{0,\ldots,7\}:\text{bit $i$ of $c$ is set}\}\in\mathbb{N}$.
background
The CellInjection module runs the cell-injection test on the forced eight-tick $D=3$ cube: eight vertices, six faces, one recognition bit per vertex. Configurations are CellCfg $\cong$ Fin 256; vertex $v$ has coordinate bits $(v&1,v&2,v&4)$. The vertex extractor reads bit $i$ of the packed natural via Nat.testBit.
The boundary record is the six face-closure parities (even XOR on each face). The module asks whether bulk flips necessarily change that record. Weight measures bulk support size and is the natural grading for kernel elements: whole-face flips have weight 4; the blind set is generated by such moves.
Parallel vbit extractors exist for faces (Fin 4) and dominoes (Fin 6); the cell version is the same pattern on eight vertices. Homonymous weight classes elsewhere (gauge-volume label density, quotient path sums) are unrelated naming collisions.
proof idea
Pure definition, no proof. Enumerate List.finRange 8 and count with countP how many indices $i$ satisfy that vertex bit $i$ of $c$ is true. Equivalent to the Hamming weight of the 8-bit string of $c$.
why it matters
Grades bulk configurations in the entropy-fork / holography program. Downstream, the module uses weight to state that blindness is only global: equal boundary records imply Hamming distance at least 4, tight because a whole-face flip (weight 4) is invisible from every base. That feeds the rank-nullity picture $|\mathrm{image}|=|\mathrm{kernel}|=16$ on the cell record map and the dichotomy that every single-vertex flip posts while the record map remains non-injective.
Outside holography, the same notion appears as Hamming weight on $\mathbb{F}_2^3$ (unique weight-0/weight-3 vectors, nonzero count 7 linking Booker-plot families) and as a coherence ingredient in crystal stability scores. Framework landmarks: T7 eight-tick octave and T8 $D=3$ fix the eight-vertex cell this counts on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.