What Must Agent Memory Preserve? Representation Contracts for Exact Invalidation
Abstract
In an AgenticOS, persistent memory forms a systems abstraction boundary: implementations can compact evolving logical state and still promise current invalidated-set snapshots, future invalidation updates, and auditable explanations. We study the information retained service state must preserve to keep those operations exact. Under a finite monotone invalidation semantics, current invalidity is the dependency closure of targets named by accepted direct-invalidation certificates. For a fixed record universe, the future-invalidation contract admits a complete invariant: the current invalidated set together with reachability whose targets remain currently valid. With dependency topology fixed across updates, this contract quotient is update-closed: accepting any seed set advances the quotient from its current value and the input alone, even when reachability into already-invalid targets has been discarded. Monotone invalidation therefore shrinks update-relevant reachability, whereas cause-labelled audit can require finer cause-relevant state. Six explicit collision witnesses expose representation failures, and executable theorem controls exhaustively verify the update characterization and quotient transition over the complete three-record invalidation/dependency control family. The resulting design principle is contract-relative: probabilistic models can propose candidate state changes under uncertainty; acceptance into the memory state commits an AgenticOS memory layer to preserving the distinctions required by its exact maintenance and audit operations.