Proof of `Two-sided Gram normalization for individually injective frames` (3rd statement)
groundedproofs/Lax342547Proofs/GramNormalization.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
One extra ambient dimension beyond p+q makes both failure bounds at most one half. Hence every individually injective Gram orbit has independent column probability at least 2^(-pq-2), the explicit density denominator used for bounded channel frames.