Holography Cell Injection Invisible Iff Kernel

The cell-injection test

Consider a cube with one binary bit stored at each of its eight corners. A boundary record summarizes the cube by reading, on each of its six faces, whether the four corner bits on that face satisfy an even-parity condition. The question is whether an internal change, a flip of one or more corner bits, can go undetected by this record. The answer, proved by exhaustive computation over all 256 configurations, is a sharp dichotomy: every single-bit flip changes the boundary record, yet some multi-bit flips do not.

Flipping any one corner bit always changes the record, and it changes exactly the three faces that meet at that corner. No single internal distinction is invisible. The surprise is that the record map is still not one-to-one. Sixteen distinct 8-bit configurations, including the global complement that flips all eight bits, share a boundary record with the all-zero configuration. These blind spots form a closed group: they are precisely the moves generated by flipping entire faces of the cube, and each such move changes at least four bits. Any two configurations that look identical from the boundary differ in at least half the cell, so blindness is never a small local edit.

The declaration invisible_iff_kernel states this classification exactly: a move is invisible from every configuration if and only if it belongs to that 16-element kernel. The proof is a direct computation, and the result is packaged with its supporting facts, including the rank-nullity identity that the record image and the kernel each have size 16, whose product is the full 256 configuration space.

In Recognition Science, this result sharpens a central premise. The framework models physical structure as a ledger, a discrete record of events, and asks whether every internal distinction must leave a boundary-readable witness. The cell-injection theorem reduces that question, for the forced three-dimensional cell, from a statement about all 256 bulk states to a statement about 16 explicit global parity moves. It does not prove those moves are unobservable in principle; it isolates them as the only candidates, turning a philosophical axiom into a finite, checkable list.

/-- 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

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

/-- The global complement posts nothing: flipping all 8 vertices leaves every face
parity unchanged (each face has 4 flipped vertices, an even number). -/
theorem complement_invisible : faceRecord cellComplement = faceRecord cell0 := 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

/-- Shift-invariance classifies blindness exactly: a move `d` is invisible from every
base iff `d` lies in the record kernel. The 16 kernel elements are the complete list
of unrecorded bulk moves. -/
theorem invisible_iff_kernel :
    ∀ d : CellCfg,
      (∀ c : CellCfg, faceRecord (xorCfg c d) = faceRecord c) ↔ d ∈ recordKernel := by
  decide

/-- First-isomorphism check of the actual cell record map:
`|image| · |kernel| = |domain|` (`16 · 16 = 256`). -/
theorem record_image_times_kernel :
    (Finset.univ.image faceRecord).card * recordKernel.card = 256 := by decide

What this page does not claim

The theorem does not prove the 16 kernel moves are gauge; it only identifies them as the sole candidates for blindness. The result does not establish that every bulk distinction in a larger system has a boundary witness. The computation does not derive the three-dimensionality of space; it assumes the forced D=3 cell.

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: