Proof of `Majority normalization of sparse cut profiles` (1st statement)
groundedproofs/Lax342547Proofs/CutSparsity.lean · lax-342547
What this proof establishes
no assumptions
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
If every value class has size at most half the tags, each tag has at least half the tags as unequal partners. Counting ordered pairs then contradicts the assumed upper bound on nonzero unordered cuts.