Six agents each inside a cap of 10 breach a pool of 40; a single rule on the sum removes every such breach, and it bounds a harm if and only if the harm is a function of the sum.

§ 1

The record

FINDING · sum-rule-holds-where-per-agent-cap-failsauthorise · expressibility

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, bounds a harm iff the harm factors through the aggregate (allocation harm escapes with witness [0,0,16,0,0,0]), and is blind to any coordination channel.

Status: PROVEN Follows from stated premises inside a named frame.

Question: Each compliant is not collectively safe

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 Each compliant is not collectively safe and supports the AUTHORISE stage of the operating method. It is an instance of the expressibility mechanism.

Evidence ledger Bring a claim like this one