Holography Cell Injection Record Blind Only Global

The global blindness theorem

The cube has eight corners, and the test puts one recognition bit on each corner, giving 256 possible configurations. The boundary record, a discrete list of six face parities, is what the ledger closure posts for the whole cell. The question is whether a change inside the cube always shows up on that record.

The answer is a sharp dichotomy. Flipping any single corner bit changes the record, and it changes exactly the three faces that meet at that corner. No local change is ever invisible. Yet the record is not a perfect picture of the inside: there are 16 distinct whole-cell moves that leave the record unchanged. These blind moves are exactly the flips of entire faces, including the flip of all eight bits at once.

The theorem record_blind_only_global states the key bound: any two configurations with the same boundary record differ on at least 4 of the 8 corners, meaning half the cell. This bound is tight, because flipping one whole face changes exactly 4 corners and is invisible from every starting configuration. So blindness is only global: it never hides a change to a single corner, only changes that sweep across half the cell at once.

In Recognition Science, this result sharpens the question of complementarity, the idea that no bulk distinction exists without a boundary-readable witness. The theorem does not prove that the 16 blind moves are gauge, or unphysical. It isolates them, computing and classifying the blind set rather than assuming it. The choice of whether those moves count as real distinctions remains open.

For the reader, the practical upshot is a precise accounting: the record posts 4 bits of information, the blind kernel holds 4 bits of freedom, and their product is the full 256 configurations. The cell's interior is not fully readable from its boundary, but every single-bit difference is. The blindness lives only at the scale of whole faces and the whole cell.

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

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

/-- 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 that the 16 blind moves are gauge or unphysical. The theorem does not apply to configurations with more than one cell or to glued surfaces. The theorem does not establish that every bulk distinction posts, only that every single-bit flip does.

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: