Proof of `Fresh point-ray spans are disjoint from the nominal table spaces` (1st 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
The existing sparse-label exclusion works for all sets of size at most R+14, so it also works for the fourteen selected rays at each endpoint.