IndisputableMonolith.Holography.PixelGluedPlaquette

   1import Mathlib.Data.Fin.VecNotation
   2import Mathlib.Data.Fintype.Pi
   3import Mathlib.Data.Finset.Card
   4import IndisputableMonolith.Holography.PixelLocal
   5
   6/-!
   7# PixelGluedPlaquette (LB1): the recognition-sector count is NOT area-additive
   8
   9This module settles the panel's first "live bet" (LB1) on GAP 1 (the count→area
  10ansatz). The single boundary pixel (one cube face) carries exactly `4` ledger-closed
  11sectors modulo its `D₄` stabilizer (`PixelLocal.recognition_sector_count`). If that
  12integer were an AREA DENSITY — i.e. if the sector count were the multiplicative
  13coefficient on an extensive area — then a region of TWICE the area should carry twice
  14the count. We test this directly by gluing two faces along a shared edge (a 2×1 domino,
  15twice the area of one face) and enumerating its sectors with the identical machinery.
  16
  17## The construction (parallel to `PixelLocal`)
  18
  19A 2×1 domino has 6 vertices in a 2-row × 3-column grid (top `0 1 2`, bottom `3 4 5`),
  20packed into the 6 low bits of `Fin 64`. It is the union of two unit faces:
  21
  22* left face, cyclic `0-1-4-3`;
  23* right face, cyclic `1-2-5-4` (sharing edge `1-4` with the left face).
  24
  25**Ledger closure** requires BOTH unit faces to post a balanced loop (each face's 4
  26vertex bits XOR to 0). **The stabilizer** is the symmetry group of the 2×1 rectangle,
  27the Klein four-group `Z₂ × Z₂` (identity, horizontal mirror, vertical mirror, 180°
  28rotation) — *not* `D₄`, because the rectangle is not a square. Sectors are counted by
  29canonical (numerically smallest) orbit representative, exactly as in `PixelLocal`.
  30
  31## The finding (machine-checked, axiom-clean)
  32
  33`glued_sector_count`: the domino carries exactly **9** sectors, not `2 · 4 = 8`. The
  34count is **super-additive**: `9 = 2·4 + 1`, the `+1` being the boundary correction from
  35the shared edge. So the sector count does NOT scale as a clean area density; the
  36per-pixel integer `4` is not an area coefficient in the extensive sense.
  37
  38This is evidence AGAINST the count→area ansatz (GAP 1), not for it. It does not refute
  39the framework — the integer `4` per face is still a theorem — but it shows that
  40identifying that integer as the multiplicative area coefficient `a_pix = 4·H·ℓ_P²` is a
  41genuine modeling step, not a consequence of the enumeration. Closing GAP 1 cannot route
  42through "the count IS the area"; the count is not extensive.
  43
  44Axiom-clean (`propext, Classical.choice, Quot.sound`); every theorem is `by decide`.
  45-/
  46
  47namespace IndisputableMonolith
  48namespace Holography
  49namespace PixelGluedPlaquette
  50
  51/-- A glued 2×1 domino configuration: one recognition bit on each of the 6 vertices of a
  522-row × 3-column grid (top `0 1 2`, bottom `3 4 5`), packed into the 6 low bits of a
  53`Fin 64`. -/
  54abbrev DominoCfg := Fin 64
  55
  56/-- Vertex bit `i ∈ Fin 6` of a domino configuration. -/
  57def vbit (c : DominoCfg) (i : Fin 6) : Bool := Nat.testBit c.val i.val
  58
  59/-- **Ledger closure** on the domino: BOTH unit faces post a balanced (zero-sum) ledger
  60loop. Left face `0-1-4-3` even parity AND right face `1-2-5-4` even parity. -/
  61def closed (c : DominoCfg) : Bool :=
  62  (! (vbit c 0 ^^ vbit c 1 ^^ vbit c 4 ^^ vbit c 3)) &&
  63  (! (vbit c 1 ^^ vbit c 2 ^^ vbit c 5 ^^ vbit c 4))
  64
  65/-- **The domino stabilizer** = the Klein four-group of the 2×1 rectangle: identity,
  66horizontal mirror `(0 2)(3 5)`, vertical mirror `(0 3)(1 4)(2 5)`, 180° rotation
  67`(0 5)(1 4)(2 3)`, as permutations of the 6 vertices. -/
  68def dominoStabilizer : List (Fin 6 → Fin 6) :=
  69  [ ![0, 1, 2, 3, 4, 5], ![2, 1, 0, 5, 4, 3], ![3, 4, 5, 0, 1, 2], ![5, 4, 3, 2, 1, 0] ]
  70
  71/-- Act on a domino configuration by a vertex permutation, reassembling the 6 bits. -/
  72def actBy (σ : Fin 6 → Fin 6) (c : DominoCfg) : DominoCfg :=
  73  ⟨ ((if vbit c (σ 0) then 1 else 0) + (if vbit c (σ 1) then 2 else 0)
  74      + (if vbit c (σ 2) then 4 else 0) + (if vbit c (σ 3) then 8 else 0)
  75      + (if vbit c (σ 4) then 16 else 0) + (if vbit c (σ 5) then 32 else 0)) % 64,
  76    Nat.mod_lt _ (by decide) ⟩
  77
  78/-- A configuration is its sector's canonical representative iff it is the numerically
  79smallest configuration in its Klein-4 orbit. -/
  80def isSectorRep (c : DominoCfg) : Bool :=
  81  dominoStabilizer.all (fun σ => decide (c ≤ actBy σ c))
  82
  83/-- **The admissible sectors of the glued 2×1 domino**: ledger-closed (both faces)
  84configurations modulo the rectangle stabilizer, counted by canonical representative. -/
  85def admissibleSectors : Finset DominoCfg :=
  86  Finset.univ.filter (fun c => closed c = true ∧ isSectorRep c = true)
  87
  88/-- **THEOREM (axiom-clean, by `decide`). The glued 2×1 domino carries exactly 9
  89recognition sectors** — NOT `2 · 4 = 8`. -/
  90theorem glued_sector_count : admissibleSectors.card = 9 := by decide
  91
  92/-- **The sector count is super-additive (the LB1 finding).** Two faces glued along an
  93edge give `9 = 2·4 + 1`, where `4` is the single-face count
  94(`PixelLocal.recognition_sector_count`) and the `+1` is the shared-edge correction. The
  95count is therefore NOT an extensive area density: the per-pixel integer `4` is not the
  96area coefficient in the additive sense. -/
  97theorem glued_super_additive :
  98    admissibleSectors.card = 2 * PixelLocal.admissibleSectors.card + 1 := by decide
  99
 100/-- The explicit nine orbit minima of the domino. -/
 101theorem admissibleSectors_eq :
 102    admissibleSectors = ({0, 7, 9, 14, 18, 21, 27, 45, 63} : Finset DominoCfg) := by decide
 103
 104end PixelGluedPlaquette
 105end Holography
 106end IndisputableMonolith
 107