Proof of `Removing selected atoms leaves only unselected component labels` (1st statement)
groundedproofs/Lax342547Proofs/ResidualLabels.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
The list labels are injective, so their sum is the sum over the selected label set. The common scalar identifies each selected block with the corresponding atom. The finite intersection/difference identity deletes exactly those blocks from every component.