IndisputableMonolith.Holography.PixelLocal

   1import Mathlib.Data.Fin.VecNotation
   2import Mathlib.Data.Fintype.Pi
   3import Mathlib.Data.Fintype.Prod
   4import Mathlib.Data.Finset.Card
   5
   6/-!
   7# PixelLocal: the forced recognition-sector count on the D=3, 8=2³ lattice
   8
   9The RS holography panel (2026-06-29/30) split the recognition-pixel area
  10`a_pix = 4 · H · ℓ_P²` into three quantities that must be derived **separately**:
  11the integer `4`, the per-event entropy `H = (φ+2) log φ`, and the area scale `ℓ_P²`.
  12`H` is already a theorem (`RecognitionEventCapacity.forcedEntropy`); `ℓ_P²` is blocked
  13by a scale-invariance no-go (`Consciousness.PixelScaleNoGo`). This module attacks the
  14remaining quantity, the integer, on the **actually forced discrete substrate** rather
  15than by importing continuum isotropy or any Bekenstein-Hawking input.
  16
  17## The greenlit construction
  18
  19The forced 8-tick cell in D=3 is the cube `2³`: 8 vertices, 6 faces. A **boundary
  20recognition pixel** is one cube face, a square plaquette with 4 vertices. Put one
  21recognition bit on each vertex (`Fin 16` = the 4 low bits). The forced substrate
  22contributes exactly two structures, and nothing else:
  23
  24* **Ledger closure.** A closed recognition loop posts a balanced (zero-sum) ledger
  25  around the plaquette, so the 4 vertex bits XOR to 0 (even parity). This is the only
  26  admissibility condition, and it comes from the recognition ledger, not from geometry.
  27* **The face stabilizer.** Two boundary configurations that differ only by a symmetry
  28  of the square are the same physical sector, so we quotient by the square's symmetry
  29  group `D₄` (4 rotations + 4 reflections, the 8 elements that fix the plaquette).
  30
  31`card(AdmissibleBoundarySectors / FaceStabilizer)` is then a finite, `decide`-able
  32number. **It comes out to exactly 4** — the four orbits are the empty loop `0000`, the
  33two adjacent-edge loops modulo rotation, the two diagonal loops, and the full loop
  34`1111`. That is `2^(D-1) = 2² = 4` realized concretely on the forced lattice.
  35
  36## What this proves, and what it does not (honest scope)
  37
  38THEOREM (axiom-clean): the count is 4. No `H`, no `ℓ_P`, no area quantity appears in
  39any definition here; the result is pure plaquette combinatorics on the forced 8 = 2³
  40substrate. This is the substrate-native realization of the geometric coefficient the
  41paper writes as `4`.
  42
  43OPEN (deliberately not proved here, two distinct gaps the panel flagged):
  441. **Count → area-coefficient link.** Many cube invariants equal 4 in D=3 (edges per
  45   face, transverse DOF, `χ·2`). That this *sector* count is the *area* coefficient in
  46   `a_pix = c · H · ℓ_P²` is a separate argument, not the enumeration.
  472. **The length scale `ℓ_P²`.** Provably unreachable from the current dimensionless
  48   theorem data (`Consciousness.PixelScaleNoGo.area_not_fixed_by_dimensionless`); a new
  49   forced J-cost / action normalization carrying a length is required first.
  50
  51So this module supplies the forced integer and nothing more. It does not let anyone
  52claim a "derived Bekenstein 1/4"; it closes the integer leg of the three-leg split and
  53points the autonomous loop at the two remaining legs.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Holography
  58namespace PixelLocal
  59
  60/-- A boundary plaquette configuration: one recognition bit on each of the 4 vertices
  61of a cube face, packed into the 4 low bits of a `Fin 16`. -/
  62abbrev FaceCfg := Fin 16
  63
  64/-- Vertex bit `i ∈ Fin 4` of a face configuration. -/
  65def vbit (c : FaceCfg) (i : Fin 4) : Bool := Nat.testBit c.val i.val
  66
  67/-- **Ledger closure** on the plaquette: the 4 vertex bits XOR to 0 (even parity).
  68A closed recognition loop posts a balanced (zero-sum) ledger around the face. -/
  69def closed (c : FaceCfg) : Bool :=
  70  ! (vbit c 0 ^^ vbit c 1 ^^ vbit c 2 ^^ vbit c 3)
  71
  72/-- **The face stabilizer `D₄`**: the 8 symmetries of the square (4 rotations +
  734 reflections), as permutations of the 4 vertices arranged in cyclic order 0-1-2-3. -/
  74def faceStabilizer : List (Fin 4 → Fin 4) :=
  75  [ ![0, 1, 2, 3], ![1, 2, 3, 0], ![2, 3, 0, 1], ![3, 0, 1, 2],
  76    ![0, 3, 2, 1], ![2, 1, 0, 3], ![1, 0, 3, 2], ![3, 2, 1, 0] ]
  77
  78/-- Act on a face configuration by a vertex permutation, reassembling the 4 bits. -/
  79def actBy (σ : Fin 4 → Fin 4) (c : FaceCfg) : FaceCfg :=
  80  ⟨ ((if vbit c (σ 0) then 1 else 0) + (if vbit c (σ 1) then 2 else 0)
  81      + (if vbit c (σ 2) then 4 else 0) + (if vbit c (σ 3) then 8 else 0)) % 16,
  82    Nat.mod_lt _ (by decide) ⟩
  83
  84/-- A configuration is the canonical representative of its sector iff it is the
  85numerically smallest configuration in its `D₄`-orbit. -/
  86def isSectorRep (c : FaceCfg) : Bool :=
  87  faceStabilizer.all (fun σ => decide (c ≤ actBy σ c))
  88
  89/-- **The admissible boundary sectors of one cube face**: ledger-closed plaquette
  90configurations modulo the face stabilizer `D₄`, counted by canonical representative. -/
  91def admissibleSectors : Finset FaceCfg :=
  92  Finset.univ.filter (fun c => closed c = true ∧ isSectorRep c = true)
  93
  94/-- **THEOREM (axiom-clean, by `decide`). The D=3 forced lattice yields exactly 4
  95recognition sectors per boundary face.**
  96
  97`card(AdmissibleBoundarySectors / FaceStabilizer) = 4 = 2^(D-1)`. No `H`, no `ℓ_P`,
  98no area input enters any definition; the count is pure ledger-closed plaquette
  99combinatorics on the forced 8 = 2³ substrate. -/
 100theorem recognition_sector_count : admissibleSectors.card = 4 := by decide
 101
 102/-- The four sectors are exactly the orbit minima `{0000, 0011, 0101, 1111}`
 103(empty loop, an adjacent-edge loop, a diagonal loop, the full loop). -/
 104theorem admissibleSectors_eq :
 105    admissibleSectors = ({0, 3, 5, 15} : Finset FaceCfg) := by decide
 106
 107/-- The geometric exponent realized: `2^(D-1)` at `D = 3` is the sector count. -/
 108theorem sector_count_eq_two_pow : admissibleSectors.card = 2 ^ (3 - 1) := by decide
 109
 110/-- The forced 8-tick cell in D=3 is the cube: `2³ = 8` vertices. -/
 111theorem cube_vertices : Fintype.card (Fin 3 → Bool) = 8 := by decide
 112
 113/-- The cube has 6 faces (an axis together with a side). -/
 114theorem cube_faces : Fintype.card (Fin 3 × Bool) = 6 := by decide
 115
 116end PixelLocal
 117end Holography
 118end IndisputableMonolith
 119