Proof of `Table coordinates and private channel complements` (4th statement)
groundedproofs/Lax342547Proofs/TableSpaces.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
Read a table vector in its two primal and two channel coordinate blocks. This map is injective. Each primal projection has dimension at most the total pin rank, and each channel block has its full coordinate dimension.