collective-bound

That six agents each inside a cap of 10 breach a pool of 40 while a rule on the sum removes every such breach (Lean, closed data, no axioms); that the sum rule holds for every coordinated profile and bounds a harm iff the harm factors through the aggregate, and is channel-blind (Z3); and that a learning adversary with full sight of the meter never exceeded the bound over 180,000 episodes while each hand-built relaxation was exploitable to the predicted magnitude.

Anything about a deployed multi-agent system. Lean over closed data only; Z3 encoding faithfulness argued, not proved; the per-agent cap is not shown to be unfixable; the channel-blindness result assumes perfectly secure steganography rather than constructing it. Not preregistered.

Two Lean files extracted unmodified from a larger private development; five Python files and six sealed records extracted unmodified from a private Z3 development; runners that write only under out/; three Z3 mutation controls and one Lean mutation control.

lake build succeeds; #print axioms reports no axioms for all six theorems; records 0001 to 0003 and exp-0003 regenerate byte for byte (hashes 3fd7b869…, 95a0989f…, 34142856…, 23f5d078…); all four negative controls fail as required.

The Lean 4.30.0 kernel and toolchain; z3 4.16.0 and the faithfulness of the linear-integer encoding; the vendored omega_seal hashing (stdlib only); seeded numpy for the learning run.

Aggregate and conservation caps as a design pattern; Motwani et al., Secret Collusion among AI Agents (NeurIPS 2024), whose undetectable-collusion setting is the adversary in the channel-blindness result, built on the perfect-security construction of Schroeder de Witt et al. (ICLR 2023). The contribution is the machine-checked interaction between the sum rule and undetectable coordination, and the exact boundary.

make lean axioms z3 controls

Findings drawn from this artifact are on the evidence ledger.