Proof of `Bounded table data and linear-size nominal coefficient records` (3rd statement)
groundedproofs/Lax342547Proofs/TableCounts.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
Each bilinear form is determined by a matrix with one entry per pair of basis vectors. Both table domains have dimension at most 2K+2h. Multiply the binary matrix counts over both cross orientations and all components.