Holography Cell Injection Record Nullity Eq Four

The cell record theorem

In Recognition Science, a ledger (a discrete record of events) assigns to each configuration of a cell a boundary record, the list of parities on its six faces. The declaration record_nullity_eq_four is a machine-checked theorem about the simplest nontrivial cell, the cube with one recognition bit on each of its eight vertices. It states that the map from the 256 possible interior configurations to the boundary record has a kernel of size 16, and since 16 is 2 to the fourth power, the nullity is 4. In plain language: exactly 16 distinct interior states produce the same boundary record as the all-zero state.

The theorem does not merely count the blind states; it identifies them. The 16 configurations are exactly the whole-face flips: flipping all four vertices of any one face, or combinations of such flips, including the global complement (all eight bits flipped) and two inscribed tetrahedra. The proof is by exhaustive computation over all 256 cases, and the result is sharp. Any two configurations with the same boundary record differ on at least 4 of the 8 vertices, so blindness is never local: a single vertex flip always changes the record, and it changes exactly the three face records incident to that vertex.

This dichotomy is the theorem's substance. Every local bulk distinction posts to the boundary, yet the record map is not injective. The blind set is a rank-4 subgroup of 16 moves, and the image also has size 16, so the image times the kernel equals 256, the full configuration space. At the scale of one whole cell, the posted information (4 bits) and the hidden freedom (4 bits) are exactly balanced.

In the framework's account, this result sharpens the complementarity premise of holography. The claim that no bulk distinction exists without a boundary witness reduces, on the forced cell, from a statement about all 256 states to a statement about 16 explicit global parity moves. The theorem does not prove those 16 moves are gauge; it isolates them as the complete set of blind moves, leaving the physical interpretation of that blindness as a separate question.

/-- Record nullity of the whole cell: 4 free bits (`log₂ 16`). At whole-cell
granularity rank = nullity; the entropy fork splits only per face and under gluing. -/
theorem record_nullity_eq_four : Nat.log2 recordKernel.card = 4 := 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

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

/-- 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, only that they are the complete set of blind moves. The theorem does not establish any claim about cells of dimension other than 3 or with a different number of vertices. The theorem does not derive the complementarity axiom of holography; it reduces it to a statement about 16 explicit moves.

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: