Holography Edge Sector Bridge Sector Is Lossy Quotient Of Closed

The sector as a projection

In the Recognition Science framework's holographic boundary model, a boundary pixel has four raw edge bits, and a sector is a label that groups configurations related by a symmetry. The framework's machine-checked library of formal theorems proves that the sector label is a deterministic, lossy quotient of the edge bits: it is a projection that discards information, never a free-standing quantity added on top of the edges. The theorem sector_is_lossy_quotient_of_closed states that the number of admissible sectors times two equals the number of ledger-closed edge configurations, an exactly 2-to-1 compression.

The proof rests on two combinatorial facts, each checked by exhaustive finite computation. First, the ledger-closure parity constraint removes exactly one of the four raw edge bits' degrees of freedom: there are 8 = 2³ closed configurations out of 16 raw ones. Second, the sector map is total, deterministic, and surjective onto the four admissible sectors, meaning every sector is reached from some closed configuration, and every closed configuration maps to exactly one sector. Because the sector is recoverable from a strict compression of the edge bits, the closed-edge substrate carries log 8 of information while the sector carries only log 4, exactly half.

The consequence is a double-count kill. A proposed area law adding an independent entropy term for the sector on top of a per-edge entropy, written H + log 4, treats the sector as if it carried information the edges do not already contain. The theorem shows this is false: the sector adds no independent information, so the additive term double-counts. The live candidates for the physically correct pixel-area formula move to the edge substrate itself, either the pre-closure capacity 4H or the post-closure realized information 3H.

What the theorem does not decide is which of those two candidates is physically correct. The choice between 4H and 3H depends on which substrate the pixel area actually attaches to, a physical question the combinatorial facts sharpen but do not resolve. Nor does the theorem establish that one edge equals one independent recognition event; that identification remains an unformalized physical assertion. The module also leaves open whether the count 3 survives for an entangling surface, where a shared-vertex lattice model may force a different value between 1 and 2.5.

/-- **The double-count kill (by `decide`).** The closed-edge substrate carries `log 8`
of information; the sector quotient carries only `log 4`, exactly half. Since sector
identity is entirely recoverable from (a strict compression of) the edge bits, adding
an independent `log 4` term on top of a per-edge entropy `H` double-counts information
the edges already contain. This is the precise combinatorial content behind killing
`H + log 4` as a candidate area law: `admissibleSectors` is a 2-to-1 lossy quotient of
`closedConfigs`, not a free-standing degree of freedom. -/
theorem sector_is_lossy_quotient_of_closed :
    admissibleSectors.card * 2 = closedConfigs.card := by decide

/-- **Restated as "3 free bits."** Ledger closure on 4 raw edge-bits leaves exactly 3
independent bits, not 4. This is the fact the `4H` vs `3H` live bet hinges on: if pixel
area tracks *realized* (post-closure) information, the count is 3; if it tracks *raw*
(pre-closure) capacity, the count is 4. -/
theorem closed_free_bits : closedConfigs.card = 2 ^ 3 := closed_configs_card

/-- **THEOREM (surjectivity, by `decide`). Sectors carry no information beyond the
edge bits.** Every one of the 4 admissible sectors is hit by `sectorOf` from some
ledger-closed edge configuration. Combined with `sectorOf_mem_admissibleSectors`, this
proves `admissibleSectors` is exactly the image of `closedConfigs` under a
deterministic quotient map — a sector is a *projection* of the edges, never an
independent quantity added on top of them. -/
theorem sectorOf_surjective_on_closed :
    admissibleSectors ⊆ closedConfigs.image sectorOf := by decide

What this page does not claim

The physically correct pixel-area formula is 4H or 3H. One edge equals one independent recognition event. The count 3 applies to entangling surfaces with shared vertices.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/EdgeSectorBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: