silent_iff_kernel
plain-language theorem explainer
A bulk move on the forced D=3 cell leaves every boundary face-record unchanged if and only if it lies in the 16-element record kernel. Anyone citing the injection-test classification of unrecorded moves, or the gauge-coset structure in the entropy-fork chain, uses this name. The proof is a one-line re-export of the decidable classification already proved in CellInjection.
Claim. For every full-cell configuration $d$ on the forced $D=3$ cell (eight vertex bits), the following are equivalent: (i) for every base configuration $c$, the six face-closure parities of $c \oplus d$ equal those of $c$; (ii) $d$ belongs to the record kernel (the finite set of configurations whose boundary record matches the empty cell).
background
The module RecordMonotonicity is step 3 of the entropy-fork development: it derives weak complementarity (injection of bulk states into boundary letter space) on the forced $D=3$ cell from record accounting, rather than assuming monolithic complementarity. Configurations are CellCfg $= \mathrm{Fin},256$, packing one recognition bit on each of the $8=2^3$ vertices. The boundary record is the list of six face-closure parities (one per cube face). Moves act by bitwise XOR.
The record kernel is the finite filter of configurations whose face-record equals that of the empty cell; these are exactly the record-invisible bulk states. Upstream, CellInjection already classifies shift-invariance: a move is invisible from every base if and only if it lies in that kernel (proved by decide over the finite space). The present declaration simply renames that classification as "silent moves" for the monotonicity and gauge-coset arguments that follow in this module.
proof idea
One-line wrapper: apply invisible_iff_kernel at the given configuration $d$. No new reasoning; the biconditional and the finite decision procedure are inherited verbatim from CellInjection.
why it matters
Silent moves are the only candidate violations of complementarity on the forced cell. Naming them as the record kernel lets the module identify gauge classes with kernel cosets (gauge_iff_kernel in the module narrative) and then prove that no record-compatible protocol separates a gauge pair. That chain replaces the holography manuscript's strongest premise (recognition complementarity) by two weaker, falsifiable inputs: ledger book-balance (no free erasure of posted record) and the finite kernel classification from the injection test.
Framework landmarks: the cell is the forced $D=3$ eight-vertex cube from the T7/T8 forcing chain (eight-tick octave, three spatial dimensions). Downstream used_by is currently empty for this alias, but sibling results (books_balance, no_free_erasure, erasure_exports_debit, and the gauge/protocol theorems sketched in the module doc) consume the same kernel language. The declaration is a proved re-export, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.