Who Pays to Keep It True?

Take the Ashdown instruction, the invented intake matter that recurs through this book, and give the firm a library of encoded rules: a limitation rule, a building-claims rule, a privilege rule and a filing date. Nobody has been told that the rules are their job.

The building-claims rule is invented, but a real one shows what happens to it. On 28/06/2022 the Building Safety Act 2022 inserted section 4B into the Limitation Act 1980, for England and Wales. Under it, an action under section 1 of the Defective Premises Act 1972 that accrued before commencement is read "as if the reference in subsection (1) to 15 years were a reference to 30 years" (Building Safety Act 2022, s 135). An encoding of the old period for those claims went false that day, and section 135(3) treats the amendment as always having been in force, so in law it counts as never true, save for claims already settled or finally decided (s 135(6)). Its proofs still compiled.

Mathlib is the right precedent for how to keep a formal library and the wrong one for who pays. Three claims follow. First, law's library has a cost that mathematics' does not: an outsider holds the clock, so abandoning it produces false answers and not merely old ones, and a grant that ends cannot cure a rate. Second, and most contestable: selling the library is a safe funding rule only until the library matters. The instrument this book proposes, a presumption attached to a published predicate, is, on my reading of the EU Court of Justice's reasoning, the feature that exposes such a text to compulsory disclosure. Such texts are still on sale, so this is a claim about what a budget can rest on. Third, where the state does not pay from general taxation, the working precedent is neither philanthropy nor subscription. It is a compulsory charge at a point the users cannot avoid. A presumption has such a point only for those who claim it, so the charge falls on them and its yield has to be tested. So price the reliance and leave the reading free.

I build verified AI systems for law firms. A shared corpus would lower my costs and my rivals' alike, shrink what my proprietary formalisation layer can charge for, and put a fee on my customers. I have not worked out which of those wins. Nothing here is legal advice, and each legal statement below is marked by jurisdiction.

I owe three corrections. In How High Can You Build in Mud? I called drift maintenance "the cost nobody budgets for and everybody pays". The National Archives has long paid an in-house team for exactly that, as below. In LegalLean I called an open verification layer over a proprietary formalisation layer "the same model that underlies much of the formal verification ecosystem". That answers who may inspect, not who keeps the work current. In Mathematics Went First I said to budget for maintainers "as the Lean community has through the Mathlib Initiative". A programme funded by donations is not a budget line.

What Mathlib actually is

Mathlib has "over 2 million lines of formally verified mathematics, written by over 750 contributors" (Mathlib Initiative roadmap, October 2026 to March 2027). Final approval of changes rests with maintainers, who join "at the invitation of the current maintainers" for "a renewable two-year term" (Mathlib maintainers page). Authority comes from peer selection, and that is the part to copy.

The Initiative says Mathlib's "natural growth rate is beyond what can be achieved through purely voluntary support" (About). It is "a program of Renaissance Philanthropy", with "an extremely generous founding donation from Alex Gerko, Founder and CEO of XTX Markets" and a Sloan Foundation donation. Its team page lists nine employees and ten contractors. Of the 28 maintainers listed on 02/11/2026, by my count of their published biographies, five name an Initiative role, three the Lean FRO [the non-profit that builds Lean], two an AI company, and eighteen a university or research institute. The FRO lists Gerko among its funders too. I allege no misuse, but the shared layer rests on a few donors' continuing decisions, and the Initiative says Mathlib's maintainer, reviewer and moderator structures "were not designed for the scale the community is now reaching".

"Review capacity remains the principal constraint on how fast Mathlib can grow." Measurement showed "both that our review throughput increased over the year and that the open-PR queue nevertheless continued to grow". The target of a response within a week for 90% of review rounds "was not achieved". And "many now consume Mathlib without contributing to it". That is a funded team reporting free riders and a growing queue from inside a very successful formal library.

The Archive of Formal Proofs, for Isabelle, is the older precedent, and it has half of this chapter's check. An accepted author "must agree to maintain your archive entry or nominate someone else", because the Isabelle team "does not have the resources to fully maintain the complete archive" (AFP submission page). In what I read, neither library sets an expiry on an entry, and neither needs one.

Who holds the clock

Mathlib's maintenance is real: "code written for one version of Mathlib may no longer compile with a newer version" (Baanen et al., 2025). But the maintainers choose those changes, the build reports them, and a project pinned to an old commit still has its theorems. Nobody can legislate a false theorem into being. A formalisation can misstate the mathematics, and that is found, not imposed.

Law's clock belongs to someone else. legislation.gov.uk lists 154 recorded changes affecting the Limitation Act 1980, from instruments of 1994 to 2026. The count is lumpy: 19 from instruments of 2018, 18 from 2024, 2 from 2022. Volume is no proxy for importance, since one of those two from 2022 is the section 4B change, and 16 of the 154 are commencement orders. Somebody must read them to find out which ones change an answer.

The proofs are as trivial as those in Nobody Is Paid to Delete; the content is in the definitions. Treat the stale stock as a queue, with arrive changes per tick and review capacity per tick. backlog_linear proves that when arrivals are at least capacity the stock is the starting stock plus t times the gap. backlog_clears proves that otherwise it falls by the margin until it reaches zero. Start from zero, set capacity to zero and walk away. walkaway_internal_clock gives zero stale entries at every tick, because a library nobody else can falsify has no arrivals. walkaway_external_clock gives t × a. The two differ in one assumption, a = 0. The model does not count Mathlib's compile drift, which the build reports; the stock here is a false entry that still builds.

The queue has already run in public. In 2012 The National Archives said its editors apply "up to 10,000 complex legislative changes" a year, while the UK's legislatures "may make 15,000 new effects", and that "around half of the laws currently visible on the site are not fully up-to-date" (The National Archives, 2012). Read as parameters and not as a measurement, those give tna_2012_shape: 5,000 more each year. Its help pages now say "All Acts on Legislation.gov.uk are kept up to date", as is secondary legislation from 2018, with older instruments still in progress at June 2026 (legislation.gov.uk help). It reports 153,004 amendments applied in 2024-25 against 107,094 the year before, a period including EU Exit work (Annual Report 2024-25). I draw no ratio across thirteen years of possibly different counting. But the state has largely delivered, for Acts and recent instruments, what it said in 2012 had for decades been "beyond reach". Regulation here produced a capability: an official, free record of what the law says.

A grant buys a level

Open source shows who pays when nobody must. OpenSSL's foundation "typically receives about US$2000 a year in outright donations", its fundraiser wrote in April 2014 (Marquess, 2014). One figure is not an estimate, but Nadia Eghbal's general point stands: people assume others are reviewing "when in reality nobody is taking responsibility" (Eghbal, 2016). Hoffmann, Nagle and Zhou put demand-side value at $8.8 trillion, on a replacement-cost counterfactual and not as a measured output (Hoffmann et al., 2024). Use appears to outrun what maintainers receive.

A grant that ends does not close that gap, for a reason that is arithmetic. Let capacity m run for g ticks and stop. grant_rate_after proves the stock then rises by a every tick. grant_is_level_not_rate proves that, for every later tick, the no-grant stock exceeds the grant stock by the same amount. The grant moved a level, once. Build cost is a level too, so philanthropy suits a first build, and suits an annual flow only while the donor renews. An endowment whose return pays the flow is outside this model: it is a flow, and it needs capital of the annual cost divided by the return. Nothing here compounds: the costs below are flows, constant by assumption.

What the cost model says, with no numbers in it

These are assumptions, and I hold no value for any of them.

