Holography Pixel Glued Plaquette Closed

The domino ledger

A ledger is a discrete record of events. In this framework, each vertex of a grid carries one recognition bit, a single mark of whether an event is recorded there. A closed ledger is one where every unit face, a square of four vertices, posts a balanced loop: the four bits on that face must sum to zero modulo two. A single square face has exactly four such balanced states, once you identify states that differ only by the square's symmetries.

Now glue two faces along a shared edge to make a 2 by 1 domino. The domino has six vertices, not eight, because the two faces share two vertices along the edge. The ledger closure condition now requires both faces to be balanced. The symmetry group is no longer the square's eight symmetries but the rectangle's four: identity, horizontal mirror, vertical mirror, and 180 degree rotation. Counting balanced states modulo these symmetries gives exactly nine, not the eight you would get by doubling the single-face count of four.

The machine-checked library of formal theorems proves this directly. The theorem glued_sector_count states that the admissible sectors of the glued domino number exactly 9. A companion theorem, glued_super_additive, records the relationship as 9 equals 2 times 4 plus 1. The extra 1 is the boundary correction from the shared edge. This is a proved result, checked by computation, with no unproved assumptions beyond the standard logical axioms.

The finding is evidence against a specific modeling idea, not against the framework itself. The idea was that the per-face integer 4 behaves like an area density, a multiplicative coefficient on an extensive area. If it did, a region of twice the area would carry twice the count. The domino shows this fails: twice the area gives 9, not 8. The integer 4 per face remains a theorem, but identifying it as an area coefficient is a genuine modeling step, not a consequence of the enumeration.

What this changes is the route available for closing a known gap in the framework. The count to area ansatz cannot proceed by asserting the count simply is the area. The count is not extensive. Any future derivation of area from recognition sectors must account for boundary corrections of this kind, where glued edges add states rather than multiply them.

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

What this page does not claim

The integer 4 per face is an area coefficient in the extensive sense. The count to area ansatz is refuted by this finding. Any claim about physical area or Planck length follows from the sector count alone.

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: