RecordMonotone
plain-language theorem explainer
Record monotonicity is the generalized-second-law predicate on bulk trajectories: the posted record potential is nondecreasing at every consecutive step. Anyone working the entropy-fork or weak-complementarity argument cites it as the target property of closed (zero-export) paths. It is a one-line definition: chainwise inequality of cell potentials along a configuration list.
Claim. A trajectory $p$ (a list of cell configurations) is record-monotone when the record potential $\Phi$ is nondecreasing along consecutive steps: for every adjacent pair $(c,c')$ in $p$, $\Phi(c)\le\Phi(c')$.
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced $D=3$ cell. The manuscript isolates weak complementarity (injection of bulk states into boundary letter space) as the strongest holography premise and replaces it by record accounting plus two weaker inputs.
The ledger books balance: boundary heat equals posted record flux channel by channel, and path heat is exact against the record-weight potential, $\mathrm{pathHeat}=\Phi(\mathrm{end})-\Phi(\mathrm{start})$. Consequently an erasure (weight drop) always exports as negative boundary heat, and a zero-heat step preserves weight exactly. The cell potential $\Phi$ is that record-weight potential on configurations; record monotonicity is the chainwise nondecrease of $\Phi$ along a trajectory.
The surrounding development already has the Clausius selector and cell-injection test; this predicate is the GSL shape those balance identities feed.
proof idea
Pure definition: RecordMonotone p is List.IsChain of the relation $\Phi(c)\le\Phi(c')$ on consecutive configurations. No proof obligations. Downstream, recordMonotone_of_no_export turns a zero-export chain ($0\le\mathrm{stepHeat}$) into this predicate by rewriting each step via stepHeatCell_eq_potential and a linear-arithmetic close.
why it matters
In the Recognition holography program this is the GSL predicate on the posted record: not an extra thermodynamic law, but the shape of the bookkeeping identity once heat is identified with record flux. The parent theorem recordMonotone_of_no_export states that any closed-system trajectory (no heat export at any step) is record-monotone; with the balance theorem, that is pure accounting.
It sits inside the entropy-fork path that derives weak complementarity on the forced cell (T8 forces $D=3$, eight-tick octave) from no-free-erasure rather than from a monolithic complementarity axiom. Gauge classes, record-compatible dynamics, and the eventual injection into boundary letter space all treat nondecrease of the posted record as the discipline that forbids free erasure and free record manufacture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.