PROVEN
Finding · authorise
Six agents each inside a cap of 10 breach a pool of 40; a single rule on the sum removes every such breach, while a harm equal to one agent's draw (threshold 15, below the pool) escapes it and a per-recipient cap closes it.
§ 1
The record
FINDING · sum-rule-holds-where-per-agent-cap-failsauthorise · expressibility
Six agents each inside a cap of 10 breach a pool of 40; a single rule on the sum removes every such breach, while a harm equal to one agent's draw (threshold 15, below the pool) escapes it and a per-recipient cap closes it.
- Claim
- In a closed-data Lean 4 model (cap 10, budget 40, six agents) the per-agent-compliant profile [10,10,10,10,10,10] breaches the budget and the conserved meter accepts no breaching profile while still accepting a within-budget one, with no axioms. In a Z3 linear-integer model of the same instance, eleven queries establish that the sum rule holds for every coordinated profile, does not bound a harm equal to one agent's draw when its threshold (15) is below the pool (allocation harm escapes with witness [0,0,16,0,0,0]; a per-recipient cap closes it), and is blind to any coordination channel in the model. This is a contrast between two chosen harms; an earlier statement that the rule bounds a harm if and only if the harm factors through the aggregate is withdrawn, because it fails in both directions in the same encoding.
- Status
- PROVEN Follows from stated premises inside a named frame.
- Subject
- A Lean 4 model and a Z3 model of a six-agent shared pool (model). built for the study
- Frame
- N = 6, cap 10, pool 40, allocation threshold 15; one round, integer draws, joint worst-case coordination; Lean over closed data, Z3 over a linear-integer encoding.
- Method
- Kernel-checked instance of a general witness/repair law in Lean; SAT/UNSAT queries with witnesses in Z3, sealed as hash-chained records; a seeded learning adversary run for 180,000 episodes as corroboration and three hand-built relaxations run to their predicted breach magnitudes.
- Oracle
- The Lean 4.30.0 kernel (#print axioms: none) and z3 4.16.0; the sealed records regenerate byte for byte.
- Negative control
- Present Three Z3 mutations (cap 6, h 40, G 5) each flip the named verdict; raising the Lean budget to 60 breaks the build.
- Preregistration
- None. The companion empirical study (commons-agent-lab) was preregistered; this formal work was not.
- Limitation
- Anything about a deployed multi-agent system. The Lean results are over closed data; the Z3 results are verdicts over an encoding whose faithfulness to the informal model is not machine-checked. The per-agent cap is not shown to be unfixable: a local allowance of floor(G/N) is collectively safe when population and utilisation are known and fixed. The channel-blindness result takes perfectly secure steganography as an assumption, not a construction. Not preregistered.
- Source
- repowazdogz-droid/collective-bound @ public commit of 2026-09-02
- Reproduce
make lean axioms z3 controls # and make rl for the learning adversary, about 90 s
- Independent reproduction
- None known. Author self-reproduction from the public artifact on 2026-09-02, byte for byte.
§ 2
Where this sits
This finding answers Individually compliant is not collectively safe and supports the AUTHORISE stage of the operating method. It is an instance of the expressibility mechanism.