Nobody Is Paid to Delete

Every serious engineering system accumulates a corpus of rules about itself. Coding standards. Lint configurations. Pre-commit checks. Runbooks. The file at the root of the repository that tells the AI agent how to behave. Each entry was added by somebody who had just watched something go wrong and did not want it to happen again, which is a good reason, and each entry is individually defensible, which is the problem.

These corpora only grow. Not usually. Structurally.

I want to make that claim precisely, because "documentation rots" and "bureaucracy accretes" are folk observations that everybody nods at and nobody acts on. The precise version is sharper, and it has a fix, and the fix is not the one you would reach for first. In fact the one you would reach for first is worse than doing nothing, and I can show that.

The claim

A corpus of rules written by authors whose tenure is shorter than the artefact's life grows without bound, because deletion is a dominated strategy for every author, and no volume of instruction can make it otherwise.

Three conditions produce this, and where all three hold I would expect monotone growth:

1. Authorship is credited. Adding a rule is visible diligence.
2. Removal carries asymmetric personal risk. If the rule you deleted turns out to have been load-bearing, that is your name on the commit.
3. The author's tenure is shorter than the artefact's life. Whoever writes the rule is gone before its cost is paid.

The third condition does the heavy lifting, and it is worth noticing how widely it holds. A legislator gets credit for a statute and carries risk for repealing one. A compliance officer is rewarded for adding a control and exposed by removing one. The author of an internal policy will have moved on before anybody feels its weight. And an AI agent working a single session is the limiting case: it is scored on what it did in front of you and then it ceases to exist, so it bears exactly none of the cost of what it wrote into your always-loaded context.

What is proved, what is argued, and what is proposed

Because the rest of this leans on different kinds of claim, here is the inventory.

Proved, in Lean 4, with the kernel checking. A module of a few hundred lines. It builds, contains no sorry, and no theorem in it depends on any axiom beyond propositional extensionality and quotient soundness, which I checked with #print axioms rather than assuming.

Argued from the record. The section on conservation laws draws on published evaluations of national regulatory-budget schemes. I have read secondary summaries rather than conducting my own evaluation, and I say so where it matters.

Predicted, and testable on your system rather than mine. I am not going to publish an audit of my own tooling. Instead I will state in advance what I expect a particular measurement to find on any sufficiently old rule corpus, so that you can run it and tell me I am wrong. That is a better use of the claim anyway: a self-audit by an interested party is weak evidence, and a prediction that survives somebody else's data is strong evidence.

Proposed, and not yet built. Everything in the final section.

I should be blunt about what the Lean is worth, because the temptation to use "I proved it in Lean" as an authority move is strong and I want to disarm it now. The proofs are trivial. One of the central ones says that truncating a list to length B yields a list of length at most B, and it is two lines because that is all it is. Nothing here is a mathematical result and nobody should read it as one.

What the formalisation does is force every assumption into a named hypothesis where it can be attacked, and force me to be exact about which conclusions survive which assumptions. All the content sits in the definitions and none of it sits in the proofs. That is a legitimate use of a proof assistant, and it is a much smaller claim than "formally verified".

The four moves and their payoffs

When an author discovers a problem, there are four things they can do about the corpus, on top of fixing the problem itself. Record nothing. Write a rule so it cannot recur. Write a rule and wire up telemetry, so somebody later can tell whether the rule ever fires. Or retire a rule that has become redundant.

Price those four from the author's point of view, remembering that their point of view ends when their tenure does.

Writing a rule is the best available move. Visible diligence, obligation discharged, and the cost falls on people who are not in the room.

Recording nothing is punished, often deliberately: most engineering cultures have some version of the principle that letting a known failure recur is worse than the failure itself.

Wiring telemetry costs strictly more than not wiring it, for identical credit. The sensor is a pure cost to its author and a pure benefit to a stranger. This is why so many rule corpora cannot answer the question "which of these has ever done anything?" It is not an oversight. Nobody was ever paid to answer it.

And retiring a rule is the only move with no reward channel at all. The benefit accrues to people the author will never meet. The risk lands on the author. There is usually no field anywhere in the system that could even record "this person correctly identified a rule that had stopped earning its place".

So the author writes. Every time. And the corpus ratchets.

The kernel corrected me

While formalising this, I asserted in prose that retirement was the worst of the four moves. The kernel refused, and it was right.

Under the parameters I had chosen, recording nothing scores worse than retiring, because the penalty on letting a failure recur is larger than the blame risk of a removal. Which of the two losing moves is worse depends on those two quantities, so it is a parameter question, not a structural one. What survives without qualification is the ordering that matters: writing strictly beats retiring, always, whenever the author is short-tenured.

That is a small correction and I am reporting it because the alternative is to present formalisation as decoration on a conclusion already reached. If the kernel can only ever agree with me, I am not using it, I am quoting it. It is also, honestly, the one place in the whole exercise where the formal machinery earned its keep rather than tidying up after me.

Why the obvious fix is strictly counterproductive

The natural response, and it was my first, is to write a rule that says: when you add a rule, retire one.

This cannot work.

Cooperation in repeated interaction is sustained by the shadow of the future. Reputation, reciprocity, the threat of sanction in later rounds: all of it requires that the party being disciplined plays again. A short-tenured author does not. In the limiting case of an AI agent, the next instance inherits your files, not the previous instance's reputation. There is no round two in which anything could be collected.

An instruction addressed to an author's concern for the future is therefore a threat against a player who has no future. It is not weak. It is void.

The formal version is short. If the author's incentives do not depend on the text of the corpus, then no edit to the corpus can change what the author chooses, and this holds for every possible edit, of any size, however emphatically worded. Editing the text is precisely the operation the incentives are invariant to. That is a one-line proof about a strong assumption, and the assumption, not the proof, is where the argument lives. If you want to attack this essay, attack that assumption.

The instruction is not merely ineffective. It is itself a rule, occupying space in every future reading, forever. So it strictly increases the cost it was written to reduce, while leaving behaviour exactly where it was.

Read the contrapositive, because that is the design lesson. To change the behaviour, the incentives must become a function of the corpus. That is what a gate does at the moment of the write, and what a paragraph, read sympathetically by a well-meaning author, cannot.

Prior art, because none of this is new

Three literatures got here first.

Cache replacement. This is structurally an eviction problem, and computing has known for fifty years that a cache without an eviction policy is not a cache, it is a leak. Least-recently-used, least-frequently-used, adaptive replacement, second-chance and victim caches all exist because "keep everything useful" is not implementable. What follows is approximately least-frequently-used with a protected segment and a victim cache, and I would rather say so than imply novelty. What is not standard is applying it to a corpus of instructions, where entries are read by an intelligence rather than fetched by an address, and where the value of an entry is contested rather than observed.

Regulatory accumulation and regulatory budgets. Policy accretion is documented, and one-in-x-out rules are the standard proposed remedy. Their track record is below, and it is bad.

Goodhart, and Campbell before him. Any measure adopted as a target ceases to be a good measure. I did not merely fail to anticipate this. I had already been caught by it, which is the next section.

The cap that measured the wrong thing

Suppose you notice the growth and impose the obvious control: a hard size cap on the file, enforced automatically, so it cannot grow past a limit.

Watch what that produces. As the file approaches the cap, the response is not deletion. It is relocation: move the text into a linked document and leave a pointer behind. The cap is satisfied continuously. Nothing was removed. The total a reader must load has not fallen, and may have risen, because now there is a pointer as well as the text.

I did this to myself and did not notice for months, because the check kept passing. The cap measured one file. The thing that actually costs is the total a reader must take on across every file the pointers lead to. Those are different quantities, and the gap between them is exactly wide enough to drive an entire corpus through.

The general form: a budget over a quantity that can be relocated is not a control, it is a redirection. Hold that thought for four paragraphs.

Two growth laws

The dynamics are not subtle.

Under free addition, where new rules arrive each round and none leave, size grows linearly and without bound. There is no steady state, ever. That is definitional rather than deep, and the point of stating it is that nothing about it depends on the rules being bad, or the authors careless, or the corpus disorganised. Good rules accumulate exactly as fast as bad ones.

Under a conservation law, where new rules arrive and the corpus is then truncated to a fixed budget keeping the highest-ranked, size is bounded by the budget after the first round, unconditionally. No assumption about the arrival rate, the starting corpus or the authors is required.

The contrast is the whole argument, and notice where the content sits: the proof of the bounded case is three lines, because all the work is in the step function rather than in the theorem. That is how it should be. A design that needs a clever proof to establish its safety is a design whose safety depends on the proof being right.

There is a related point about what compounding actually requires. A system that only accumulates is not compounding, it is silting up. Compounding needs both terms: a high arrival rate of things worth keeping and a strictly positive rate of forgetting. With the forgetting term at zero, more learning produces more sediment and nothing else. It is possible to spend a very long time optimising the first term without once setting the second, and I recommend against it.

The part where this has been tried, at scale, and abandoned

Here is the strongest objection to the fix, and it is not hypothetical.

Conservation laws on rule corpora are a real policy instrument with a real record. The United Kingdom ran one-in-one-out from 2011, tightened it to one-in-two-out, then to one-in-three-out under the Business Impact Target, requiring three pounds of savings for every pound of new business cost. The European Union operates a one-in-one-out approach. The United States ran a two-for-one requirement under Executive Order 13771. The United Kingdom then discontinued regulatory offsetting during the 2017 Parliament.

The criticisms map onto the proposal almost item for item. The quotas were called arbitrary, imposed without evidence that the existing stock was excessive. The accounting captured business costs and ignored benefits that were not business costs. And the framework was gamed through its own scope: many regulations were simply excluded from the count, so the target could be met while the stock grew.

That last one should stop anybody about to propose a rule budget, because it is the same failure as the size cap four paragraphs ago. Text moves out of the measured place into an unmeasured one. The exclusion need not be adversarial; it is the path of least resistance, taken by well-intentioned people, and it produces a passing check on a growing corpus.

My defence used to be a disanalogy about measurement, and I now think it is only half a defence. Here it is, and then here is the half that fails.

The half that holds. In regulation, the cost of a rule is contested, estimated, and scored by the party proposing it. An impact assessment is a forecast, its methodology is negotiable, and scope is decided by interested parties. In a rule corpus, cost is not estimated, it is counted: how much a reader must take on is a measurement, taken mechanically at the moment of the write, with no forecast and no discretion. That genuinely removes one of the two failure modes.

Which yields a prediction I would rather state now than defend later. If the size measure ever becomes negotiable, the mechanism will be gamed exactly as the Business Impact Target was. The moment anyone argues that a rule should not count because it lives in a linked document, or because it is important, or because it is temporary, the scope exclusion is back and the budget is theatre. The measure must cover everything actually loaded, with no exemptions.

The half that fails, and it is the more important half. Measuring cost exactly does nothing about measuring benefit. The obvious value proxy is how often a rule has fired, and firing frequency measures activation, not harm prevented. So the budget prices the denominator precisely and the numerator badly, which is exactly the criticism levelled at one-in-two-out: it counted the costs and ignored the benefits that were inconvenient to count. The flaw I was congratulating myself on avoiding reappears one level down.

I do not have a good answer. I have a partial one, which is that the relevant measurement is usually available and almost never taken.

The measurement I think you should run, and what I expect it to show

Take any rule corpus in your organisation more than a year old with some form of automated enforcement. For each rule, ask one question that requires no judgement and no taxonomy:

Has this rule ever actually stopped anything?

Not "is it good". Not "does it fire". Has it ever blocked an action that would otherwise have proceeded. In most systems that is a field in a log, or can be made into one cheaply.

Here is what I predict, stated so you can falsify it:

• The distribution will be brutally long-tailed. A small number of rules will account for nearly all of the actual enforcement, and the majority will have stopped nothing, ever.
• A large fraction will carry no instrumentation at all, so the question cannot even be asked of them, and that fraction will correlate with age.
• The ratio of advisory activity to enforcement activity will be far higher than anyone in the organisation would guess before measuring.
• And the rules you would have guessed were overhead will not be the ones that turn out to be idle.

That last one is not a rhetorical flourish, it is the part I got wrong. I reached first for a measure that depended on my own classification of rules into "real" and "bureaucratic", and it made a satisfying story. A reviewer pointed out that a self-selected taxonomy from an interested party is not evidence. He was right, and worse: when I ran the measurement that needs no taxonomy, it contradicted the classification I had been about to publish. The rules I was ready to call overhead were not the idle ones.

So distrust your intuition about which of your rules are dead weight, and go and look. If you run this and find a flat distribution with broad enforcement coverage, I am wrong, and I would genuinely like to know.

One caveat I will not bury, because it cuts against my own proposal. A block is not an error prevented. It is an error alleged, and the corpus's owner gets to overrule it. Blocks are a better proxy for value than activations, which is a statement about how bad activations are rather than a recommendation of blocks. Any eviction policy ranking on them is ranking on a proxy it knows to be weak, and should therefore be built to be cheap to reverse. Which it needs to be anyway, for a different reason.

Why eviction must be demotion, and never deletion

Retirement was dominated for two reasons, and a budget only fixes one. A conservation law makes eviction the price of the thing the author already wants, so the author evicts. But if eviction means deletion, the blame risk remains: remove the wrong rule and something breaks, with your name on the commit.

Make the eviction reversible and that term goes to zero. A demoted rule leaves the active surface and stays in the repository and in version control. In the formal model, restoring after demoting is provably the same as restoring directly, which is a precise way of saying that demotion destroys no information. Deletion admits no such law.

This is not a softening for comfort. Reversibility is the term that made retirement dominated in the first place. The author who demotes a rule to make room for their own is not being altruistic and is not thinking about the future; they are paying a price engineered to be near zero for something they wanted anyway. That is the entire design: a mechanism requiring no forward-looking preference, because a short-tenured author cannot supply one.

It also answers the strongest technical objection cheaply. A rule that never fires might be preventing problems precisely by existing, and I cannot refute that, because firing frequency measures activation and not harm prevented. Under demotion the objection costs nothing to accommodate: if the problem recurs after a demotion, restore the rule and record the recurrence as the observable that earns it permanent residency. An unfalsifiable claim about deterrence becomes a testable one, at no cost if the claim is true.

Two design details I got wrong on the first pass.

Hysteresis. A naive demote-and-restore loop oscillates. Demote for inactivity, the problem recurs, restore, it sits quiet, demote again. That is a feedback loop with no damping and it will flap, generating churn indistinguishable from noise. A restored rule must ratchet into a protected segment permanently, or at minimum have its observation window multiplied on each restore. The restore is evidence, and evidence must ratchet.

Category exemption. Rules guarding secrets, outbound communications and deployments should be exempt from automatic demotion, because for those the asymmetry runs the wrong way. A rare firing may be the only thing standing between a normal week and a disclosed credential.

Four ways this fails

It rewards compression rather than restraint. A budget denominated in size creates an incentive to write terser rules, not fewer, and terseness in an instruction corpus buys ambiguity. A rule compressed until it fits has lost the worked example, the founding case and the boundary condition, which are the parts that make it followable. The partial answer is to budget the count of resident rules alongside the size, so compression cannot manufacture headroom.

Value is measured badly, as above. This is the one I would bet on if it fails.

Legibility damage. Ranking by activation makes the corpus legible along the one axis that is cheap to observe, and what survives will be whatever value happens to correlate with firing frequency. Rules that shape how a problem is approached, rather than blocking a specific action, will never fire and will always rank last. The category exemption is a crude guard and I do not think it is sufficient.

The owner overrides it. A budget adds friction to the work of the person who installed it, and that person holds the override. A mechanism its principal routinely bypasses is not a mechanism. If the override rate is high after thirty days, the honest conclusion is that the design is not incentive-compatible for its owner, and it should move from blocking at the moment of the write to silently truncating a generated view by rank, which never asks anybody anything.

How far this generalises

The mechanism generalises to any corpus whose cost can be counted rather than estimated. That plausibly includes agent instruction files, dependency manifests, feature flags, alert rules, lint configurations and CI pipelines, all of which have exact, non-negotiable footprints. It does not generalise to regulation, and the record says it did not.

