closed_free_bits

In the EdgeSectorBridge setting, a face carries four raw boundary bits (the edge bits of a pixel). Ledger closure is a single parity constraint on those bits: only configurations whose bits sum even (or the module's equivalent parity) are retained. The surviving set is the closed-configuration collection; its cardinality is the number of free post-closure bits.

The module's panel brief relocates the live holography candidate from sector labels (D₄-orbit names) down to these edge bits. Two decide-level combinatorial checks settle content before any measure theory: (i) sector identity is a deterministic function of the edges, and (ii) closure leaves exactly three free bits, not four. This declaration is check (ii).

Upstream scaffolding supplies the edge geometry and recognition primitives used elsewhere in the bridge; the local fact needed here is only the finite enumeration of closed bit-strings.

One-line term wrapper: the statement is definitionally the already-proved closed-configuration cardinality lemma, so the proof is just that lemma applied as a term. No new case split or decide runs at this site.

This is the free-bits half of the EdgeSectorBridge certificate: the parent edgeSectorBridgeCert records it as the free_bits_three field, alongside sector well-definedness, surjectivity onto admissible sectors, and the lossy two-to-one quotient.

Framework role: it sharpens the live 4H versus 3H fork named in the module brief. If pixel area tracks realized post-closure information, the count is three free bits (log 8); if it tracks raw pre-closure capacity, the count is four. The combinatorial side is now closed: parity removes exactly one degree of freedom from four raw bits.

It does not touch T5–T8 forcing, the RCL, or the alpha band. It also does not identify an edge with an independent T9 recognition event; that remains an unformalized physical assertion. What dies here is any informal claim that closure somehow preserves four free bits.