Proof of `Bit rank and Walsh bounds for global vector-slot pairings` (3rd statement)
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
A nonzero coefficient matrix has rank at least one, so the full bit form has rank at least N. The general bilinear Walsh estimate gives the required correlation bound, uniformly in the two bounded group weights.