The counterfactual is not zero. It is today: firms and publishers each doing this privately, at a cost nobody publishes. shared_cheaper_iff gives the exact condition, when integration costs no more than doing it alone: sharing wins when sharedTotal < n × (perFirmPrivate - integrate). no_scale_rescues proves that if integrating costs a firm at least as much as doing it alone, no number of firms helps. scale_suffices proves that any strict gap is enough at sharedTotal + 1 firms. So integration cost decides this, and law's open texture lives there. If each firm must re-read every predicate because it will not rely on another's reading, integration approaches the private cost and the corpus is a waste of money. That is how this chapter can fail.

Review has a second trade-off. Reviewing each fact every h ticks costs reviewLoad / h per tick, and an amendment can then sit unnoticed for up to h, costing lossRate × h. horizon_floor proves a whole-number form of the floor, for all values: 4 × reviewLoad × lossRate × h² ≤ (reviewLoad + lossRate × h²)². Over the reals, not formalised here, that gives a cost per tick of at least 2√(reviewLoad × lossRate), at h = √(reviewLoad / lossRate), the algebra of Harris's economic order quantity (Harris, reprinted 1990; bibliographic record checked). A sketch, not a proof: if n firms share one corpus, the review load stays the same and the loss rate becomes n times larger, so the best horizon shortens by √n and each firm's share of the floor falls by √n. A shared corpus should be reviewed more often than any firm would review its own. That is a level effect for a given n, not a productivity claim. The falsifying measurement is the pilot's integration cost, and the main benefit, fewer wrong answers, appears in no statistic anyone collects.

Nobody alone, or one patron

Why not a voluntary consortium? On toy values, worth_it_but_nobody_alone computes three firms whose joint benefit exceeds the cost while no firm would pay it alone, and one_patron_alone computes a group with one large firm, which alone would fund it. Harvard University Press's description of Mancur Olson's The Logic of Collective Action (1965) calls the patron case "a surprising tendency for the “lesser” members of the small group to exploit the “greater” members" (publisher's description). Where all must agree and values are private and independent, George Mailath and Andrew Postlewaite prove that "as the number of agents increases, the probability of an affirmative efficient decision goes to zero" (Mailath and Postlewaite, 1990, abstract). A charge set by a public body removes the premise that all must agree, though not the need for enough firms to claim.

All of this is standard, and I claim no novelty in law and economics. Louis Kaplow already says "Rules typically are more costly than standards to create" (Kaplow, 1992, abstract), after Ehrlich and Posner (1974, bibliographic record only). I add a flow term, the cost of staying true after creation, and an allocation of it.

Selling is safe until it matters

The market's answer is a publisher, and for private reading of the law it works. RELX reported £1,806m of 2025 revenue in its Legal segment, which covers far more than keeping texts current (RELX 2025 overview).

My second claim concerns what happens when a text gains force. In Public.Resource.Org v Commission (EU law, Grand Chamber, 05/03/2024), the standards at issue came from private bodies which, as a case note puts it, "rely on their sales to finance their standardisation activities" (Kanevskaia, 2025). The Court reasoned from the effect of a presumption of conformity (para 76), held that "the requested harmonised standards form part of EU law" (para 80), said the rule of law "requires free access to EU law" (para 81), and found an overriding public interest in disclosure (para 85) (C-588/21 P). The case concerns access to documents held by the Commission, the Court did not reach the ground about intellectual property (para 87), and it does not mention software predicates.

In the United States, Georgia v Public.Resource.Org (2020) reached annotations that Lexis drafted under a contract giving it "the exclusive right to publish, distribute, and sell" the code. The majority: "no one can own the law", and non-binding works by officials with authority to make law are not copyrightable. The rule does not reach private parties who lack that authority (590 U.S. ___). For the UK and Australia I have read no decision on point, and I make no claim.

Now read Make the Safe Harbour Compile against that. I proposed a published predicate that gives a firm a presumption of compliance. If an EU instrument attached a presumption to it, paras 76 to 81 are a short walk to free access. That is my inference; no court has ruled on a predicate. A vendor's private encoding with no legal effect stays saleable. So the better the shared corpus works as law, the less a funding rule can rest on selling it. That essay needed a funding rule and did not have one.

The precedent: charge at the chokepoint

The lighthouse is the textbook public good, and Ronald Coase's reply is the textbook surprise. Samuelson wrote, as Coase quotes him, that a businessman "cannot claim a price from each user". Coase found British lights paid for by light dues from shipowners, collected at the ports, and concluded that "economists should not use the lighthouse as an example of a service which could only be provided by the government" (Coase, 1974). David Van Zandt's reply disputes how private that was; I know it only from its bibliographic record and secondary summaries, which report Crown enforcement as essential. If they are right, it helps me: the money was never voluntary. In UK law today, general light dues are "payable in respect of all ships whatever", with listed exemptions (Merchant Shipping Act 1995, s 205). A ship cannot be charged for seeing the light, but it can be charged at the port.

CanLII, launched in 2001, is "funded by Canada's 14 law societies" and owned by their Federation (CanLII, 2025). In British Columbia the 2027 practice fee carries a CanLII line of $61 (Canadian) per lawyer, towards the society's portion of $962,000 (Law Society of BC, 2026), and lawyers in Canada must by law belong to a law society (Federation of Law Societies). Reading is free. This is the closest I found to my proposal, with a limit: CanLII publishes law and encodes nothing, so its burden tells us little about predicates.

BAILII, which publishes British and Irish primary materials free, is the strongest case for philanthropy. It is a registered charity, took government contract income in 2021 and 2022, and spent more than its income in each of the five years to 31/12/2025, £203,105 against £197,651 in the last (Charity Commission, no 1084803). It still runs, which counts against me. But its stated activity is giving access to law, not encoding it. I read its register entry, not its site or donor list.

The 2012 programme announced "trained editors from the private and voluntary sectors", with Practical Law among those employing them, "without any additional cost to the taxpayer", while The National Archives "retains ultimate responsibility for the accuracy of the content". Anyone may re-use the data "to create their own commercial products and services". Private employers were to pay for public capacity under public review. I found no evaluation of what that produced.

So this is the allocation I argue for, with each row a proposal:

Perfect Compliance, Defeated Purpose proved in same_test_sunset_is_a_fee that when re-earning costs both routes the same it changes no ranking: it is a fee. Fine. Fees are what this needs. A renewal at each sunset, charged to the claimant, is the flow matched to the flow.

A corpus makes it cheaper to learn what a rule requires. It should not make the rule require less, and a fee must not buy a lighter test.

Who gains? benefit_levy_whole proves that a levy proportional to true benefit leaves every firm no worse off whenever the group benefit covers the cost. But benefit is private, and headcount_levy_can_hurt computes a firm with many people and little use for the corpus left worse off. Charging at the claim of a presumption avoids much of that, since a firm that does not claim does not pay. That is also where the port analogy stops. Every Canadian lawyer must belong to a law society, but a firm can read a predicate, comply and never claim. Nor does anything yet require a filing: the AI Act attaches its presumption to conformity (Article 40(1), EU), so a statute must make filing a condition. Revenue is the fee times the claimants, and it need not reach sharedTotal. If it falls short, the state pays the difference or the corpus covers less, and I would cut coverage before raising the fee. I expect the fee also to favour large firms, for whom it is small. That reopens the entrenchment the Safe Harbour essay raised and answered by saying a small firm could "run for nothing" a published predicate: it still can, but claiming now costs. So bands or a public subsidy for the smallest are part of the design, and cheaper compliance is not self-evidently a public good. Vendors who resell the corpus pay nothing unless they claim. Free reading requires that, and I have no fix.

Governance, because a levy without it is capture with a statute. The boring work goes to employed editors at the corpus body, with named duties; volunteers are welcome and no duty rests on them. Merge authority over drafts comes by peer invitation, as at Mathlib. Legal force does not: a predicate carries a presumption only when a public authority cites it, as a harmonised standard does on citation in the Official Journal. Peers choose who edits; an accountable body chooses what binds. No payer gets a seat by paying, and a cap, a parameter I do not set, limits any one employer's share of merge rights. A public body collects the fee. Queue statistics are public. Retiring a predicate is paid work with its own credit, because of what Nobody Is Paid to Delete showed. All of this is proposed; none has run.

The check, and what it does not check

The block below is copied from lean/BuildingInSteel/Maintenance.lean, which compiles on Lean v4.29.1 with only the book's case file.

def Fact.sound (h now : Nat) (f : Fact) : Bool :=
  (match f.owner with | some p => isHuman p | none => false) &&
  (match f.expiresAt with
   | some e => decide (now < e) && decide (e ≤ now + h)
   | none => false)

corpusOK_iff proves, for every horizon, tick and corpus, that the check means what that says. By definition an agent cannot be an owner: it ends with its session. ashdown_defects computes, on the case at tick 5, three defects of three kinds: the limitation rule has no owner, the building rule has no expiry, the privilege rule is owned by the drafting agent.

Expiry changes how the corpus fails. walkaway_goes_dark proves that if the check passed at now, then with no further review every fact has stopped answering at now + h. Unfunded, it goes dark, where a corpus with no such gate goes on answering. wrong_ticks_le_horizon proves that a fact passing at now, amended at any later tick, is served wrongly on at most h ticks, for that one record. The count starts at the amendment, so it misses what section 135(3) does: a retrospective change makes earlier answers wrong as well, and no expiry reaches those. This is the lease of Yesterday's Permission, applied to facts. It has the same cost: dark means a true rule refused, perhaps with a limitation date running, which Never Breaks a Rule, Never Finishes treats as a harm of its own. So dark must page a human.

renewal_floor proves that with at most m reviews per tick, having n distinct facts all reviewed inside a window of h ticks needs n ≤ h × m, even if no law ever changes.

For a developer: pin each encoded rule to its legislation.gov.uk provision, poll the effects feed (the changes pages offer one, and the API documents them), expire a rule when an effect lands on its pin, and fail CI on defects. The feed lags: its preparatory processes "typically take from four to eight weeks". For a partner: ask who owns the limitation rule in your tools, and when it expires. A person and a date is the answer.

Goodhart, and what formalising loses

The check will be gamed once it is a target. Everything gets one owner: overloaded_passes_check_fails_capacity computes a partner holding four facts with a capacity of one a tick and a window of two, passing corpusOK and failing capacityOK. Owners will renew without reading, and each renewal is a new record with a fresh window, so the bound above does not survive a rubber stamp. check_blind_to_truth computes the plain case: a corpus that passes at tick 9 while one of its facts went false at tick 8. A renewal dated after an effect on its own pin can be voided by machine, and sampling renewals against seeded changes, as in The Last Person Who Knows How, catches some of the rest. A body with a target of zero backlog will be tempted to drop the hard rules, the scope exclusion from Nobody Is Paid to Delete, so publish coverage beside backlog.

Formalising loses something too. Today currency sits in many heads, redundantly and unevenly. A named owner may let everyone else stop looking. And a model in which staleness has a price invites asking whether a wrong answer is worth fixing, which a client or a citizen may not want asked.

What exists and what does not

Proved generally in lean/BuildingInSteel/Maintenance.lean (no sorry, no declared axioms; #print axioms lists at most propext, Quot.sound and Classical.choice): backlog_linear, backlog_clears, tna_2012_shape (general in t, on those two parameters), walkaway_internal_clock, walkaway_external_clock, grant_rate_after, grant_is_level_not_rate, shared_cheaper_iff, no_scale_rescues, scale_suffices, horizon_floor, benefit_levy_whole, corpusOK_iff, walkaway_goes_dark, wrong_ticks_le_horizon, renewal_floor.

Computed on toy values or the case: worth_it_but_nobody_alone, one_patron_alone, headcount_levy_can_hurt, ashdown_defects, ashdown_repaired_passes, check_blind_to_truth, overloaded_passes_check_fails_capacity.

Sketched, not proved: the real-valued floor and best horizon, and the √n result. Assumed: every parameter, with constant flows. Judgment, in no theorem: which changes matter, whether a predicate reads a rule correctly, and the allocation table.

Exists: Mathlib's and the AFP's maintenance, legislation.gov.uk's editing and feed, CanLII's levy, light dues. Does not exist, as far as I have read: a shared formal corpus of statute law with a funded maintenance line, or any predicate with a statutory presumption. Catala, covered in The Translator Writes the Rule, and OpenFisca, whose association lists "membership fees; donations; voluntary work; public subsidies" among its resources (Statutes, art 9), are the nearest working systems.

Objections

"Generation is cheap now. Re-encode on every amendment and the cost goes away." The strongest objection, from this book's own premise. It lowers the cost of drafting a change and leaves the cost of checking one. The Initiative's roadmap says AI tools "significantly lowered the cost of producing Lean formalizations", that the kernel "can not check a formalization's semantic alignment", and that review remains the constraint. Verdict: review demand may rise. I would change my mind on a measured pilot, audited by someone other than the vendor, in which review capacity outran arrivals with error rates held.

"Publishers already do this, and free law kills the cheap version." Half right. Justice Thomas warned in dissent in Georgia that perhaps "many States will stop producing annotated codes altogether", citing Georgia's assertion that Lexis sold its code for $404 against West's $2,570. Poorer readers may lose. Verdict: publishers keep the private layer. The presumption layer is where a budget cannot rest on selling, and it needs a fee because that subsidy would go. I would concede if a publisher opened its encodings to public audit and let them carry a presumption without charging to read them.

"Harmonised standards are still on sale. Your second claim has already failed." EN 18286:2026, the first harmonised standard under the AI Act, was cited in the Official Journal in October 2026, which gives a presumption of conformity (CEN-CENELEC, 2026), and DIN Media sells the German edition from 149.80 euros including VAT (DIN Media). CEN-CENELEC says the judgment "does not call into question that Harmonized Standards are subject to copyright protection" (CEN-CENELEC, 2024), though the Court left that ground unexamined (para 87). Verdict: the sale survived the ruling, and the right to refuse disclosure did not, at least for the four standards requested. A budget resting on those sales rests on an open question. I would withdraw the claim if an EU court upheld that copyright against a disclosure request for a presumption-bearing text.

"One corpus is one reading. You are funding a monoculture." The Translator Writes the Rule exhibits two defensible translations of one sentence that differ. An official predicate picks one. Verdict: real, and limited by design: the presumption stays rebuttable, the corpus covers only closed-texture tests, and forks stay free. I would withdraw the proposal on evidence that tribunals treat a presumption predicate as conclusive.

"This is public work. Tax it, and stop pretending a fee is neutral." I partly agree: the text layer is public capacity, the state built it well, and calling that a cost misses what it produces. For predicates I keep the fee, since those who benefit most can be identified at filing and general taxation would subsidise them. Verdict: fee, under public governance. I would switch if fee-payers captured the rule-setting, shown by predicates moving towards large claimants' practice, or if the fee kept small firms out.

Predictions

1. By 31/12/2028, no formal library of statute law in any jurisdiction will publish a recurring maintenance budget covering more than one legal domain, funded by anything other than grants, one employer or one government department's project money. Refuted by one such library with a published budget and named editors.
2. Mathlib's open pull requests on GitHub will number more at 31/12/2027 than at 01/10/2026, though more are closed in 2027 than in 2026. Refuted if they number fewer, which would weaken my claim that cheap generation raises arrivals faster than review capacity. Untested if closures fall.
3. Any formal encoding of a rule given a presumption of conformity by an EU instrument by 31/12/2030 will be free to read, at least on request under Regulation 1049/2001. Refuted by a refusal standing at that date, which would break my second claim. A seller's price does not refute it: EN 18286:2026 has one. If none is given one by then, the prediction is untested, not confirmed.

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.