Holography Pixel Glued Plaquette Domino Stabilizer

The domino stabilizer

A stabilizer is a symmetry group: the set of transformations that leave an object looking the same. For a 2×1 domino, a rectangle twice as long as it is wide, the symmetry group has four elements: doing nothing, flipping it horizontally, flipping it vertically, and rotating it 180 degrees. This group is called the Klein four-group. The declaration dominoStabilizer lists exactly those four vertex permutations as the definition of this symmetry group for a six-vertex grid.

The framework's recognition sector count, a discrete record of balanced configurations, is not additive over area. A single square face carries exactly 4 sectors. Two faces glued along an edge, a domino with twice the area, carry exactly 9 sectors, not 8. The theorem glued_sector_count proves this by exhaustive computation: 9 = 2·4 + 1, where the extra 1 is the boundary correction from the shared edge. This is super-additivity, and it means the per-face integer 4 is not an area density coefficient.

This result settles a live bet against the count-to-area ansatz, the tempting idea that sector count scales with area. It does not refute the framework; the single-face count of 4 remains a theorem. It shows that identifying that integer as an area coefficient is a genuine modeling step, not a consequence of the enumeration. The count is not extensive, so closing the gap cannot route through "the count IS the area."

The theorems are machine-checked and axiom-clean, relying only on the standard three axioms of the ambient type theory. Every theorem is proved by decide, meaning exhaustive computation over the finite configuration space. The explicit nine orbit minima are {0, 7, 9, 14, 18, 21, 27, 45, 63}.

/-- **The domino stabilizer** = the Klein four-group of the 2×1 rectangle: identity,
horizontal mirror `(0 2)(3 5)`, vertical mirror `(0 3)(1 4)(2 5)`, 180° rotation
`(0 5)(1 4)(2 3)`, as permutations of the 6 vertices. -/
def dominoStabilizer : List (Fin 6 → Fin 6) :=
  [ ![0, 1, 2, 3, 4, 5], ![2, 1, 0, 5, 4, 3], ![3, 4, 5, 0, 1, 2], ![5, 4, 3, 2, 1, 0] ]

/-- **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 declaration does not claim the sector count is a physical area density. It does not claim the framework is refuted by the super-additivity result. It does not claim the single-face count of 4 is derived from the domino construction.

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: