sectorOf_surjective_on_closed
plain-language theorem explainer
Every admissible sector arises as the image of at least one ledger-closed edge configuration under the deterministic map from edges to sectors. Anyone arguing that sectors add no independent information beyond edge bits cites this. The proof is a finite exhaustive check via decide on the closed-config set.
Claim. The set of admissible sectors is contained in the image of the ledger-closed edge configurations under the sector map: every admissible sector equals the sector of some closed edge configuration.
background
The EdgeSectorBridge module settles two combinatorial facts about holographic pixel edges versus $D_4$-orbit sector labels. Raw boundary data are four edge bits; ledger closure (parity) cuts that to eight closed configurations, i.e. three free bits. The sector map sends each closed configuration to one of four admissible sector labels.
The module's panel verdict relocated the live area-law candidate from sectors down to edges: a sector is only a $D_4$-orbit label on those bits, not a free-standing degree of freedom. Surjectivity of the sector map on closed configs is half of showing that the admissible sectors are exactly the image of that map (the other half is that every image lands in the admissible set).
Upstream cost notation $H$ (shifted $J$-cost) appears in the surrounding double-count argument: closed edges carry $\log 8$ of information while sectors carry only $\log 4$, so an additive $H + \log 4$ term would double-count.
proof idea
One-line finite check: decide exhausts the finite sets of admissible sectors and closed edge configurations and verifies every admissible sector appears in the image of the sector map. No algebraic lemmas are invoked; the statement is pure Boolean inclusion on small enumerated sets.
why it matters
Feeds the certificate edgeSectorBridgeCert as the sector_surjective field, alongside well-definedness, three free bits after closure, and the 2-to-1 lossy quotient fact. Together those four facts kill $H + \log 4$ as a candidate area law: sectors are a projection of edge bits, never an independent additive $\log 4$.
In the holography fork between pre-closure capacity $4H$ and post-closure realized information $3H$, this closes the combinatorial half of question (1) from the module doc: sectors carry no information beyond the edges. It does not choose $3H$ versus $4H$, and it does not identify an edge with an independent T9 recognition event; those remain physical questions. Framework-wise it sharpens the holographic counting that sits downstream of the eight-tick and $D=3$ forcing chain without touching the $J$-uniqueness or $\phi$ fixed-point steps directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.