Holography Cell Injection Record Image Times Kernel

The cell's bookkeeping balance

In the Recognition Science framework, the fundamental object is a ledger, a discrete record of events. The framework models a three-dimensional cell as a cube with one recognition bit on each of its eight vertices, giving 256 possible configurations. The boundary record of the cell is what the ledger posts: six parities, one per face, each recording whether the four vertices on that face have an even number of 1-bits. The declaration record_image_times_kernel is a machine-checked theorem, proved by exhaustive computation, stating a precise balance: the number of distinct boundary records (16) multiplied by the number of configurations that leave the record unchanged (16) equals the total number of configurations (256).

This balance is not a trivial counting identity. It sits inside a sharp dichotomy that the framework's library proves about the cell. First, flipping any single vertex bit always changes the boundary record, and it changes exactly three of the six face records. No single-bit distinction is unrecorded. Second, the record map is nonetheless not one-to-one: there are 16 distinct moves that leave the record untouched. These 16 moves form a group generated by flipping all four vertices of a whole face, and they include the global complement (flipping all eight bits) and two inscribed tetrahedra. Third, blindness is only global: any two configurations with the same boundary record differ on at least four of the eight vertices, half the cell. The bound is tight, since one whole-face flip of weight four is invisible from every base configuration.

In Recognition Science, this theorem matters because it refines a central premise of the framework's holography program: that no bulk distinction exists without a boundary-readable witness. On the forced cell, that premise reduces from a statement about all 256 bulk states to a statement about 16 explicit global parity moves. The theorem does not prove those 16 moves are gauge, or physically irrelevant; it isolates them and computes their structure. The balance expressed by record_image_times_kernel is the exact statement that the posted record (4 bits of information) and the invisible degeneracy (4 bits of freedom) coincide at the whole-cell level. This coincidence is a per-cell phenomenon, invisible when one looks at individual faces or glued surfaces, where the rank and nullity split differently.

What the theorem does not claim is equally important. It does not prove that the 16 invisible moves are physically meaningless or that they should be quotiented out. That identification, that an unposted move is not a performed distinction, is a separate interpretive choice within the framework. The theorem also does not establish anything about the physical bridge from recognition to linking in three-dimensional space; that bridge remains an open target. What the theorem does give is a precise, machine-checked accounting of what a single cell's boundary can and cannot see, turning a philosophical question about complementarity into a concrete, computable classification of 16 explicit moves.

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

/-- **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 boundary record map is NOT injective on raw bulk states.** The countermodel
of the holography paper survives at cell level unless record-equal states are
physically identified. -/
theorem record_not_injective : ¬ Function.Injective faceRecord := fun h =>
  absurd (h complement_invisible) (by decide)

theorem recordKernel_card : recordKernel.card = 16 := 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 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 prove that the 16 invisible moves are physically meaningless or should be quotiented out. The theorem does not establish anything about the physical bridge from recognition to linking in three-dimensional space. The theorem does not prove that every bulk distinction has a boundary witness; it only shows that single-bit flips do.

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: