Revision log, kept in the open so the record shows what changed.
First draft, 2026-09-11, commit ea08510.
Second draft, revised 2026-09-11, commit 39e1018. The diff between the two is the honest account of what changed. The change in register is deliberate: we decided that the argument for the result's utility is load-bearing, so where the first draft was conservative about the science, this one is predictive along its consequences, each consequence stated with its bound and what would falsify it.
Third draft, revised 2026-09-11: the rhetorical arguments distilled to their essence and the opener reordered, because a claim nobody understands is a claim nobody can falsify. The claims themselves are unchanged across all three.
Fourth draft, revised 2026-09-16: one prediction below has since been tested and held, and the post says so at the grade it has today. The AI paragraph is sharpened into a conjecture, dated, and the reason is the news: in the last few days the heads of the largest AI labs have jointly called for coordinated limits on the pace of frontier work, with evaluators embedded in the labs and governments asked to back it, in the name of safety. We think that gets the problem backwards. Nobody has yet stated the alignment problem in a form a record could answer, and slowing a field is not a substitute for understanding it, so this draft makes the strongest conjecture it honestly can and asks to be argued with. The account of how the finding was reached is told in specifics and in the order it happened. And because the paper and its development keep moving, where a claim's backing has grown or its wording has been refined since the last draft, the post now says it the way the development does.
Fifth draft, revised 2026-09-19: a note to the reader now comes first. The post states the political position its result entails, and why it is published ahead of review. We did not choose that position. The model forces it. The technical content is unchanged.
Sixth draft, revised 2026-09-19: a technical refinement. The class of claims with bounded proofs is wider than earlier drafts said. It was stated as the list homomorphisms. The development now characterizes it as the local positional homomorphisms, of which the list homomorphisms are the position-free case. It also proves the boundary from the other side: any query answered over arbitrary windows by a sound, complete, non-over-revealing scheme that recombines opened ranges is a finalized positional fold. With both directions proved, this is where the class ends for schemes of that kind, and it cannot be widened again without leaving them. The section "What You Can Check Without Reading Everything" is updated to match, and the text was edited throughout for consistency between drafts.
Before You Read¶
This post is unusual, and you should know how before you start. It is an exhaustive account of a claim, written to be complete rather than approachable. It is long, it is formal wherever a claim is being made, and it ends in a political position that follows directly from the result. More approachable writing is planned, and readers who want the conclusions without the full argument will be better served by that when it comes. This post is a formal statement of what we found, what we take it to mean, and what we intend to do about it.
The first drafts presented a mathematical result and its engineering uses and stopped there. The result does not stop there. It says what any record can and cannot bear, and the institutions we live under, science, law, money, are records that ask to be believed. A finding about the first is a finding about the second. So what follows is a demonstration and then a demand. The demonstration is the theorem. The demand is what the theorem asks of anyone who keeps a record and wants to be trusted: give the account wherever an account can be given, and name who is being relied on wherever it cannot. That standard applies to us first.
Here is what the claim stands on. The proof is finished and machine-checked. What remains before the paper is submitted, within the month, is its exposition at the register its venue requires, which is the foundations of computer science and nothing else. None of the political argument belongs in that paper, which is why it is here. The paper also applies its method to itself: every claim in it is graded by what backs it, as a demonstration that the method is general. Beyond the proof there are the retrodictions. Several fields of computer science reached findings separately that they could not explain, and the theorem explains them with one reason. The same reason accounts for a practice far older than any of those fields, going back to the people who first asked the question and tried to answer it by intuition; that comes near the end. And there is a prediction. The theorem named a class of proofs no field had named and said what they would cost, and when we built an engine and ran it at scale, that is what they cost.
None of it is a claim to know everything. This is epistemology, a formal method for the practice of knowing, and it leaves open every hard question of ontology in every domain: what a domain's entries mean, and what exists in its world. What it gives is one structure for epistemic integrity, the same in every domain, derived rather than intuited. To our knowledge that did not exist before.
If you only want the engineering, the sections from "Everything Is a Trust Decision" through "Three Instances" stand on their own. I am asking you to check the argument. Agreement is beside the point.
Far More General Than Packaging¶
Last time I argued that Nix is right about everything except the store, and near the end I said in passing that the line between what a system can verify and what it can only vouch for should be a field in the metadata, not a feeling.
I undersold it. The line is a theorem, and it is not about packaging. It applies to anything that keeps a record that only grows and wants an answer from it to stay true: package managers, transparency logs, signed commits, reproducible science, the key you rotate the day your laptop is stolen. You already make trust decisions all day. The result says to make them on purpose, and write them down.
The largest such record is the scientific one. Last week a lab announced a solution to a Millennium Prize problem, and two researchers who had posted first asked in public how their work had been used. I do not know who is right. Nobody can know from the record, because the record science keeps cannot answer the question. Who posted what, when, and what was built on it are questions about a sequence of findings that only ever grows, and science settles every one of them by reading, argument, or reputation.
A dispute over credit is not a small thing. Science is meant to correct itself, and its correcting rule is short: check the result, then rerun it. Applied to science's own record, the rule fails. "Who found this first" and "what does this rest on" cannot be checked or rerun by anyone, because the record was built to hold findings, not the answers to those questions. When credit goes wrong, a field takes its lead from whoever took the work instead of whoever did it, and everything built on that lead is built on the wrong foundation. There is no court to send it to. A truth is nobody's property, and that is as it should be, but it means no law can put credit back where it belongs. Only conduct ever did, and a record cannot store conduct.
Under the credit problem sits a deeper one. A citation tells the reader that the evidence is elsewhere and who holds it. Almost nobody follows it. So a citation is taken on faith, and a result is not checked by being cited, however many times. If you hold the evidence yourself and can rerun it, the result is checked, whether or not a journal ever said so. The citation stands in for a check the reader cannot run. Our institutions have the order backwards. What gets believed is what the pipeline has approved, and the approval says nothing about the contents: a true result without it is waved away because there is nothing to cite, and a false result with it travels for years looking like knowledge. The pipeline decides who is believed, and everyone who wants to be believed has to queue for it. A record in which every claim carries its grade, checked by machine, cited at source, taken on a named person's word, or argued from other claims, would let anyone look instead of asking whom to trust. That is a problem of how the record is built, and a problem of that kind can have an engineered solution.
Certificate Transparency shows what one looks like. It is the public log of every TLS certificate issued, and the most widely deployed append-only record in the world. It can prove exactly two things. That an entry is in the log. And that a newer version of the log is the old one with more entries on the end, nothing erased or rewritten. Both proofs are small. The log is a Merkle tree, a tree of hashes, which I will also call fingerprints, and a proof is one path down it, logarithmic in the size of the log. Ask it anything about what the entries say, how many certificates it holds for your domain, whether one was issued by an authority you never authorized, and it has no proof to give you; someone reads the entries. That is no gap in its engineering. Its two proofs read the shape of the tree and never its contents, and nobody had a theory of which claims about contents could have a proof like that.
Some claims about a record have a special shape: what they say about the whole is assembled from what they say about the pieces, as a total is assembled from its parts. The paper calls a claim of that shape a fold. Whenever a claim over a record is a fold, a checker can settle it at every size the record ever reaches with a number of openings that grows only with the logarithm of the record, from the shape of the claim alone, assuming nothing but that fingerprints cannot be forged. Every other claim that keeps its proof small pays for it with a cryptographic hardness assumption. The paper's word for a record held that way is eusynoptic, Aristotle's word for a city small enough to survey at a glance, and the glance stays the same size no matter how large the record grows. Certificate Transparency's two proofs, "this is in the log" and "this log extends that one," are both of this shape, and both read the structure of the log and never its entries. "This finding was in the record before that one" is another, and it reads the entries. So is "everything this paper cites was in the record before it," and so is "no package beneath this program has been pulled as of entry n." "This result reproduces" is fixed by the record only when the record carries everything a stranger needs to run it, and where it does not, the theorem names what you are trusting instead: the authors' word, or a named replicator's.
Nobody has felt this yet, because nobody has built a record whose claims come with proofs with as few pieces as a Merkle path: priority as a receipt instead of a dispute, a citation as a pointer you can check instead of one you take on faith, a result graded by what a stranger can rerun. Those follow from the result, and each can be tested. If one fails, the result is wrong.
Since the first draft, we tested one of them: that the small proof is not a property of Merkle trees but of any claim with the fold shape, over any domain, and that it holds at scale. We built an engine on the paper's two calculi and ran it against randomly generated domains and randomly generated claims of that shape, each resting on many entries, over records of up to a million entries, under three seeds. The work to check a claim stayed logarithmic in the record's size, in counted operations and in wall-clock time, and the part of the engine that opens a proof against the record's fingerprint is proved sound in Lean, assuming an injective hash and stated at the simplest measure. The run itself uses a test hash that is not injective, so the run is evidence about the structure rather than about collision resistance, and the logarithmic bound on the number of openings is proved in the paper's development and tested, not proved, in the engine. The engine is not public yet. Until it is, this is my report of what it did; when it is, you can run it. We are building two records on it, one for packages and one for identity, and both appear near the end, along with the rougher one that built this paper. The one science needs, nobody has built, and the finding says what it would have to be. You may want to see us succeed or you may want to see us fall. Either way, the argument is the thing to contend with.
I did not set out to find any of this. I spent a decade inside Nix, and this summer, after years of building the atom, I saw that it could replace Nix outright; that was the last post. What replaced it was a record of atomic actions, small self-contained entries, canonicalized and signed, the same shape Zach had already built for identity in Cyphr, where he knows far more than I do. Two systems in two fields with the same record under them made a question hard to avoid, one I had not thought to ask in ten years: does this problem have a formal upper bound? It did. So we tried to put Nix and a software bill of materials into the same model, to see how they compared, and could not: only the atom was generative over signatures, the only one where you keep deriving what to trust instead of being handed a list. The bound then kept showing results about how long a claim stays true that looked, vaguely, like the old tradeoffs of distributed systems; they became two smaller results we thought were the whole story, until the question of whether there were exactly three ways to fail came up in the middle of them and was too interesting to leave. It had an answer. Months of using that answer showed it was one piece of a calculus, which is my name from here on for the result in the paper, and the calculus has since become an engine. Most of the years before this are experiments and false starts I never wrote down, and I was wrong for most of them. A finding about what any record can and cannot answer does not fit in the vocabulary of package managers or key rotation; it has to be said at the level it lives at, which is the level of anyone who keeps a record and asks it whom to believe. That is why this post exists, and why an engineer who was fixing two things is now writing to everyone.
A few facts the argument depends on. This is my first scientific contribution. My co-author Zach Collier and I asked one question in two forms. Trust has boundaries; everyone knows that, and Thompson drew one forty years ago. What nobody had was a proof that the boundaries are exhaustive: that past a certain line there is nothing left to verify, and every kind of trust that remains has been named. So: is there a provable upper bound on how much you can verify, and is what lies past it completely accounted for? The answers are in the paper, which stays private with the Lean 4 development behind it until it has been reviewed. Lean 4 is a proof assistant, a program that confirms every step of a proof and accepts nothing it cannot confirm; the development is the proof as written in it, which I will also call the mechanization. The mechanization is mostly mine, with AI assistance, done under a discipline I describe at the end. Until the development is public, "the machine checks it" means I ran the check and am telling you the result. Once it is public, you can run it yourself.
This post is out of order, and deliberately. It is a critique of the process by which science, and open source with it, decides which claims to admit and whom to believe, and it is published before that process has reviewed it. None of that is contempt for the process. Peer review, standard formulations, citation at source, proof a stranger can rerun: that discipline is the only reason a result like this could exist, and the paper will go through it. But a process that cannot check its own record cannot correct itself from inside in time, and the result makes a demand that binds the people who found it before anyone else. A check you could have finished and did not finish is not trust; the name for it is sloth. The mathematics can be presented now, at the register it needs, where it can be challenged, and declining to present it would be the failure the result names. So the paper goes to review and this account goes out today. If the two ever disagree, the review wins and this post will be corrected. The dilemma was not chosen. The result forces it, given the state of things.
The timing matters as well. The institutions that keep society's records are being asked, right now, to absorb machines that produce claims faster than anyone can check them, and a year is a long time to hold back a result about what checking can and cannot do. A large firm can publish a result within days of finding it; an independent researcher waits a year for review, and many of the bottlenecks in that wait are what a graded, verifiable record could automate away. The dispute above is also the plain argument for posting dated: a public statement of what you found and how strongly you hold it is the cheapest insurance there is.
The Question Thompson Opened¶
The question is old. Socrates was called the wisest man in Athens, and his own account of why was that he alone knew there was an end to what he knew. He could not say where it was, only show that everyone he examined was standing past it without noticing. Twenty-four centuries later, Ken Thompson put the end inside the machine: you cannot trust code you did not totally create yourself, and no amount of reading the source will save you, because the compiler was itself built by a compiler, and that one could be lying. He closed with a moral rather than a map. Verification stops somewhere; he did not say where, and he was not trying to.
For forty years the pieces needed to say it sat in different fields. Distributed-systems theory proved which states of knowledge a group of machines can reach. Cryptography proved exactly which sets of corrupt players a protocol can survive. Security engineering drew a perimeter around the trusted computing base, the part of a system you take on faith, and admitted, in Lampson's words, that what is inside it is "not easy to figure out." Some argued the limit is social and cannot be a theorem at all. And the people who build tamper-evident logs, records designed so that any tampering shows, listed their trusted parties one system at a time, without asking whether the list was complete or why those parties and no others. Everyone since Thompson has agreed that verification stops. What nobody asked, as far as we can find, is whether the place it stops has a shape. Take a record that only grows, and take every claim you could make about it. Is the set a checker of bounded power can settle exactly describable, with everything past it being exactly what you must trust, and is that line a theorem rather than a policy? The sentence falls the day someone produces the prior work, and I will say so when it does.
Why did it go unasked for forty years with the pieces on the table? The honest answer is boring. They lived in different fields: cryptography had the tree, functional programming had the fold, databases had the time window, distributed systems had common knowledge, security logic had the trust statement, metascience had reproducibility. Each solved its own component, and nobody stood where they meet, because standing there is not a research position in any of them. We stood there because we were building a system that needed every piece at once and kept asking what they had in common. That is a vantage, not an insight the fields lacked.
I am going to claim that the question is closed, and the claim is about trust itself wherever trust concerns knowing: what is left to it has an exact structure, the same in every domain. Two things stay open, and the result says why. One is each domain's ontology, what its entries mean. The other is the decision, whether to rely on this named party for this named piece, which depends on things no record fixes. The result does not make that decision. It makes it a question a person can answer.
What we have in hand is a fundamental piece of machinery for knowing, not proposed but derived, for claims over a record, resting on two named assumptions that I state near the end. Within that bound every part of it is forced: the three conditions with no fourth, the residues, meaning the leftover kinds of trust, with none missing, the order of the climb, the shape of the certificate. Anyone who cares what that sentence claims will know exactly what it claims, and can check it when the development is public.
Start with what you already do. A lockfile pins what you depend on, not who stands behind it. A signed commit is someone's word. The CA root in your trust store is something you decided to believe, once, and stopped thinking about. The transitive dependency your dependency pulled in, that you never opened, is nobody's word at all.
Those are four different positions. Take any artifact you run and everything beneath it, transitively: sources, dependencies, their dependencies, the compiler, the keys. Call each a part, and call the whole set its closure. Every part is in exactly one of the four. Some you closed: a check you can rerun passed, on top of someone's vouch that the thing is what it claims to be. The rest is the open surface, and it splits three ways. Some of it you were given and chose to take as is: the seeds, meaning the compiler you run, the hash function, the root key. Some was vouched for by a principal you admit, someone whose word your policy accepts, and not yet checked. And some is anonymous: nobody has vouched, nobody has checked. Run the opening examples through it. Your CA root is a seed. The signed commit is a vouch. The reproducible build you re-ran yourself is closed. The dependency nobody opened is anonymous.
That is the first equation, and it belongs to the second of the paper's two calculi, the one about built things:
The open surface of an artifact, everything under it that verification has not closed, is the disjoint union of what you were given, what was vouched for, and what is anonymous. Every open part is in one bucket and one only. That split is how the accounting classifies every part, and the classifier has no fifth verdict; the theorems come later, when the buckets start to move.
The thesis of this post is under that equation. Trust is not the enemy of verification but what verification leaves behind, and it can be named, counted, and moved. The given bucket, what you chose to take as is, is not a failure but a decision. Zero trust does not exist. Named trust does.
The title is a play on "everything is a file." That slogan earned fifty years because it was literally true of the architecture, and you could hold Unix to it. I want the same bar here and the same consequence: a discipline you can hold a system to. Everything is a trust decision, and an attestation, a signed statement that you stand behind a claim, is your signature on one. Write every one of them down, sign it, and put it where it can be counted. Not trustless: trust less, and say exactly what is left.
What It Means for a Claim to Last¶
Everything above is a snapshot. The real question is what happens when the record grows. You verified something yesterday; overnight the log took ten thousand new entries. Do you check again?
Three words carry the rest, each in its plain sense:
- A record is an append-only sequence of entries: things are added at the end and nothing is ever changed or removed. Git history if you never force-push. A transparency log. A package index that only adds.
- A certificate is the thing you check instead of re-reading the record: a Merkle path, a signature, a proof.
- A claim is enduring when its certificate keeps working no matter what is appended.
Plato had a word for an opinion tied down by an account of why it is true: it becomes monimos, abiding. A record in which tied-down claims abide is what the paper calls a monimograph, and the word will matter once, near the end, for a record that is not one. The first of the paper's two calculi ranges over exactly this object, and its judgment is the one to remember:
Over the record , the claim holds by the certificate , and keeps holding over every extension of . The plus is the point: not "true now" but true from here on. The law that makes the plus honest says that if the record grows from to and endured at , then holds at : the certificate was made at , stays anchored there, and you never need a new one. The machine checks that.
Exactly Which Claims Can Last¶
Take the claim every developer knows: "this commit is the latest." It is true right now, it is computable from the record, and the next push unmakes it. No certificate, of any kind, under any assumption, can make "latest" endure. That is not a limitation of Merkle trees or signatures; it is what the claim is, a photo of a scoreboard mid-game, true the instant you took it and meaningless a moment later.
The central theorem says which claims can last, and it is a biconditional:
Determined means the record alone fixes the answer; who is asking and who wrote it do not matter. Certifiable means a checker of the power you actually have can recognize a certificate for it. Monotone means that once it is true, appending more entries cannot make it false. A claim has an enduring certificate exactly when all three hold, and the machine checks that in both directions: given the three conditions, it builds the verifier.
Why three and not four? Because there are three things in the picture: the record, the checker, and the record's growth. Each condition is one of them failing, and there is no fourth part to fail. The count is a theorem because the split is proved over every claim there is; the three parts are why it comes out at three.
"Latest" fails the third condition, and that one fact is why every transparency log in production had to grow a liveness layer, a layer whose whole job is to keep confirming that the record is still current: servers gossiping to compare what each has seen, witnesses, freshness checks. Certificate Transparency shipped its two proofs and then found it needed gossip on top. The field found that by getting burned; the calculus says it had to be so. People who build distributed systems will recognize the third condition from the other side. A result there called CALM says a monotone specification needs no coordination, meaning a system whose facts only ever accumulate can run without its machines stopping to agree, and our watcher is that coordination, bought per claim. The calculus adds a checker leg CALM does not range over, and the claim that the three conditions are exhaustive.
The three conditions say nothing about your domain, and that is the design lever. The calculus does not know what an entry means, what a signature is, or what a build does. It fixes the procedure for knowing and leaves every one of those choices to you, which means they are yours to get right. So classify the claims your system will live or die on before you build, because the classification tells you which can be checked once and which will have to be checked forever, and nothing you build afterward can move a claim across that line.
One note on where the checking stops. "A checker of the power you actually have" is a dial, and the machine checks the biconditional at two settings of it: unlimited power, and merely computable. Polynomial time, the setting most developers care about, is future work in the paper. I do not think that weakens anything. At any power a checker either exists or it does not, so the count of three is the same theorem at every setting. What changes at polynomial time is the floor: our proofs take the hash as absolutely binding, and a polynomial version would have to take it as computationally binding, which makes it a theorem in cryptography with hardness assumptions and security parameters, on a trusted base that has no usable definition of polynomial time yet. I expect it to follow with the partition untouched.
The three conditions also reach AI, and that is the application I care about most. Science in our time is increasingly done by machines, and the dispute this post opened with is, underneath, an argument about what machines did and in what order, which no record anyone keeps can say. Everyone says they care about AI safety, and almost nobody can state the question in a form a record could answer. Alignment in the large is hard, and the theorem does not settle it. But there is a small version made of claims a record can hold. "The machine did X" can be a receipt. "X serves the goal I wrote down" can be one too. "The machine is making progress toward that goal" is a claim about a trajectory, and a trajectory is a phone call: you re-measure, you never certify. And "the goal I wrote down is what I actually want" is the one the record does not fix at all, a witness's word. Every step a machine takes is a claim, and a claim can be graded by what it rests on: checked by machine, cited at source, the operator's word, or argued from other claims. The grade asks what the claim rests on, not who made it. That rule falls on me, on the machine that assisted me, and on you, because all three of us are fallible, and "who wrote it" is not a grade. Track every intermediate claim and grade it, and the whole has a grade.
Now point the same discipline at the training data instead of the working session. Imagine the training set itself graded, every claim in every entry, so the model was built from a record where each claim carried what it rests on rather than from text taken as given. In practice there would be an error ratio; the point is the picture, not a promise. A hallucination, in the second calculus's vocabulary, is an output claim with no vouch your policy admits and no check that ran: anonymous, the bucket the rest of this post says to weed out. Whether it is also false is the first calculus's question, answered only where the record fixes it. With a graded corpus you could trace every output claim to what it rests on, or flag it as anonymous, without opening the model. In so far as alignment and hallucination are questions about trust, about what a claim rests on and whether it can be checked, they are bounded by the three conditions exactly, once they are written as claims over a record at a named checker power, and I make that claim here, dated, as a prediction. What the record does not carry, intent and deception about intent, stays outside, in the witness residue with a watcher beside it, because what is wanted moves.
One step further is a conjecture: alignment in the large may be reachable by setting the machine's goal to the record itself: emit claims at the grade they have and never above it, which is the one part of honesty a stranger can check. The condition is that the machine never sets its own goals. A goal is a directive; it has no backing to check, only a signer to hold. A goal the machine appended for itself carries no signature your policy admits, so under the partition it is anonymous, and everything that rests on it rests on anonymous trust at the helm. Progress toward the goal you signed can still be measured. Progress toward the goal the machine gave itself cannot be graded at all. Autonomous execution under a human-signed goal is fine. Autonomous goal-setting is the one state the record cannot follow, and if the field means what it says about alignment, that is the state to rule out, not the one to build toward. None of this is a theory of alignment. It is the trust-shaped part of one, and the session version is how this paper was built: the claims machines made on the way to it were recorded and graded, and the paper's own claims carry those grades onto the page.
What You Can Check Without Reading Everything¶
Why does everyone reach for a Merkle tree? Is that the right instinct or a fashion?
A claim you can check from summaries alone is one whose answer over a stretch of the record combines from the answers over the pieces that tile it. The simplest form ignores where the pieces sit:
That is a list homomorphism, in the sense of Bird's theory of lists, and earlier drafts of this post gave it as the whole class. It is too narrow. Certificate Transparency's consistency proof is not of that form, because its summary depends on where in the log a block sits, so the class as first stated excluded the best-known proof of its own kind. The development now types a summary by the window it covers:
The summary of a window is the combination of the summaries of any two adjacent windows that make it up, and what kind of thing a summary is may depend on the window's endpoints. One condition is needed, locality: a window's summary reads only the entries inside that window. The machine checks that locality is exactly the condition. A summary is a fold over its window if and only if it is a local positional homomorphism, and the list homomorphisms are the case where the summary ignores its endpoints, recovered with nothing about them changed. The wider class is strictly wider: the development exhibits a summary that reads absolute position, which no position-free fold reproduces. Consistency is exhibited as a member, at the list of peaks and at the single root a verifier holds, with at most openings. It rests on the summary binding prefixes, which is collision resistance, and that is stated as a hypothesis and shown satisfiable, not proved.
For claims in this class a checker takes the whole record in at every size with a bounded number of openings, at most for a window and for a prefix, and the bound comes from the shape alone, with nothing assumed but a binding hash, a fingerprint that cannot be forged; that is the glance, the eusynopsis, from the top of the post. The development also proves the converse for schemes of this kind. Any scheme that answers windows by opening ranges that tile them and recombining the results, and that is sound, complete, and reveals no more than it must, computes a positional fold. Among such schemes the class is therefore exact, and "no more" is a theorem. The compact proof systems of modern cryptography are not schemes of that kind; they reach outside the class and pay for it with a hardness assumption. The calculus's term language was widened to match. Its terms denote exactly the positional folds, every term a fold and every fold some term, with the earlier language embedded as the position-free case, and the enduring terms among them are those read over a fixed window with a checker.
That is where the tree comes from. Because is associative, meaning you can group the pieces however you like and get the same answer, you may bracket the fold any way you like. The balanced bracketing is a tree, and the certificate for one entry is one path down it. That is a Merkle tree, and its logarithmic proof, the short chain that barely grows as the record grows, is the shape the algebra produces: the associativity made visible. The instinct was right. It is easy to say too much about the tree, so here is exactly what is true: it is optimal for certificate length among constructions that assume nothing but a binding hash, a lower bound that is Tamassia and Triandopoulos's, and constant-size alternatives exist, accumulators and vector commitments, which buy their constant with a hardness assumption.
Inclusion, "this entry is in the log," is the single-entry case, and consistency, "this log extends that one," is a positional summary over the peaks of the tree. Certificate Transparency stops at those two, and both read only structure. Read the entries instead and the same tree gives the same proof for any claim of this shape, a fold over every entry it touches. The claim can be stated after the entries it ranges over, or extended as the record grows, and as long as every piece it is built from endures, the whole endures and you can verify it at any time. Where a piece does not, the calculus names which one, and that is exactly where your checking stops.
In practice the calculus hands you an interface with four parts: what you read out of each entry, how two readings combine, what you do with the total, and which stretch of the record you range over. Supply those, and say whether your checker can compute the reading, and it tells you which cell your claim lands in and whether an enduring certificate can exist for it. Take "no package in this closure has been yanked," meaning pulled from the index. Read each entry as "is this a yank of one of mine," combine with or, finish by negating, range over the whole record so far. Determined, checkable from summaries, and not monotone: the next entry can be the yank. That claim is a phone call: you have to keep asking. Change one parameter, the range, to "as of entry 1,204," and it is a receipt you can issue once and keep. Nothing else about your system had to change.
That is the designer's job: not picking a data structure, but committing to data and metadata such that the claims you care about come out as folds over the record, and knowing before you ship which ones cannot and what you owe in their place. Leave a claim outside the class and you have not failed; you have a residue with a name, and a bill.
Five Ways to Fail, Three Cures, One Price¶
Three conditions give eight combinations. One is the verifiable case. Two cannot happen, because a claim the record does not fix admits no checker at all, so certifiability is not even a coordinate for it. That leaves five ways a claim can fail to endure, each with a named residue. The paper has the table; what a working engineer needs is the three kinds of thing you are left trusting, each with a claim you have shipped:
- The record does not fix the answer, so you trust a witness to history. "The key that signed this event was in its owner's hands." The xz backdoor lived here. Every signature on those releases was valid, and the signatures told the truth: the person who inserted the backdoor was the person who signed. What no record could fix was whether the person behind the key was who two years of patient contribution said they were. No mechanism removes that residue. A record can only make it a named person's word instead of nobody's, and mark exactly where you are relying on it.
- The answer is fixed but no checker of your power can reach it, so you trust a voucher. "This build never finishes."
- The answer is fixed and checkable and the next entry can unmake it, so you trust someone still watching. "This certificate has not been revoked." "This is the current key."
Each has a cure, and each cure is a single edit to the claim:
- Restrict the window. Stop saying "latest." Say "as of entry 1,204." That claim endures.
- Get a vouch. Let a named principal's attestation stand in for what you cannot compute. The claim now rests on their word, and the calculus writes that word down as what it rests on. A software bill of materials, the publisher's list of what is inside an image, is this cure: it rests on the publisher's word, which is why a laundered image can ship with a clean one.
- Get a witness. For facts the record does not carry, who did it and when, a witness's entry in the record. The claim rests on the witness.
Paying someone to keep watching, so the current-window claim stays alive, is not a cure, and the word matters. Gossip and heartbeats are a price, paid continuously, for as long as you insist on the claim, and much of the confusion in this space comes from treating the price as a cure. The shorter way to say the third failure was the first theorem we found on the way here: a certificate can be eternal, it can be checked offline, or it can be about now, and you may have any two of the three. Eternal and offline is a receipt. Now is a phone call.
That reframes a cost intuition most of us carry, and I held it for years: trust cost scales with the record, bigger log, more to check. It does not. The cost is per claim. A claim in the enduring class costs one certificate, forever, however large the record grows. A claim outside it costs a watcher, forever, however small the record is. Engineers have sorted claims into those two piles by trial and error for decades, and often got it backwards, building a vault where a receipt would do or handing out a receipt that silently expires. The calculus says which pile, in advance. It is also where transparency logs and blockchains part ways: not by size but by which claims they insist on. A blockchain insists on one claim a log does not, that there is a single current tip, one true end of the record, and this is it, and that claim is not monotone. Consensus, every machine in the network stopping to agree, is its price. That is what the bill is for, and the discipline is to pay it for the one claim that needs it, on purpose, and for nothing else.
Where an Artifact Stands¶
A dashboard that counts "unverified vouches" will go up as your system gets healthier, right up to a point, and only then start falling. If that sounds like a bug in the dashboard, keep reading.
The first calculus ranged over the record. The second ranges over composed artifacts, things built from other things, which the record does not carry: two artifacts can share one record and differ in what is still open beneath them. Its judgment reads: given the evidence admitted so far, the artifact stands on an open surface and a standing basis.
is the evidence admitted so far, the vouches and checks your policy accepts, with a retraction modeled as an omission. is what is not yet closed beneath . is the admitted evidence it rests on. As grows, only shrinks and only grows. They move in opposite directions and never trade places.
The climb has two marks on it, and a distance between them:
The floor is where nobody anonymous remains under the artifact. The ceiling is where only what you chose to trust remains. The distance is how many vouches still await a check.
From here the machine-checked results are no longer true by construction. Both marks are genuine biconditionals: they fail in one direction under a classifier that mistakes an undeclared leaf for a seed, a part nobody declared taken for one you chose to accept, and we know because ours did until it was fixed. Nothing closes without both a re-runnable check and someone's vouch behind it, so you cannot reach the ceiling without passing the floor, and the order of the climb is a theorem, not a policy. And the distance can rise before the floor, because an anonymous part gaining a vouch is honest progress that looks like regress on the count; it falls only after the floor. The dashboard was right and the intuition was wrong.
The floor is the one piece of guidance I would hand any team tomorrow, and it shows where good practice turns into bad. Nothing stops you from admitting an anonymous part; the calculus represents it fine. But an anonymous part is the one position in the partition that nobody decided, and with one anywhere beneath an artifact you cannot guarantee the provenance of anything above it. That is not an opinion about hygiene but what the partition says, and you can only say it because every term in it is exact. So treat anonymous trust as the smell, and make the floor your admission criterion: nothing enters that nobody has vouched for. Then close the vouches. Systems that skipped straight to closing, without a floor, left anonymous parts they could not see, because a part nobody has vouched for is on nobody's list, and their dashboards said nothing because there was no count under them.
The Floor of Two Assumptions¶
Thompson said verification must end somewhere. Here is where.
The result grants exactly two things and names them. First, that the hash binds: two different records never share a commitment, the fingerprint that stands for the whole record. We state that as absolute, which is an idealization, and we own it; real hash functions are collision-resistant against bounded adversaries, not collision-free, and the paper says how far that is from absolute. Second, that the verifier you run is the one you think you run. That is Thompson's moral read as a premise: you cannot check your ruler with the same ruler. Neither grant is an axiom of the mechanization. Inside the proof the axioms are Lean's own three and none of ours: entries and contexts are type parameters, a theorem that needs a context, or two that differ, states that as its own hypothesis, and a check in the build fails if any theorem's axiom list grows. The two grants sit beneath the model. The proof does not see them.
Everything above those two is a statement about what a record can carry, and this is where the old question ends. Socrates knew there was an edge to knowing and could not say where. Thompson found it in the compiler and left it as a moral. Here is the edge, drawn: two grants beneath it, three named pieces of trust above it, and no fourth. Verification ends at the floor; everything past it is named, counted, and its cost known, and nothing above the floor need be anonymous.
Three Instances¶
If the shape is real it should show up where nobody was thinking about packaging, and it does: wherever anyone keeps a record of claims and wants an answer to survive the record's growth, which is a much larger place than software. Version control and transparency logs, obviously. Ledgers and land registries. The rules of evidence, which already let a hash stand in for a witness. Causal inference, where the record not fixing the answer has its own name. History, which is a record with witnesses and nothing else. Science. The justice system. The class is abstract, so nobody will finish that list, and the paper does not try. Each domain brings its own entries, its own checks, and its own idea of a vouch; the calculus brings the three conditions and the count. Here are three, each further from software than the last.
Packaging. Nix got the first move right twenty years ago: compute the closure before the build, so every input has a name before anything runs. I spent a decade inside that model and said last time what it costs. What I did not say is exactly where it stops. A derivation, Nix's build recipe, exists before the build and is addressed by its own hash, but nothing binds a named principal to a claim about it until after the build, when a cache key signs the output. That is an attestation after the fact, and in the calculus an attestation after the fact is a citation, not a verification: a pointer at a history the record never fixed, graded as a witness's word. The closure is a map of the floor, but nobody in it has vouched, so the map is not the floor.
Signing derivations up front would not fix it. Nix in practice is a just-in-time attestation machine: this expression yields this derivation, which yields this output, decided at evaluation time, with no object anywhere that states the claim ahead of it. A derivation is a recipe, and a recipe is the wrong shape for a claim. It carries too much, every flag and every path, and it is coupled to the bytes on disk, which is what makes it rigid and what keeps real content addressing out of reach for the reasons the last post gave. The discipline is old and plain: separate the concerns. Attestations belong in their own append-only record, not welded to the data they are about.
That is what the atom is. An atom is a minimal, signed, versioned statement of intent, sources plus manifest plus lock, entered into its own append-only record before anything is built, with the build derived from it step by step in that order. The order is the whole point. Declared first, "this was built from those" is fixed by the record. Built hermetically, sealed off from anything not declared, a stranger can check it. Anchored in a record that only grows, it stays checked. Those are the three legs, and they have a practical face: you check the atom before you run the build, walking its closure signature by signature, and if one is wrong you stop walking. Nothing has been built yet, so nothing has to be thrown away. The atom is the claim to the recipe and to the content underneath it, and every vouch on every part is a signed fact in the same record. That is the field I said the metadata should carry. It turned out to be the floor, with the accounting above it.
Identity. This is where the question was born. Identity is more basic than packaging, because packaging depends on stable identity, and nothing deployed has solved it well. Zach leads Cyphr, our lab's self-sovereign identity protocol, and I work on it with him. In Cyphr, who you are is a genesis commitment, a first signed entry that fixes your root, and an append-only chain of signed key events under it: this key added, that one rotated, this one revoked. Your whole identity, keys and history, is one fingerprint. Of the claims the chain fixes and a checker can settle, the monotone ones endure and the rest are claims about the present, and the one Cyphr pays a watcher for is "this is their current state," a tip claim, a claim about the current end of the record. It cannot endure, and nothing you sign can make it. That is why key transparency needed gossip, why rotation needs a record rather than a replacement, and why Cyphr's design has a witness network: the watcher the calculus names, bought for that one claim.
The attack we were designing against is the split view, where a server shows two people two different histories. Working through it in the calculus gave us a sentence I keep using: evidence of a lie endures, evidence of honesty never does. Two conflicting signed heads are a monotone fact; append anything you like and they still conflict. "The log has been honest" is only ever true as of now. That asymmetry is why gossip works at all, and it fell out of the classification before we had a name for the classification. Zach's insight, which partly inspired the question, is the middle rung of a ladder of names: a content-addressed name fixes what; an attestation-addressed name, the fingerprint of content and attestation together, fixes what and who attested; a position in an append-only record fixes what, who, and after what. The mechanization carries an identity instance beside the packaging one, a hash chain of key events with view consistency shown non-monotone, and the tip claim shown non-monotone in the shared core, so a reviewer can watch the same core do both.
Science. A reproducible result is a claim the published record fixes and a checker of bounded means, a lab with the equipment, can settle. A citation is a pointer at the record where the claim is to be verified. A result that cannot be reproduced from what is available is a vouch, the authors' word, and an honest literature would grade it as one. Science has no monimograph: no shared append-only record that a finding is entered into under a commitment, and a retraction that deletes rather than appends breaks the chain. So a finding's endurance is claimed, never judged. The opening of this post said what that costs, and the closing sections say what would have to change. The full argument is the book's.
One thread runs through all three, and I keep seeing it in science and open source alike. A result whose inputs are withheld is a vouch, the authors' word, and that is the reproducibility failure. A commons whose admission is keyed to who you are converts, for everyone it excludes, closures into vouches, and that is the open-source failure. Same bucket, reached by two routes, withholding and identity-keyed admission, and cured the same way: inputs in the record, and admission by a check anyone can re-run. That is not an analogy between two fields. It is one structure instantiated twice.
Not Trustless. Trust Less.¶
Science is not the only commons in this argument. Open source is the other, and I have argued twice in this series that a commons cannot be run as a business without ceasing to be one. The calculus gives the structural half of that in one line: nothing counts as verified unless the check is one you can run again yourself, so an input that is kept from you can never be verified by you, or only by leaning on a cryptographic assumption, and every other route to it is someone's word. Both commons are failing in public, open source in burned-out maintainers and captured governance, science in results that do not hold up when someone finally reruns them, and they depend on each other: without science, civilization cannot scale or even sustain itself, and the science that runs on software runs on the open-source commons. Good behavior does not scale for either. A record whose claims carry their grades does, and it is what both lack and both need. I have said before that something formal and distributable is what it takes to scale science past its current breaking point without giving up integrity; the discipline is the same for both.
The industry's answer to every supply-chain incident of the last decade has been more of the same: more signatures, more scanners, more dashboards. Each hides a trust decision, and the decision is the part nobody writes down. A signature says who signed and nothing about what that is worth to you. A scanner reports what it found and nothing about what it could not have found. A dashboard counts what it was told to count, and without a floor under it the number means nothing. None of it is wrong, and all of it is trust nobody wrote down: the decision to rely on it lives in someone's head, where nobody can audit it.
The discipline that replaces it is short enough to fit on a card, and every line of it is something the calculus says you can do, not something it says you should.
Classify before you build. Decide which of your claims must be receipts, and shape your data and metadata so those claims come out as folds over the record, built up from the pieces, because those are the claims whose proof keeps as few pieces as a Merkle path however large the record grows. Where a claim cannot, know which condition it fails and name the residue you carry: a witness, a voucher, or a watcher.
Weed out anonymous trust. Admit nothing that nobody has vouched for, so the floor is where you start rather than where you hope to end up. That includes goals: a machine's goal carries a human's signature or it does not enter the record. Then count the distance to the ceiling and climb it, vouch by vouch, at whatever pace you can afford.
Pay for watching on purpose. Some claims are phone calls, and you will keep making the call for as long as you insist on them. Insist on as few as you can, know which ones they are, and put the cost where you can see it.
Grade your own claims. Never state a status above your backing. Checked by machine, cited at source, vouched by a named party, or argued in prose: those are different things, and whether a person or a model made the claim is not one of them. A reader who cannot tell which you mean has no way to trust you correctly. It is the only part of the discipline anyone can check you against, and the part that makes the rest honest.
No law compels any of this, and the theorem holds whether or not anyone acts on it. But everything is a trust decision either way, and the only open question is whether you make yours explicitly. If you claim your system is verified, or your result reproducible, or your identity yours, the check now exists and it will be run.
I did not fully realize, in the first drafts of this post, that its very title is a political statement. Yet it is one. There is a slogan in my field that all software is political, and it is half right. The consequences of widely used software are political, inevitably, because people have to live under them. What the slogan gets wrong is the step from there to treating the record itself as a matter of opinion. What a record can bear has three sides and a floor, and that stays true whoever is asking and whatever they would like it to say.
Science rests on its literature and its data, law on its evidence and its precedents, finance on its ledgers, and each of those is a record that is supposed to grow and never be quietly rewritten. For a long time "as sound as we can make it" ended the conversation about any of them, because nobody could say what was possible. Now that the possible has a shape, the excuse is gone. Where a check can be finished, leaving it unfinished and asking for trust in its place is work left undone, with someone else carrying the risk. How much of that anyone may be excused depends on their office. Nobody expects a citizen to audit the grain stores. The official in charge of them has no such excuse.
That last point is old, and it is the retrodiction promised at the top. The theorem says no institution can eliminate what is left to trust; the most it can do is name who holds each piece and keep them answerable. The question of what it means to know something comes down to us from Athens, and Athens also ran its city on that arrangement. A man was examined before he took office, the dokimasia, and when he left it he rendered his accounts to a board of auditors, the euthyna; until he had, he could not leave the country, dedicate his property, or make a will. "In this city, so ancient and so great," Aeschines told a jury, "no man is free from the audit who has held any public trust." In Attic Greek, epistemology and civic accountability shared a vocabulary. When Socrates demands that a man give an account of what he claims to know, the phrase is the one the auditors used of a magistrate. English later split these into two subjects with separate words. The theorem says the Greeks had it right: what is left to trust has one structure, whether the claim is a philosopher's or an official's. They had the practice and the reason for it. They lacked the proof that what they were auditing has three shapes and no more, and that took the computational sciences to supply. Audited accounts are older than Athens; what Athens has is the practice and the theory together on the record.
The arrangement deserves a name, and the honest one is theirs. I will call it the euthynic politic. It has a record that grows and erases nothing. It has a gate: nothing enters the record as settled unless a check settled it, or a named person vouched for it where no check was possible. And it has an audit: whoever holds any part of what is left can be called to account for it, and no office is exempt. In plainer words it is receipt accounting, applied to everything that asks to be believed. For something concrete, picture a social platform whose ranking rewards what holds up over what spreads, where a claim rises as it gathers evidence anyone can rerun and sinks when it is refuted, and every vouch has a name on it. Building that is an engineering project. The theorem was the part missing until now.
My own place in this is on the record. I came to it through industry. I have worked professionally in this field for years, most of them on a single hard problem, and that problem led here. I did it outside the academy, alongside people of that caliber, disagreeing with them often and applying something like this method before it had a name. Readers of this blog know I have argued for a grounded politics before; nothing here depends on any of that, and the claims in this post stand on their own evidence. Much of the pressure that holds the status quo in place is ordinary and forgivable: deadlines, payroll, engineers trying to ship and eat. Some of it is not. I was pushed out of professional spaces, NixOS among them, for challenging people whose standing depended on things staying unclear. Submitting this very post to lobste.rs got me banned there. There are now whole profit centers built on a murky foundation for what counts as known, and the largest are the AI firms, which are selling fear to buy regulation that would secure their lead. Those adversaries are better equipped than I am by any ordinary measure. Resources decide an argument conducted in confusion, and they decide much less once there is a count anyone can check. This position is therefore a defense of myself as much as of the work, and silence would not have spared me the need for it. Once you have seen that what is left to trust has a shape, you cannot work honestly while pretending it does not.
That is the whole of my politics here. It is a politics against confusion, the kind that is eating our institutions from the inside: keep the record honest, and keep the commons whole, which is the argument I made about open source in Anamnesis and now hold for every institution that keeps a record and asks to be believed. It belongs to no party, and it applies to anyone on any side who asks for trust where an account could be given. On the question of how we know what we know, we are leaving the realm of opinion, and anyone who prefers it murky will have to say so out loud. For those willing to accept what it asks, it is a fixed point to steer by.
What We Claim, What We Do Not, and What Comes Next¶
All of this is technical, which is the other reason nobody gave the whole problem a structure: each piece was hard enough on its own, and holding all of them at once looked like a philosophy project. It is not, once the pieces are in hand: three conditions, three residues, two marks, and a count. What takes discipline is keeping hold of what we are actually talking about, which is not trust in the abstract but verifiable truth, and where its edges are.
Piece by piece, our contribution is small: an exhaustive bound, and two calculi for working with claims coherently, tying together things the fields already knew. That is how a field matures: decades of partial understandings, each sound in its corner, until someone puts the pieces in one place and the folklore turns out to have a shape. The shape is what closes the book, because a count is not a matter of taste. Since we found it, it has explained after the fact more than we have had time to write down, and it has shaped two protocols in advance, the atom's declare-first record and Cyphr's witness layer. Standard formulations, a machine proof, and a structure that has explained things after the fact, in one case some twenty-four centuries after, and predicted one thing before, the scaling result above: that is why we are confident, and the only reason.
The order things happened in, for the record. The opener told the first half: two problems that turned out to be one, and then the trichotomy, the three-way split of what is left to trust. After that I built a record system to keep long AI-assisted sessions honest: graded claims, signed entries, an append-only log, an open surface of unbacked claims and unanswered questions. It adheres to the trichotomy; I do not claim it is formally sound against the calculus. Using it showed me the trichotomy alone could not account for what it had to track, and that is where the second calculus came from. The same system then built the paper, which carries a reviewer's guide, one row per claim with its grade and its backing: that system projected onto the page.
The method has a name, and we claim it as ours: claim factoring. Two verbs. Factor: write every claim with what backs it, a check that ran, a named witness, a derivation from other claims, or nothing, so that a document has a visible open surface exactly as an artifact does. Contend: send each unbacked claim to up to n reviewers, human or machine, in contexts that cannot correlate, so none sees another's verdict until you decide; what survives is backed, cut, or left open by name. The first verb is the one nobody had, and it is why the second was always hard: without your claims sorted by what backs them, there is nothing to aim the cross-examination at. Its known limit is that when reviewers converge on a general claim whose narrow form is what each actually checked, more reviewers cannot break the tie, and the escalation is to someone holding a different model of the problem. The results above were reached under it, this post was written under it, and you can run it tomorrow.
I have said elsewhere that if nobody wants to listen, I will be content not to take part. Until then I will point at a dated post, a paper going to review this month, and a mechanization that adds no axiom of its own, and say: check it. That is the only kind of authority I want, and the only kind this result allows anyone.
Thompson's moral was that you cannot trust code you did not create. The moral that follows from the model is its complement: you can trust exactly what you can re-run, from anyone. Closure is keyed to re-runnability, and who you are enters the model in one place only, the admission policy that says whose checks count. So a commons that refuses a re-runnable check on any axis orthogonal to whether it runs, whatever the axis, converts closures into vouches for everyone it excludes, exactly as a proprietary policy does. Identity-keyed admission is what makes a commons someone's business. "Show me the code" was always the right instinct. Its grown-up form is a policy: admit by corroboration, not by identity, and let the record say what stands.
We claim, checked by machine. The open surface partitions exactly into given, vouched, and anonymous. A claim admits an enduring certificate exactly when it is determined, certifiable, and monotone, and trust is the complement with three named factors and no fourth. The provenance floor and the total ceiling, with the order of the climb a theorem and the distance a count. That among schemes which open ranges of a record and recombine them, the claims with bounded proofs are exactly the finalized positional folds. Until the development is public, these reach you as our report of a check. Once the paper is admitted, anyone can rerun them.
We contend, on our own word for now. That the cost of trust is per claim, not per record, which follows from the theorem by argument rather than by machine. That the bound held at scale in our engine. That these results apply today and not only once a journal has said so: to the record science keeps, to the commons of open source, to the institutions that ask to be believed, and to the question of what a machine's claims rest on. That the standard they imply, an account wherever one can be given and a name wherever it cannot, binds anyone who keeps a record and asks for trust. Some of this becomes corroborable the moment the paper is admitted. That it holds now, before then, is our contention, and the burden of it is ours until then.
We conjecture. That the polynomial-time form of the theorem follows with the partition untouched. That alignment in the large can be expressed by aligning a machine to the record under goals a human has signed; that one is a conjecture of this post, not a claim of the paper.
We do not claim. Anything about degree of trust. Delegation between principals. Revocation dynamics. What the record does not carry: custody, authorship, intent. That science is, formally, a monimograph; it is not, and that is the point of the book.
The field found first. The Merkle tree. The liveness layer under every deployed transparency log. Computing the closure before the build. Attestations as vouches, which in-toto and SLSA built around this boundary without stating it.
What all of this asks for is nuance, and nuance is where the contest is being lost. Confusion has the advantage of simple language: if we do not do this, that will happen. Answering it means asking what the claim rests on, precisely, and then asking the same of everything it depends on. No person can carry that unaided at the scale our institutions now run at, and no institution does, which is where they break down. It is also why the discipline has to be assisted by machines, the same kind that are making the problem worse. A record that grades its claims can carry the nuance people cannot, and hand each of us a question small enough to decide. The structure for building one now exists. Until the paper is published, part of that statement rests on our word, and that burden is ours.
Verify all you can. Then decide what to trust of what remains. What remains has three names.