Proof of `A uniform label budget for all sparse pin vectors`
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
Choose independent sparse vectors spanning all sparse members of each projected space, and collect their labels. Interpolation makes every comparison with another sparse expansion unique, so that expansion has no additional nonzero labels. The union over signs and components has the required size.