module module moderate

`IndisputableMonolith.Holography.CellInjection`

Module defining the forced D=3 recognition cell: eight vertices, one bit each, packed as Fin 256 configurations. It supplies face records, flips, XOR, weights, zero/complement cells, and single-flip posting lemmas. Holography authors cite it as the cell-injection test (entropy-fork step 1). Structure is definitional plus elementary flip lemmas, not a deep existence proof.

claimOn the forced $D=3$ cell with $8=2^3$ vertices, a full-cell configuration assigns one recognition bit to each vertex and is identified with an element of $\mathrm{Fin}\,256$. Vertex $v\in\mathrm{Fin}\,8$ has coordinate bits $(v\&1,\,v\&2,\,v\&4)$. The module defines face records of such configurations, single-vertex and face flips, XOR of configurations, Hamming weight, the zero cell and its complement, and lemmas controlling how a single flip posts to face records.

background

Recognition Science forces $D=3$ spatial dimensions (T8) and an eight-tick octave of period $2^3$ (T7). The elementary holographic cell is therefore the 3-cube: eight vertices, each carrying one recognition bit.

A full-cell configuration packs those eight bits into $\mathrm{Fin},256$. Coordinate bits of vertex $v$ are read by the masks $v&1$, $v&2$, $v&4$. Face records project a bulk configuration onto a chosen face; flips and XOR act pointwise on bits; weight is the number of set bits. The zero cell is the all-off assignment and the complement inverts every bit.

This module is step 1 of the entropy-fork chain (panel holo_unconditional_20260701): the cell-injection test that later supports weak complementarity.

proof idea

Definition module with supporting lemmas, not a single theorem proof. It introduces the configuration type and the operations vbit, closedOn, faceRecord, flipv, xorCfg, weight, cell0, cellComplement, and faceFlip. The nontrivial content is the single-flip posting lemmas (including the three-face variant): they track how flipping one bulk vertex changes the recorded face data. Those identities are pure finite bit arithmetic on Fin 8 / Fin 256 and are discharged by direct case or card reasoning.

why it matters in Recognition Science

Imported by RecordMonotonicity, step 3 of the entropy-fork development ("no free erasure $\Rightarrow$ weak complementarity on the forced cell"). Downstream documentation states explicitly that step 1 was the cell-injection test in this module and step 2 the Clausius selector. The holography manuscript treats recognition complementarity as its strongest premise and isolates the minimal form: weak complementarity, an injection from physical bulk states into boundary records. By fixing the T7/T8 eight-vertex cell and the face-record map, the module supplies the discrete geometry on which that injection is later proved.

scope and limits

Does not prove weak complementarity or bulk-to-boundary injection; that is RecordMonotonicity.
Does not derive D=3 or the eight-tick period; it assumes the forced cell from T7/T8.
Does not treat multi-cell lattices, gluing, or continuum bulk fields.
Does not encode dynamics or time evolution of configurations.
Does not address strong complementarity or full holographic entropy equalities.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Holography.RecordMonotonicity module_import

declarations in this module (28)

abbrev CellCfg L77
def vbit L80
def closedOn L84
def faceRecord L90
def flipv L99
def xorCfg L103
def weight L107
def cell0 L110
def cellComplement L113
def faceFlip L116
theorem single_flip_posts L123
theorem single_flip_posts_three L128
theorem complement_invisible L137
theorem record_not_injective L142
def recordKernel L147
theorem recordKernel_card L150
theorem recordKernel_eq L155
theorem record_image_card L162
theorem record_rank_eq_four L165
theorem record_nullity_eq_four L170
theorem record_image_times_kernel L174
theorem record_blind_only_global L183
theorem face_flip_invisible_everywhere L189
theorem faceFlip_weight L192
theorem invisible_iff_kernel L197
def target_cell_injection L207
theorem target_cell_injection_holds L218
theorem cellInjectionCert L223