Holography Cell Injection Single Flip Posts Three

The cell injection test

A cube has eight corners. Put a single binary switch, a bit, on each corner, and record on each of the six faces whether the four corner bits on that face satisfy a parity condition. This is the setup of the cell injection test, a formal experiment inside the Recognition Science framework. The framework models physical structure as a discrete record of events, a ledger, and asks what such a ledger can and cannot hide.

The declaration single_flip_posts_three states a sharp result: flip any one of the eight corner bits, starting from any of the 256 possible configurations, and the six-face record always changes, and it changes on exactly three faces, the three faces that meet at the flipped corner. This is a proved theorem, checked by exhaustive computation over all cases, not a conjecture or a statistical observation. It establishes that no single local change to the interior of the cell goes unrecorded on its boundary.

The result is deliberately paired with a companion fact that prevents overreading. The map from the 256 configurations to the 16 possible boundary records is not one-to-one. There are 16 distinct configurations that share the same boundary record as the all-zero configuration, including the configuration with every bit flipped and the two inscribed tetrahedra. These blind spots are global, not local: any two configurations with the same boundary record differ on at least four of the eight vertices, half the cell. A whole-face flip, changing four bits at once, is invisible from every starting configuration.

In Recognition Science, this dichotomy is the content of the cell injection test. It was designed to separate two futures for the framework's complementarity premise, the idea that no bulk distinction exists without a boundary-readable witness. The theorem shows that on the forced three-dimensional cell, the premise reduces from a statement about all 256 states to a statement about 16 explicit global parity moves. The module does not prove that those 16 moves are gauge, that is, that they are not performed distinctions; it isolates them for a later decision.

What the declaration does not claim is as important as what it proves. It does not claim that the 16 invisible moves are physically unrealizable or that the framework has settled the status of complementarity. It does not claim that the boundary record captures all information about the cell, since the non-injectivity result shows it does not. It establishes a precise, machine-checked fact about a discrete model, and leaves the interpretive step to a separate axiom choice.

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

What this page does not claim

The declaration does not claim that the 16 invisible moves are gauge or physically unrealizable. It does not claim that the boundary record captures all information about the cell. It does not claim that the framework's complementarity premise is proved.

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: