Holography Edge Sector Bridge Closed Configs

The closed edge configurations

In the Recognition Science framework, a boundary pixel is described by four raw edge bits, a small digital record of which sides of the pixel touch the boundary. A ledger, a discrete record of events, imposes a closure constraint: the parity, or XOR sum, of these four bits must be zero. The declaration closedConfigs defines the set of all four-bit strings that satisfy this parity constraint, before any further grouping into sectors is applied.

The central theorem, closed_configs_card, proves by exhaustive computation that exactly 8 of the 16 possible four-bit strings satisfy the constraint. This is restated as closed_free_bits, which shows the count equals 2³, meaning the parity constraint removes exactly one degree of freedom from the four raw bits, leaving three independent bits. This is a purely combinatorial fact, verified by the machine-checked library of formal theorems.

This count matters because it adjudicates a live dispute in the framework. One proposal for the entropy of a pixel area was H + log 4, treating the pixel's sector label as an independent piece of information. The theorem sector_is_lossy_quotient_of_closed proves that the sector label is a 2-to-1 lossy quotient of the eight closed configurations, carrying only log 4 = 2 log 2 bits of information, strictly less than the log 8 = 3 log 2 bits of the closed edges. Since the sector is entirely determined by the edge bits, adding an independent log 4 term double-counts information. This kills the H + log 4 candidate area law.

What closedConfigs does not claim is equally precise. It does not decide whether the physically correct pixel-area formula is 4H (using raw pre-closure capacity) or 3H (using post-closure realized information). That remains an open physical question about which substrate the area attaches to. It also does not prove that one edge equals one independent recognition event; that identification is an unformalized physical assertion. The declaration only settles the combinatorial facts: the count is 8, and the sector adds no independent information.

/-- The ledger-closed boundary configurations: the 4 raw edge bits satisfying the
parity (ledger-closure) constraint, **before** any `D₄` quotient is taken. This is the
pre-closure edge substrate that the live `4H`/`3H` fork is about. -/
def closedConfigs : Finset FaceCfg := Finset.univ.filter (fun c => closed c = true)

/-- **THEOREM (axiom-clean, by `decide`).** Exactly `8 = 2³` ledger-closed edge
configurations out of the 16 raw configurations: the parity constraint removes exactly
one of the 4 raw edge-bits' degrees of freedom. -/
theorem closed_configs_card : closedConfigs.card = 8 := by decide

/-- **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

What this page does not claim

The declaration does not prove that one edge corresponds to one independent recognition event. The declaration does not resolve whether the pixel area formula should be 4H or 3H. The declaration does not apply to a shared-vertex lattice, where the count may differ.

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: