A Conservation Law for Accountable Systems: Integrity and Non-Establishment as Antagonistic Resources, with Machine-Checked Instances in Deniability, Anonymity, and Erasure

Accountable systems seal every persisted effect into a tamper-evident integrity structure. We show, and machine-prove, that this commitment is in quantifiable tension with non-establishment — the capacity to let an effect occur without it being constituted as an attributable record of the system. We make the tension a combinatorial conservation law over an abstract class of label-independent notarization structures: an effect's integrity strength (the redundancy of label-independent links pinning it to the established frontier) and its non-establishment capacity (its non-retroactive separability from that frontier) are antagonistic — no effect is both robustly sealed and separable (Theorem 1), and the seal carried by label-independent structure is invariant under arbitrary relabelling, including key deletion (Lemma 1, Corollary 2); any capacity forces an unsealed effect (Corollary 1); the familiar binary impossibility "total accountability excludes non-establishment" is recovered as the law's degenerate corner (Theorem 2); and redundancy is resilience (Theorem 4). The law is moreover an analysis, threaded by one structural fact: the label-independence that seals an effect (Theorem 1) is also what prices its separation (Theorems 5–7), and what governs the tractability of synthesising one — polynomial when label-independence is the only non-trivial surface mode, NP-complete in general. The least exit set is unique, definable, and computable; its cost is bounded by integrity strength, and for a fresh effect equals it (Corollary 3). All are proved unbounded in TLA⁺/TLAPS (679 obligations, 0 omitted/admitted), with non-vacuity and the load-bearing role of label-independence checked by TLC. Our central claim is unificational: three trade-offs developed by separate communities — non-repudiation vs. deniability (secure messaging), anonymity vs. accountability (ledgers), and immutability vs. right-to-be-forgotten (data protection) — are machine-checked instances of this one law, alongside the action-constitution setting that motivated it. We are explicit that the instances are isomorphic: that is precisely the content of a unification, not a defect, and we claim a clean unification of independently-recognised patterns under one predicate, not depth in any single instance. The decade of redactable-chain cryptography appears as the law's constructive dual: every known mechanism that buys separability on a sealed effect degrades the kind of integrity it offers.