Proof of `Counting tuples of symmetric matrices with bounded total rank` (2nd statement)
groundedproofs/Lax342547Proofs/ProfileCounting.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
Partition profiles by their component ranks. Each rank is at most K. For a fixed rank tuple, the checked symmetric factorization count gives at most 2^(d sum(r_e)+sum(r_e²)), bounded by 2^(dK+K²).