edgeSectorBridgeCert
plain-language theorem explainer
Certificate that ledger-closed edge configurations carry exactly three free bits and that the sector label is a well-defined, surjective, exactly 2-to-1 lossy quotient of those configurations. Anyone weighing the 4H vs 3H area-law fork, or whether sector-area quantization is an independent principle, would cite it. The proof is a four-field structure instance wiring in four already-proved combinatorial lemmas.
Claim. There is a certificate establishing four facts: the set of ledger-closed face configurations has cardinality $2^3$; the sector map sends every closed configuration into the admissible sectors; every admissible sector arises as the image of some closed configuration; and (admissible-sector count)$\times 2$ equals the closed-configuration count, i.e. the sector map is exactly 2-to-1 on closed edges.
background
This module sits in the holography layer after a panel verdict relocated the live area-law candidate from sectors (D₄-orbit labels) down to raw edge bits. A face configuration is four boundary bits; ledger closure is the parity (XOR) constraint on those bits. Closed configurations are the configurations satisfying that constraint. The sector map sends each configuration to the numerically least element of its D₄-orbit, matching the canonical sector-representative criterion. Admissible sectors are the four closed sector representatives.
The certificate structure packages the two panel-adjudicating combinatorial facts: closure leaves exactly three free bits (cardinality $2^3=8$), and the sector label is a deterministic, surjective, exactly 2-to-1 lossy quotient of the closed edges. Upstream, closed_free_bits restates the closed-count theorem as "3 free bits"; well-definedness and surjectivity of the sector map on closed configs are finite decide checks; the 2-to-1 identity is likewise decided by exhaustive enumeration.
proof idea
Term-mode structure instance for the certificate proposition. Each of the four fields is filled by a named lemma already proved in-module: free-bits-three by the closed free-bits restatement (itself a thin alias of the closed-config cardinality theorem); sector well-definedness by the decide-proved membership lemma; sector surjectivity by the decide-proved image-inclusion lemma; and the lossy 2-to-1 identity by the decide-proved double-count lemma equating admissible-sector cardinality times two with closed-config cardinality. No new reasoning occurs here.
why it matters
This is the packaged discharge of the panel's two cheap decide-checks that kill treating the sector as a free-standing degree of freedom. Because the sector is a strict compression of the closed edges (log 4 versus log 8), any area law of the form H + log 4 double-counts information the edges already carry. Sector-area quantization is thereby ruled out as an independent physical principle; the live candidates move to the edge substrate itself: 4H (pre-closure raw capacity) or 3H (post-closure realized information).
No downstream consumers are wired yet; the certificate is the stable citation surface for those combinatorial facts. It does not touch the forcing chain T0–T8, RCL, or the alpha band directly. The remaining open physical questions it sharpens but does not resolve are which substrate a_pix attaches to (4H vs 3H) and whether one edge equals one independent T9 recognition event.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.