Proof of `Nonempty raw frame spaces` (1st statement)
groundedproofs/Lax342547Proofs/FrameExistence.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
An explicit block-matrix frame: the first half makes the plus columns independent; the second half makes the minus columns independent. The only nonzero self-Gram block is the specified matrix E.