IndisputableMonolith.Holography.CellInjection

   1import Mathlib.Data.Finset.Image
   2import Mathlib.Data.Finset.Card
   3import Mathlib.Data.Fintype.Basic
   4import Mathlib.Data.Fintype.Card
   5import Mathlib.Logic.Function.Defs
   6
   7/-!
   8# CellInjection: the cell-injection test (does a bulk flip necessarily post?)
   9
  10Greenlit as the first step of the entropy-fork program (panel
  11`holo_bigger_discovery_20260702`, judge Fable 5): *flip one interior bit of the D=3
  12cell and check whether the boundary record necessarily changes.* The test is designed
  13to separate two futures for recognition complementarity: if bulk degeneracy is
  14unrecorded (like the boundary fiber degeneracy of `RecordCostAsymmetry.
  15fiber_posts_one_record`), complementarity stays an axiom; if every bulk distinction
  16posts, complementarity moves toward a theorem.
  17
  18## The setup (all forced substrate, no new modeling freedom)
  19
  20The forced 8-tick cell in D=3 is the cube `2³`: 8 vertices, 6 faces
  21(`PixelLocal.cube_vertices`, `PixelLocal.cube_faces`). Put one recognition bit on each
  22vertex (`CellCfg = Fin 256`). The **boundary record** of the cell is what the ledger
  23closure posts: the six face-closure parities (`faceRecord`), one per face, exactly the
  24per-face `PixelLocal.closed` functional read on all six faces of one cell.
  25
  26## The verdict (machine-checked, axiom-clean, all by `decide`)
  27
  28The answer is a sharp dichotomy, not a yes or a no:
  29
  301. **Every local bulk flip posts** (`single_flip_posts`): flipping any single vertex
  31   bit changes the boundary record, from every one of the 256 configurations, and it
  32   changes exactly the three face records incident to that vertex
  33   (`single_flip_posts_three`). No single bulk distinction is unrecorded.
  342. **The record map is nonetheless non-injective** (`record_not_injective`): its
  35   blind set is a rank-4 subgroup of 16 moves (`recordKernel_card`,
  36   `record_nullity_eq_four`), the group generated by whole-face flips
  37   (`recordKernel_eq`), including the global complement and the two inscribed
  38   tetrahedra (`105`, `150`).
  393. **Blindness is only global** (`record_blind_only_global`): any two configurations
  40   with the same boundary record differ on at least 4 of the 8 vertices, half the
  41   cell. The bound is tight: one whole-face flip (weight 4) is invisible from every
  42   base configuration (`face_flip_invisible_everywhere`).
  434. **Rank-nullity of the cell record map**: `|image| = 16 = 2⁴`, `|kernel| = 16 = 2⁴`,
  44   `16 · 16 = 256` (`record_image_times_kernel`). At whole-cell granularity the
  45   record cost (4 posted bits) and the fiber degeneracy (4 free bits) COINCIDE; the
  46   entropy fork of `CoefficientBridge` (rank 1 vs nullity 3 per face; rank 2 vs
  47   nullity 4 on the domino) is a per-face / glued-surface phenomenon, invisible at
  48   the single whole cell.
  49
  50## What this buys for recognition complementarity (honest scope)
  51
  52The complementarity premise of the holography paper ("no bulk distinction exists
  53without a boundary-readable witness") REDUCES, on the forced cell, from a statement
  54about all `2⁸` bulk states to a statement about 16 explicit global parity moves:
  55weak complementarity through the posted record holds iff the whole-face parity flips
  56are recognition gauge. That identification is exactly the record-cost reading again
  57(an unposted move is not a performed distinction), so the fork selector and the
  58complementarity axiom are the SAME choice at cell level, now with the blind set
  59computed and classified rather than postulated. This module does NOT prove the
  6016 moves are gauge; it isolates them.
  61-/
  62
  63namespace IndisputableMonolith
  64namespace Holography
  65namespace CellInjection
  66
  67/- The `decide` proofs below enumerate `Fin 256` (and pairs over it); the derived
  68`Fintype` decidability instances recurse once per element, so the default
  69`maxRecDepth 512` and heartbeat budget are far too small. Raising them changes
  70nothing about trust: the kernel still checks every case. -/
  71set_option maxRecDepth 100000
  72set_option maxHeartbeats 4000000
  73
  74/-- A full-cell configuration: one recognition bit on each of the `8 = 2³` vertices of
  75the forced D=3 cell, packed into `Fin 256`. Vertex `v ∈ Fin 8` has coordinate bits
  76`(v&1, v&2, v&4)`. -/
  77abbrev CellCfg := Fin 256
  78
  79/-- Vertex bit `i ∈ Fin 8` of a cell configuration. -/
  80def vbit (c : CellCfg) (i : Fin 8) : Bool := Nat.testBit c.val i.val
  81
  82/-- Ledger-closure record of one face with vertices `i j k l`: the four bits XOR to 0
  83(even parity), i.e. the closed-loop condition of `PixelLocal.closed`, negated XOR. -/
  84def closedOn (c : CellCfg) (i j k l : Fin 8) : Bool :=
  85  ! (vbit c i ^^ vbit c j ^^ vbit c k ^^ vbit c l)
  86
  87/-- **The boundary record of the cell**: the six face-closure parities, one per cube
  88face (axis, side), each face collecting the four vertices whose axis-bit equals the
  89side. This is everything the ledger closure posts at the cell boundary. -/
  90def faceRecord (c : CellCfg) : List Bool :=
  91  [ closedOn c 0 2 4 6   -- x = 0
  92  , closedOn c 1 3 5 7   -- x = 1
  93  , closedOn c 0 1 4 5   -- y = 0
  94  , closedOn c 2 3 6 7   -- y = 1
  95  , closedOn c 0 1 2 3   -- z = 0
  96  , closedOn c 4 5 6 7 ] -- z = 1
  97
  98/-- Flip vertex `i` of configuration `c`. -/
  99def flipv (c : CellCfg) (i : Fin 8) : CellCfg :=
 100  ⟨(c.val ^^^ (1 <<< i.val)) % 256, Nat.mod_lt _ (by decide)⟩
 101
 102/-- Bitwise XOR of two configurations (the move taking one to the other). -/
 103def xorCfg (c d : CellCfg) : CellCfg :=
 104  ⟨(c.val ^^^ d.val) % 256, Nat.mod_lt _ (by decide)⟩
 105
 106/-- Hamming weight: how many of the 8 vertex bits are set. -/
 107def weight (c : CellCfg) : ℕ := (List.finRange 8).countP (fun i => vbit c i)
 108
 109/-- The empty cell. -/
 110def cell0 : CellCfg := ⟨0, by decide⟩
 111
 112/-- The global complement (all 8 vertex bits flipped). -/
 113def cellComplement : CellCfg := ⟨255, by decide⟩
 114
 115/-- One whole-face flip: the four vertices of the `z = 0` face (`{0,1,2,3}`). -/
 116def faceFlip : CellCfg := ⟨15, by decide⟩
 117
 118/-! ## 1. The injection test: every local bulk flip posts -/
 119
 120/-- **THE CELL-INJECTION TEST (the panel's question, answered positively for local
 121moves).** Flipping any single vertex bit of the D=3 cell changes the boundary record,
 122from every configuration. No single bulk distinction is unrecorded. -/
 123theorem single_flip_posts :
 124    ∀ (c : CellCfg) (i : Fin 8), faceRecord (flipv c i) ≠ faceRecord c := by decide
 125
 126/-- Sharper: a single vertex flip changes EXACTLY three of the six face records — the
 127three faces incident to that vertex. The posting is local and quantized. -/
 128theorem single_flip_posts_three :
 129    ∀ (c : CellCfg) (i : Fin 8),
 130      (List.zipWith (fun a b => a != b) (faceRecord (flipv c i)) (faceRecord c)).count
 131        true = 3 := by decide
 132
 133/-! ## 2. The record map is not injective: the blind set -/
 134
 135/-- The global complement posts nothing: flipping all 8 vertices leaves every face
 136parity unchanged (each face has 4 flipped vertices, an even number). -/
 137theorem complement_invisible : faceRecord cellComplement = faceRecord cell0 := by decide
 138
 139/-- **The boundary record map is NOT injective on raw bulk states.** The countermodel
 140of the holography paper survives at cell level unless record-equal states are
 141physically identified. -/
 142theorem record_not_injective : ¬ Function.Injective faceRecord := fun h =>
 143  absurd (h complement_invisible) (by decide)
 144
 145/-- The **record kernel**: configurations sharing the empty cell's boundary record
 146(all six faces closed). These are the record-invisible states. -/
 147def recordKernel : Finset CellCfg :=
 148  Finset.univ.filter (fun c => faceRecord c = faceRecord cell0)
 149
 150theorem recordKernel_card : recordKernel.card = 16 := by decide
 151
 152/-- The blind set, explicitly: the rank-4 GF(2) group generated by the six whole-face
 153flips (`15, 51, 85, ...`), containing the global complement `255` and the two
 154inscribed tetrahedra `105 = {0,3,5,6}` and `150 = {1,2,4,7}`. -/
 155theorem recordKernel_eq :
 156    recordKernel =
 157      ({0, 15, 51, 60, 85, 90, 102, 105, 150, 153, 165, 170, 195, 204, 240, 255} :
 158        Finset CellCfg) := by decide
 159
 160/-! ## 3. Rank-nullity of the cell record map -/
 161
 162theorem record_image_card : (Finset.univ.image faceRecord).card = 16 := by decide
 163
 164/-- Record rank of the whole cell: 4 posted bits (`log₂ 16`). -/
 165theorem record_rank_eq_four :
 166    Nat.log2 (Finset.univ.image faceRecord).card = 4 := by decide
 167
 168/-- Record nullity of the whole cell: 4 free bits (`log₂ 16`). At whole-cell
 169granularity rank = nullity; the entropy fork splits only per face and under gluing. -/
 170theorem record_nullity_eq_four : Nat.log2 recordKernel.card = 4 := by decide
 171
 172/-- First-isomorphism check of the actual cell record map:
 173`|image| · |kernel| = |domain|` (`16 · 16 = 256`). -/
 174theorem record_image_times_kernel :
 175    (Finset.univ.image faceRecord).card * recordKernel.card = 256 := by decide
 176
 177/-! ## 4. The dichotomy: blindness is only global -/
 178
 179/-- **THE DICHOTOMY (the module's headline).** Any two distinct bulk configurations
 180with the SAME boundary record differ on at least 4 of the 8 vertices, half the cell.
 181Together with `single_flip_posts`: the record misses nothing local; what it misses is
 182exactly a 4-bit group of cell-global parity moves. -/
 183theorem record_blind_only_global :
 184    ∀ c c' : CellCfg, faceRecord c = faceRecord c' → c ≠ c' →
 185      4 ≤ weight (xorCfg c c') := by decide
 186
 187/-- The bound is tight, and blindness is base-independent: one whole-face flip
 188(weight 4) leaves the boundary record unchanged from EVERY configuration. -/
 189theorem face_flip_invisible_everywhere :
 190    ∀ c : CellCfg, faceRecord (xorCfg c faceFlip) = faceRecord c := by decide
 191
 192theorem faceFlip_weight : weight faceFlip = 4 := by decide
 193
 194/-- Shift-invariance classifies blindness exactly: a move `d` is invisible from every
 195base iff `d` lies in the record kernel. The 16 kernel elements are the complete list
 196of unrecorded bulk moves. -/
 197theorem invisible_iff_kernel :
 198    ∀ d : CellCfg,
 199      (∀ c : CellCfg, faceRecord (xorCfg c d) = faceRecord c) ↔ d ∈ recordKernel := by
 200  decide
 201
 202/-! ## 5. Bundled target + certificate handle -/
 203
 204/-- **The cell-injection bundle.** Every local flip posts (on exactly three faces);
 205the record map is non-injective with a 16-element blind group; rank·nullity checks;
 206and blindness is only global (minimum invisible weight 4). -/
 207def target_cell_injection : Prop :=
 208  (∀ (c : CellCfg) (i : Fin 8), faceRecord (flipv c i) ≠ faceRecord c)
 209  ∧ (∀ (c : CellCfg) (i : Fin 8),
 210      (List.zipWith (fun a b => a != b) (faceRecord (flipv c i)) (faceRecord c)).count
 211        true = 3)
 212  ∧ ¬ Function.Injective faceRecord
 213  ∧ recordKernel.card = 16
 214  ∧ (Finset.univ.image faceRecord).card * recordKernel.card = 256
 215  ∧ (∀ c c' : CellCfg, faceRecord c = faceRecord c' → c ≠ c' →
 216      4 ≤ weight (xorCfg c c'))
 217
 218theorem target_cell_injection_holds : target_cell_injection :=
 219  ⟨single_flip_posts, single_flip_posts_three, record_not_injective,
 220   recordKernel_card, record_image_times_kernel, record_blind_only_global⟩
 221
 222/-- Verify-target certificate handle for the holography loop (`#print axioms`-gated). -/
 223theorem cellInjectionCert : target_cell_injection := target_cell_injection_holds
 224
 225end CellInjection
 226end Holography
 227end IndisputableMonolith
 228