Holography Cell Injection Complement Invisible

The invisible complement

The declaration complement_invisible states that two opposite configurations of a cube's corner bits produce the same boundary record. The cube here is the forced D=3 cell: eight corners, each holding one recognition bit, which is a discrete on-or-off mark. The boundary record is the list of six face-closure parities, one parity per face, where a face is closed if its four corner bits have even parity. The theorem proves, by direct computation over all 256 configurations, that the all-zeros configuration and the all-ones configuration (the global complement, flipping every bit) yield identical boundary records.

This single fact is the seed of a larger, machine-checked result about the cell's record map. Flipping any one corner bit always changes the boundary record, and it changes exactly the three faces incident to that corner. Yet the map from the 256 configurations to the 16 possible boundary records is not one-to-one: its blind set is a group of 16 moves, generated by whole-face flips and including the global complement and two inscribed tetrahedra. The blindness is only global: any two configurations with the same boundary record differ on at least four of the eight corners, half the cell. A whole-face flip, which changes four bits, is invisible from every base configuration.

In Recognition Science, this sharpens the complementarity premise of the holography program. The premise that no bulk distinction exists without a boundary-readable witness reduces, on the forced cell, from a statement about all 256 bulk states to a statement about 16 explicit global parity moves. Weak complementarity through the posted record holds if and only if those whole-face parity flips are recognition gauge, meaning they are not performed distinctions. The declaration does not prove those 16 moves are gauge; it isolates them as the complete blind set, computed and classified rather than postulated.

The practical upshot is a precise accounting of what a boundary record can and cannot see. A single corner flip is always witnessed, but a coordinated flip of an entire face is never witnessed. The record cost at whole-cell granularity, four posted bits, coincides with the fiber degeneracy, four free bits, since 16 times 16 equals 256. This coincidence is a per-cell phenomenon; the entropy fork seen in glued surfaces, where rank and nullity differ per face, is invisible at the single whole cell.

/-- 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 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 declaration does not prove that the 16 blind moves are recognition gauge. The declaration does not claim that every bulk distinction is recorded; it proves the opposite for whole-face flips. The declaration does not apply to glued surfaces, where the entropy fork is a per-face phenomenon.

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: