Holography Pixel Glued Plaquette Admissible Sectors

The glued sector count

In the Recognition Science framework, a recognition sector is an equivalence class of discrete configurations that a system's ledger treats as the same state. The declaration admissibleSectors in the framework's machine-checked library of formal theorems defines the set of such sectors for a specific small object: a 2×1 domino made of two square faces sharing an edge. Each face has four vertices, and a configuration assigns a recognition bit to each of the six vertices of the domino. A configuration is closed when both faces post a balanced loop, meaning the four bits on each face XOR to zero. The stabilizer, the symmetry group of the rectangle, is the Klein four-group, and a sector is counted by its canonical, numerically smallest representative under that group.

The declaration itself is a definition, but it supports a proved theorem: the glued domino carries exactly 9 sectors, not 8. The single face carries 4 sectors, so a naive area-additive guess would predict 8 for twice the area. The machine-checked result, glued_sector_count, shows the count is 9, and the companion theorem glued_super_additive states this as 9 = 2·4 + 1, where the +1 is a boundary correction from the shared edge. This is evidence against the idea that the per-pixel sector count is an area density. The integer 4 per face remains a theorem, but it is not a multiplicative area coefficient in the extensive sense.

What the declaration does not claim is just as important. It does not refute the framework; the single-face count of 4 is still proved. It does not establish that the sector count is additive, and it does not identify the per-pixel integer with any physical area constant. The finding is negative: the count is super-additive, so treating it as an area coefficient is a genuine modeling choice, not a consequence of the enumeration. This closes a specific open question, GAP 1, by showing that the count-to-area ansatz cannot be routed through a simple multiplicative coefficient.

/-- **THEOREM (axiom-clean, by `decide`). The glued 2×1 domino carries exactly 9
recognition sectors** — NOT `2 · 4 = 8`. -/
theorem glued_sector_count : admissibleSectors.card = 9 := by decide

/-- **The sector count is super-additive (the LB1 finding).** Two faces glued along an
edge give `9 = 2·4 + 1`, where `4` is the single-face count
(`PixelLocal.recognition_sector_count`) and the `+1` is the shared-edge correction. The
count is therefore NOT an extensive area density: the per-pixel integer `4` is not the
area coefficient in the additive sense. -/
theorem glued_super_additive :
    admissibleSectors.card = 2 * PixelLocal.admissibleSectors.card + 1 := by decide

/-- **The sector count is super-additive (the LB1 finding).** Two faces glued along an
edge give `9 = 2·4 + 1`, where `4` is the single-face count
(`PixelLocal.recognition_sector_count`) and the `+1` is the shared-edge correction. The
count is therefore NOT an extensive area density: the per-pixel integer `4` is not the
area coefficient in the additive sense. -/
theorem glued_super_additive :
    admissibleSectors.card = 2 * PixelLocal.admissibleSectors.card + 1 := by decide

What this page does not claim

The declaration does not claim that the 2×1 domino has 8 sectors. The declaration does not claim that the sector count is additive or extensive. The declaration does not claim that the per-face integer 4 is an area coefficient in any physical sense.

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/PixelGluedPlaquette.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: