Proof of `Exact-image bounds for independent affine columns` (3rd statement)
groundedproofs/Lax342547Proofs/AffineImages.lean · lax-342547
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
A new dependence extending an injective fixed map must have a nonzero coefficient among the random columns. Its image equals a prescribed negative old image. The affine single-image bound applies to each such relation; union over old coefficients and nonzero new coefficients.