closedConfigs
plain-language theorem explainer
The finite set of ledger-closed face configurations: the 16 raw 4-bit boundary states filtered to those with even vertex parity. Anyone counting free edge bits, closure rank, or the 4H/3H coefficient fork cites this set as the pre-D₄ substrate. The body is a one-line Finset filter on the Boolean parity predicate.
Claim. Let a face configuration be an element of $\{0,\ldots,15\}$ encoding four vertex bits. Define the set of ledger-closed configurations as those $c$ for which the four bits have even parity (XOR to zero). Equivalently, the kernel of the Boolean closure map on the full $2^4$-point configuration space, before any $D_4$ quotient.
background
In the pixel-local holography layer, a boundary plaquette is a face configuration: four recognition bits on the vertices of a cube face, packed as an element of $\mathrm{Fin},16$. Ledger closure on that face is the Boolean predicate that those four bits XOR to zero (even parity): a closed recognition loop posts a balanced, zero-sum ledger around the face.
This module sits one layer below sector labels. A panel verdict relocated the live $4H$ vs $3H$ coefficient question from $D_4$-orbit sectors down to raw edge bits. The two adjudicating combinatorial facts are: (i) a sector is a deterministic lossy quotient of the edges, and (ii) parity leaves exactly three free bits out of four. The closed-configuration set is the common substrate for both checks.
Upstream, the same parity idea appears on the glued domino (both unit faces even), but here only the single-face predicate is used.
proof idea
Pure definition: take the universe of all face configurations and retain those $c$ for which the Boolean ledger-closure predicate evaluates to true. No lemmas, no tactics; the cardinality and free-bit restatements are separate theorems proved by decide.
why it matters
This set is the kernel object that pins the live coefficient fork. Downstream, closed_configs_card proves its cardinality is exactly $8=2^3$, and closed_free_bits restates that as three free bits: if pixel area tracks post-closure realized information the count is 3, if raw pre-closure capacity then 4.
In CoefficientBridge it supplies the nullity: freeBits is $\log_2$ of this cardinality, and rank-nullity reads $|\mathrm{image}|\cdot|\mathrm{kernel}|=16$ with $|\mathrm{kernel}|$ taken from here, forcing closure rank 1 and the two rational branches of the target coefficient bridge. Locally it also feeds the lossy-quotient certificate that sectors carry strictly less information ($\log 4$) than closed edges ($\log 8$), killing additive $H+\log 4$ double-counting.
It does not settle which substrate $a_{\mathrm{pix}}$ attaches to, nor the unformalized claim that one edge equals one independent T9 event.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.