Proof of `Dimension and component-rank bounds for effective test spaces` (1st statement)
groundedproofs/Lax342547Proofs/EffectiveBounds.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
Embed the effective space into the product of its component tensor spaces. Their dimensions sum to at most the product of the total projected plus and minus dimensions. Each total is bounded by K. Component matrix ranks are bounded by the plus projection dimensions, whose sum is at most K.