Proof of `Fresh point-ray spans are disjoint from the nominal table spaces` (3rd 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
Every vector of the selected-ray span is a finite indexed linear combination. If it also lies in the table, all coefficients vanish by the indexed independence theorem, and so does the vector.