EdgeSectorBridgeCert
plain-language theorem explainer
A Prop-valued certificate packaging four combinatorial facts: ledger-closed face configs number exactly $2^3=8$; the sector-of-edges map sends closed configs into the admissible sectors; it hits every admissible sector; and the map is exactly two-to-one. Anyone adjudicating whether sector-area quantization is independent physics cites this bundle. It is a structure definition, inhabited by wiring four decide-proved lemmas.
Claim. A proposition asserting: (i) the set of ledger-closed face configurations has cardinality $2^3$; (ii) every closed face configuration is sent by the sector-of-edges map into the admissible sectors; (iii) every admissible sector is the image of some closed configuration under that map; (iv) twice the number of admissible sectors equals the number of closed configurations (exactly two-to-one).
background
In the pixel-local holography layer, a face configuration is four raw boundary (edge) bits on a cube face. Ledger closure is even parity of those bits: the XOR of the four vertex bits vanishes, so a closed recognition loop posts a balanced ledger around the face. The closed configurations are exactly the members of the universe filtered by that parity predicate; they form the pre-quotient edge substrate behind the live $4H$ versus $3H$ fork.
A sector is not an extra label. The sector-of-edges map sends each face config to the numerically least element of its $D_4$-orbit (the face stabilizer of the square). Admissible sectors are the closed configs that are already canonical orbit representatives. The module setting records a panel verdict that killed treating sectors as free-standing degrees of freedom and relocated the live candidate one layer down, to the edge bits themselves.
Upstream, the closed-config set is defined by filtering on parity; the sector map is a total fold of the stabilizer action; well-definedness and surjectivity onto admissible sectors are decide-checked; and the closed count is $8=2^3$.
proof idea
No proof body: this is a structure definition whose type is Prop. Four fields name the adjudicating equalities and inclusions. The unique inhabiting instance (edgeSectorBridgeCert) fills them by direct application of the four sibling lemmas: free-bit count from the closed-config cardinality theorem; well-definedness from membership of sector images in admissible sectors; surjectivity from the image-containment lemma on closed configs; and the two-to-one count from the lossy-quotient cardinality identity. Each of those lemmas is itself a decide (or thin wrapper around one).
why it matters
This certificate is what the panel asked for before any measure-theoretic work on edge-versus-T9 identification. It settles, by direct construction, that the sector is a deterministic lossy quotient of the edges: closed edges carry $\log 8 = 3\log 2$, sectors carry only $\log 4 = 2\log 2$, and the map is exactly two-to-one. Consequently $H + \log 4$ (entropy-per-event plus an independent sector label) double-counts and is dead.
The sole downstream consumer is the inhabiting theorem that assembles the four field proofs. Framework-wise this sits in the holography stack under the $D=3$ forced lattice (T8) and the eight-tick octave (T7) background: four raw edge bits, one parity constraint, $D_4$ orbits. It does not choose between the remaining live candidates $4H$ (pre-closure capacity) and $3H$ (post-closure realized information); it only sharpens that fork and closes the sector-only reading for good.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.