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.
The four-office governed vertical on the home page ran once, on 2026-07-26. Its identifiers, digests, and verdicts are held in a private campaign record and are not publicly inspectable. What is public is the declaration document, the prior three-office run written up in full, and each office's own statement of its jurisdiction and maturity. A reader can therefore check that the offices agree about their boundaries; a reader cannot independently verify the run. That is the exhibit's stated promotion condition, and until it is met the composition is a dated report, not a reproducible artifact.
Nor does it generalize. One composition being exercised is evidence about those four artifacts and that one effect class — the atomic Git target-ref transition. It is not evidence that any other pair of components here composes, and there is no universal pipeline behind it.
A receipt id is a hash over the canonical decision inputs, so the same inputs under the same schema always give the same id. That is a real property and it holds. It is also narrower than it sounds: this site pinned dda5a1e5… in prose for months, and when the receipt schema gained fields the id became 3f8b93c1… while the behaviour it attests did not change at all. Determinism was never violated; the claim was simply about a schema version and was written as though it were about the system. Ids belong in artifacts, not in sentences.
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.
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 attributable 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.
Approval is an explicit operator or gate decision over a specific proposal, at an authority-bearing surface, with scope, time, and evidence recorded. It is not the agent saying it was done. It is not a passing test run. It is not a completed rehearsal. It is not a chat message. It is not a proposal being generated, nor a demo succeeding. Approval is a bounded authority-bearing act — if nothing recorded a scoped operator or gate decision, nothing was approved.
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. Nothing here is deployed at scale, and this page will say so until that changes. Per-object claims, verification dates, and promotion conditions are in the status ledger; where this page and that ledger disagree, the ledger is newer.
Two claims sit at the top of the pile, and they are different kinds of claim. The runnable one: a refusal demo that reproduces in about five minutes and whose exit code fails loudly if it passes for the wrong reason — re-verified 2026-07-29 from an editable install, which is not the same as a cold clone. The reported one: four separately-owned offices carrying one bounded change end to end, dated 2026-07-26, whose receipts you cannot see. Neither is a deployment.
Naming is not stability. Several components describe themselves as an “office” of a constellation. That word states jurisdiction — what a component may and may not decide — and says nothing about API stability, packaging, or production-readiness. Two of the four offices state in their own repositories that they are not production deployable or not operator-ready.
Live cage execution is unarmed by construction — the synthetic substrate (ORIGIN_SYNTHETIC) cannot confer operational effect; that refusal is structural, not a configuration flag. Specimens run against lab substrate; they are compatibility evidence, not live testimony about a deployed estate.