Holography Cell Injection Face Flip Invisible Everywhere

The invisible flip

A cube with one binary digit, a 0 or a 1, stored at each of its eight corners. A boundary record reads six face parities, one per face, where a face parity is the exclusive-or of its four corner bits. The question is which changes to the interior bits can be detected from the boundary. The answer, proved by exhaustive case check in the framework's machine-checked library of formal theorems, is a sharp dichotomy: every single corner flip changes the record, and it changes exactly three of the six face parities, but some multi-bit flips are completely invisible.

The invisible moves are exactly the whole-face flips: take the four bits on one face and invert all of them. From any starting configuration, the boundary record after such a flip is identical to the record before it. The theorem face_flip_invisible_everywhere states this universally: for every one of the 256 possible corner-bit configurations, flipping the four bits of a face leaves all six face parities unchanged. One such flip, the face with bits 0, 1, 2, 3, is the configuration 15, and the theorem proves that adding it to any configuration via exclusive-or never alters the record.

This invisibility is not a loophole that lets small changes slip through. The same library proves that any two configurations with the same boundary record must differ on at least four of the eight corners, half the cube. A whole-face flip has weight exactly four, so it sits precisely at that lower bound: it is the smallest possible invisible change. The set of all invisible moves forms a subgroup of 16 configurations, generated by the six whole-face flips, and it includes the global complement (flipping all eight bits) and two inscribed tetrahedra. The record map sends 256 configurations to only 16 distinct records, and the kernel has size 16, so the image and the kernel each account for exactly half the space.

In Recognition Science, this cell is the forced 8-tick structure in three dimensions, and the boundary record is what the ledger closure posts. The result sharpens the complementarity question: on this cell, the question of whether every bulk distinction has a boundary witness reduces from a statement about all 256 states to a statement about 16 explicit global parity moves. The framework proves that these moves are the only blind ones, but it does not prove they are gauge, meaning it does not prove they are unperformed distinctions. That identification remains a modeling choice, not a theorem.

/-- The bound is tight, and blindness is base-independent: one whole-face flip
(weight 4) leaves the boundary record unchanged from EVERY configuration. -/
theorem face_flip_invisible_everywhere :
    ∀ c : CellCfg, faceRecord (xorCfg c faceFlip) = faceRecord c := by decide

/-- **THE CELL-INJECTION TEST (the panel's question, answered positively for local
moves).** Flipping any single vertex bit of the D=3 cell changes the boundary record,
from every configuration. No single bulk distinction is unrecorded. -/
theorem single_flip_posts :
    ∀ (c : CellCfg) (i : Fin 8), faceRecord (flipv c i) ≠ faceRecord c := by decide

/-- Sharper: a single vertex flip changes EXACTLY three of the six face records — the
three faces incident to that vertex. The posting is local and quantized. -/
theorem single_flip_posts_three :
    ∀ (c : CellCfg) (i : Fin 8),
      (List.zipWith (fun a b => a != b) (faceRecord (flipv c i)) (faceRecord c)).count
        true = 3 := by decide

/-- **THE DICHOTOMY (the module's headline).** Any two distinct bulk configurations
with the SAME boundary record differ on at least 4 of the 8 vertices, half the cell.
Together with `single_flip_posts`: the record misses nothing local; what it misses is
exactly a 4-bit group of cell-global parity moves. -/
theorem record_blind_only_global :
    ∀ c c' : CellCfg, faceRecord c = faceRecord c' → c ≠ c' →
      4 ≤ weight (xorCfg c c') := by decide

theorem recordKernel_card : recordKernel.card = 16 := by decide

/-- The blind set, explicitly: the rank-4 GF(2) group generated by the six whole-face
flips (`15, 51, 85, ...`), containing the global complement `255` and the two
inscribed tetrahedra `105 = {0,3,5,6}` and `150 = {1,2,4,7}`. -/
theorem recordKernel_eq :
    recordKernel =
      ({0, 15, 51, 60, 85, 90, 102, 105, 150, 153, 165, 170, 195, 204, 240, 255} :
        Finset CellCfg) := by decide

What this page does not claim

The theorem does not claim that the 16 invisible moves are gauge, only that they are the only blind ones. It does not claim that every bulk distinction posts a boundary witness; that complementarity premise remains an axiom. It does not claim anything about cells with different shapes or dimensions than the forced cube.

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/CellInjection.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: