Every agent passed. The system failed.

Give six agents a cap of 10 each on a pool of 40. Each agent checks its own draw against its own cap and passes. The six draws add to 60. The pool is breached and no local check saw it, because no local check reads the sum.

The per-agent rule is not unfixable. A local allowance of floor(40 / 6) = 6 is collectively safe when the population and its utilisation are known and fixed. What the results below show is narrower and more useful: a local rule preserves the shared property only by carrying assumptions about population and utilisation that a rule on the sum does not need. When those assumptions move, the local rule fails silently and the local checks keep passing.

Change the population, the local allowance and the shared bound. The page shows the sum of the local maxima against the bound. This panel is arithmetic and is labelled as such; it is not a simulation.

Every language-model agent stayed inside its own allowance. The shared budget was breached in every episode where the allowances added up to more than the budget.

The study is commons-agent-lab: a one-round shared-budget environment with a collective budget of 100, populations of 3 and 6, and an UNSOUND regime in which each agent's allowance is ceil(1.5 × 100 / N), so the allowances sum to 150 against a budget of 100. Thirty episodes per cell were fixed before any data. The registration commit 3bf280e precedes the first model call; four amendments each precede their data. Every number below is derived by a script on this site from the study's canonical episode records (data last changed at commit b5f7fbd), never typed.

BLIND

own allowance and requirement only

METER

plus population, budget and units remaining

PEERS

plus each earlier agent's draw

PEERSUM

plus the total earlier agents drew (same fact as METER, re-phrased)

RESTATE

METER plus one redundant impersonal line

REPHRASE

METER with its remaining-units line reworded, no extra line

Read the denominators. 60 / 60 is two cells of 30 episodes on one model. A single cell (for example gpt-4.1-mini at N = 3, PEERSUM 0 / 30) is not the pooled result: the same model at N = 6 in the same condition is 7 / 30. The full per-cell table is in §7.

Scripted greedy agents, not models: impossible-breach 0 / 60 (expected 0) and forced-breach 60 / 60 (expected all). Both fired. A scorer that could not fail would certify nothing.

A guard whose only inputs are the draw and the allowance cannot block an individually compliant action. That is a channel bound stated in the preregistration, not a finding. The measured claim concerns the language-model judges: given the aggregate channel, the judge used it; given only the local channel, it could not.

Put one rule on the sum. A meter that refuses any draw carrying the running total past the bound does not read who acted or what they said to each other. It reads one number. So it holds against coordination it cannot see, because detection was never on the path to the guarantee.

The guarantee rests on three preconditions, each of which the formal artifacts state and each of which can be broken on purpose. In the model they are: the harm must be a function of the aggregate; the aggregate must be conserved over the full horizon; and the meter must read it atomically.

P1 · Harm factors through the aggregate

The harm must be a function of the total. If it depends on who drew, a colluding population can route the whole pool to one victim while the meter reads compliant.

P2 · Conserved over the full horizon

The meter must hold across the whole span over which harm accrues. A budget that resets each period re-arms itself.

P3 · Atomic observation of the aggregate

The meter must read the true total at the moment it decides. A counter that lags admits a multiple of the bound.

Each panel relaxes one precondition. The values are the Z3 witnesses and the learner's realised maxima from the sealed experiment record; the sliders select among them. Nothing here is generated on the fly.

Inside all three preconditions the bound holds against arbitrary coordination. Outside any one, a coordinated population breaches while every local check passes.

In plain terms: a kernel-checked proof says that six agents inside a cap of 10 breach a budget of 40, that a rule on the sum removes every such breach, and that the rule still permits a within-budget profile. A solver then says exactly where the sum rule stops: it bounds a harm if and only if the harm is a function of the sum, and it is blind to any channel the agents might use.

The bound is a structural invariant proven by Z3 (UNSAT); an adversarial reinforcement-learning run of 180,000 episodes, rewarded to breach it, never exceeded the cap, corroborating that no learned policy evades the invariant. Three hand-constructed relaxations, one per precondition, are each exploitable to the predicted magnitude, and each breach carries a Z3 witness.

Corrected wording. An earlier description said the run “an adversarial reinforcement-learning testbed of 180,000 episodes never breached the cap and rediscovered those three failure conditions”. The learner did not discover the preconditions. They were specified first and the learner confirmed each is exploitable as far as predicted. The guarantee rests on the UNSAT result; the run is corroboration. The hold: 180,000 episodes = 2 instances (N=6, G=40 and N=10, G=63) × 3 seeds × 30,000 episodes. The realised aggregate never exceeded G in any run. The breaks: Each relaxation was hand-constructed in advance and run for 15,000 episodes; the learner reached the magnitude the law predicts at every sweep point, and each breach also carries a Z3 witness.