The strongest case against this work, stated plainly. A system built around refusing overclaims should refuse its own.
The Lean theorems prove class boundaries of refusals — that a given refusal kind is required by the custody discipline's own definitions. They do not prove that any deployed system is safe, that the Python implementation is bug-free, or that a particular production incident was machine-checked. Receipts prove instance facts: what was observed, what was decided, under which policy hash. They do not prove intentions, and they cannot make a wrong observation right — only attributable.
Custody moves cost from postmortem reconstruction into runtime. Every gate is latency on the action path. Every receipt is storage. Every typed claim is friction at write time — an agent that used to just do the thing now has to propose it, and something has to verify it. The bet is the same one behind TLS and structured logging: pay steadily at runtime instead of catastrophically at incident time. If your incidents are cheap, this trade is bad for you.
This architecture relocates trust; it does not eliminate it. The trusted computing base is the receipt store, the sealing path, and the clock witness source — small, boring, and enumerable, but real. Trust with a bill of materials. Trustless is not on offer here, and anyone offering it elsewhere is selling something.
A witness can be wrong. The system's answer is not prevention — it is attribution: which witness, attesting what, when, with what coverage. False testimony becomes quarantinable evidence with a return address instead of an anonymous rumor in a log file. That is a real improvement and a real limit: garbage observed is still garbage; it is merely garbage you can recall by origin.
Authorization checks, RBAC, OPA over inputs you already trust, audit logs for low-stakes flows, rate limits, CI gates. If your inputs are attested by construction or your blast radius is small, the conventional stack is cheaper and you should use it.
If you only need an authorization check, use an authorization check.
Alpha. Solo development. A research lab with working instruments and proof artifacts, not a product seeking deployments — lab notebook, not an oracle. The demo reproduces from a cold clone in about five minutes; that is the strongest operational claim this site makes. Nothing here is deployed at scale, and this page will say so until that changes.