KernelIsGauge
plain-language theorem explainer
Names the operational premise that physical distinguishability respects the ledger: any pair of bulk cell states that physics can tell apart must already be separable by a posting-compatible protocol. Holography and entropy-fork arguments cite it as the sole remaining hypothesis between the proved GSL bookkeeping and weak complementarity. It is a one-line Prop abbreviation, not a proved theorem.
Claim. A binary relation $\mathrm{dist}$ on full-cell configurations (8-vertex $D=3$ cells, packed as elements of $\mathrm{Fin}\,256$) is a gauge-respecting distinguishability when, whenever $\mathrm{dist}(c,c')$ holds, $c$ and $c'$ are separable by some finite protocol built from record-compatible dynamics.
background
Module RecordMonotonicity is step 3 of the entropy-fork chain on the forced $D=3$ cell. Step 1 injects bulk configurations into boundary letter space; step 2 supplies the Clausius selector. The holography manuscript's strongest premise is recognition complementarity; this module replaces it by weaker, falsifiable inputs centered on record accounting.
A full-cell configuration assigns one recognition bit to each of the $8=2^3$ vertices. Boundary heat equals posted record flux channel by channel, and is exact against a record-weight potential: along any bulk trajectory, path heat equals $\Phi(\mathrm{end})-\Phi(\mathrm{start})$. Consequently there is no free erasure of the posted record, and zero-heat steps preserve weight exactly.
Two configurations are gauge-related when they carry the same boundary record; that relation is exactly membership of their XOR difference in the 16-element record kernel. Separated means some finite protocol of record-compatible maps distinguishes the pair. The present definition packages the claim that every physically meaningful distinction is already of that posting-witnessed kind.
proof idea
Definitional, not a proof. The body is the universal implication: for all cell configurations $c,c'$, if $\mathrm{dist},c,c'$ then $\mathrm{Separated},c,c'$. No tactics, no lemmas applied; it is a named Prop standing for the operational reading of "the record kernel is gauge."
why it matters
This is the named hypothesis of step 3. The headline theorem weak_complementarity_of_gsl assumes it and concludes that record-equal (gauge-related) bulk states cannot be physically distinguished: the manuscript's complementarity injection then holds with the monolithic premise replaced by the no-free-record discipline proved from GSL bookkeeping.
Downstream, kernelIsGauge_falsifier states the honest fork: if any process distinguishes a gauge pair, the premise fails and weak complementarity breaks. The bundled target target_record_monotonicity lists it among the six clauses of the record-monotonicity certificate, and holographic_bound_of_weak_comp uses the resulting injection to place 16 physical states (4 posted bits) inside the 6-bit boundary capacity, the cell-scale holographic access bound.
Framework role: on the forced eight-tick cell ($T7$, $D=3$ from $T8$), it converts ledger exactness into operational indistinguishability of kernel cosets, without assuming full complementarity up front.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.