There is also a claim I am deliberately not making. I have not shown that any particular corpus is too large. I have shown that an unbudgeted one is unbounded, which is different and weaker, and that the mechanism which would bound it usually does not exist.

Who loses

Anyone whose contribution is measured by what they added. A conservation law makes additions rival. That is uncomfortable in exactly the way it is meant to be, and it will feel like a downgrade to whoever writes the most.

The instinct that produced the corpus. The impulse that says "never again" and reaches for a rule is a good impulse and it builds valuable things. Under a budget it must be told, routinely, that this particular never-again is worth less than one already resident. That is a real loss and I do not think it is avoidable.

Rules that shape judgement rather than block actions. These never fire and always rank last. Under this policy they are the systematic casualty, and the category exemption does not cover them.

Three objections

"You are optimising the wrong variable. The corpus is the valuable thing."

Right on the premise, wrong on the conclusion. A mature rule corpus is often worth more over its life than any single deliverable it has guarded. That argues for making it measured and bounded rather than leaving it unbounded, and it argues much harder for something I have under-emphasised: an asset that valuable should be generated, schema-validated, versioned state with per-rule identity and provenance, not a tree of hand-maintained prose files mirrored by hand across however many tools consume them. The mirroring cost is the product of the tool count and the rule count, and in an era when nobody can name the agents they will be using in two years, both terms are growing. Stable identifiers also make a parallel-write collision visible: two paragraphs merge silently, two identifiers do not.

"Firing frequency is a biased proxy and you know it."

Correct, and the concession is larger than a caveat: it means the proposed budget solves half the problem it claims to. The mitigations are demotion rather than deletion, category exemptions, hysteresis on restore, and a requirement that a never-fired rule asking to stay resident must name an observable that would distinguish deterrence from deadness. If this fails, it fails here.

"This is a very elaborate way of saying tidy up."

Partly fair, and the practical advice does reduce to something short. But the reason tidying up does not happen, even in systems explicitly designed to notice their own failures, is not that nobody thought of it. It is that the corpus's authors are structurally incapable of it, and no instruction can make them capable. That is not a restatement of "tidy up". It is the reason "tidy up" has never once worked.

The programme

One. Measure before cutting. Ask of every rule whether it has ever stopped anything. Until that exists, every specific cut is a guess with decimals on it, and your intuition about which rules are dead weight is probably wrong in a direction you will find annoying.

Two. Automatic demotion on evidence, never deletion. Rules that have not fired within a window leave the active surface and stay in version control. Restored rules ratchet into a protected segment so the loop cannot flap. Secrets, outbound and deployment classes are exempt by category.

Three. A conservation law over everything actually loaded, with no exemptions, on both size and count, so compression cannot manufacture headroom. Not per file. Not excluding linked documents. The moment scope becomes arguable, this becomes the Business Impact Target.

Four. The same law on work queues. The same arithmetic applies wherever items arrive faster than they are served. A queue whose arrival rate exceeds its service rate is not a queue, it is a landfill, and writing an item into it substitutes for handling it. Bounded slots, and admitting an item requires closing one.

Five. One corpus, generated projections. Tool-specific instruction files stop being hand-mirrored copies and become outputs of a single schema-validated source with stable identifiers.

Six. Give the gate a death certificate. If you build a control that judges whether an asset is worth keeping, look at its possible verdicts. You will probably find it can say passes, fails, and not applicable. Notice what is missing. A control that evaluates an asset once, at creation, at the moment of least information, and has no outcome that could ever retire it, is not a control loop. It is a turnstile. It is a birth certificate with no death certificate, and it will let every inherited decision ride unchallenged for as long as the system lives.

The diagnosis, I think, is solid: the arithmetic of short tenure produces monotone growth, and instruction cannot touch it. The prescription is a bet, on a mechanism whose only large-scale trial was abandoned, defended by a disanalogy that covers half the failure.

The sentence I would keep, if I could keep only one: a system that cannot forget cannot compound, it can only silt up, and the reason yours cannot forget is not negligence. It is that nobody who writes to it stays long enough to care.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.