Proof of `Cancellation on a small set of distinct balanced-predicate inputs` (1st statement)
groundedproofs/Lax253009Proofs/BalancedCancellation.lean · lax-253009
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Multiply the balanced zero-sum identity by a bounded function supported on S. All outside coordinates have the same mean by a transposition; the inside sum is at most |S| in absolute value.