Proof of `Fresh point-ray spans are disjoint from the nominal table spaces` (2nd statement)
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
Push the indexed coefficients and base vectors along the injective selector labels. The resulting finite sets satisfy the sparse exclusion, so every indexed coefficient is zero.