Proof of `Fresh key directions are independent modulo 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
Absorb each scalar coefficient into the base evaluation vector and apply the uniform sparse-label exclusion. Its constant coordinate is exactly that scalar, so a nonzero coefficient would force a forbidden label.