Proof of `Bounds for partition energy`
groundedproofs/Lax18Proofs/PartitionEnergyBounds.lean · lax-18
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
The density between two finite vertex sets lies in the unit interval. Hence each energy summand is nonnegative and at most its pair weight. Disjointness of the partition classes bounds the total pair weight by one.