sectorOf
plain-language theorem explainer
Maps each face (edge-bit) configuration to the numerically least element of its D4-orbit under the face-stabilizer action, yielding a canonical sector representative. Anyone citing the edge-sector bridge, the lossy-quotient claim, or the kill of independent sector entropy needs this map. Pure definition: fold minimum over the finite orbit of the configuration.
Claim. For every face configuration $c$ (four raw boundary edge bits), the sector of $c$ is the numerically least element of the orbit $\{ \sigma \cdot c : \sigma \in D_4 \}$ under the face-stabilizer action. Sector identity is read off the edge bits alone; it is never an independent label.
background
The EdgeSectorBridge module settles two combinatorial facts from a panel verdict on SectorAreaQuantization: whether a sector is a free-standing degree of freedom or only a quotient of edge bits, and whether ledger closure leaves 3 free bits out of 4. The live substrate is PixelLocal edge bits on a face; a FaceCfg is those four bits. Ledger-closed configs are those whose XOR parity constraint holds.
The dihedral group $D_4$ acts by permuting which vertex holds which bit. A sector representative is the canonical (numerically least) element of a $D_4$-orbit, matching the isSectorRep criterion used elsewhere. Admissible sectors are the closed configs that are already those orbit minima.
Module honesty: these facts kill $H + \log 4$ as double-counting (sector adds no information beyond edges) but do not choose between $4H$ and $3H$ as the physical pixel-area formula, nor prove that one edge equals one independent T9 event.
proof idea
Definition, not a proof. Map the face stabilizer through the action on $c$, then foldr with min, seeded at $c$. The result is the least orbit element in the ambient order on FaceCfg. Totality and computability are immediate from finiteness of the stabilizer.
why it matters
This is the constructive witness that sector identity is a deterministic function of raw edge bits. Downstream, sectorOf_mem_admissibleSectors (by decide) shows closed configs land in admissibleSectors, and sectorOf_surjective_on_closed shows every admissible sector is hit: together, admissible sectors are exactly the image of closed configs under this map. EdgeSectorBridgeCert bundles free_bits_three, well-definedness, surjectivity, and the exactly-2-to-1 lossy quotient (8 closed configs, 4 sectors).
That certificate is what kills treating the sector as an independent $\log 4$ addend on top of edge entropy. The live candidates move to the edge substrate ($4H$ pre-closure or $3H$ post-closure). Also used in mass-ladder bookkeeping (electron Z via ZOf/sectorOf in the fermion anchor path), though that Anchor.sectorOf is a separate fermion-to-sector table reusing the name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.