Lemma. A short proof when the subspaces share a coordinate basis [cn-0073]

    Status:

    Statement. Let \(m\geq 1\) and let \(e_1,\ldots ,e_N\) be a basis of a finite-dimensional vector space \(W\) over any field. Suppose each \(U_i\) and \(V_i\), \(1\leq i\leq m\), is spanned by a subset of this same basis, and \(U_i\cap V_i=0\). Then

    \[\sum _{i,j=1}^{m}\dim (U_i\cap V_j)\leq \left \lfloor \frac {m^2}{4}\right \rfloor N.\]

    Proof. For each basis index \(k\), let \(a_k\) be the number of spaces \(U_i\) containing \(e_k\), and \(b_k\) the number of spaces \(V_i\) containing \(e_k\). The two sets of indices are disjoint, since no designated pair contains a common basis vector. Hence \(a_k+b_k\leq m\), so \(a_kb_k\leq \lfloor m^2/4\rfloor \).

    The intersection of two spaces spanned by subsets of one basis is spanned by their common basis vectors. Count the contribution of each \(e_k\) to the sum: it occurs in exactly \(a_kb_k\) ordered intersections. Therefore

    \[\sum _{i,j=1}^{m}\dim (U_i\cap V_j)=\sum _{k=1}^{N}a_kb_k\leq \left \lfloor \frac {m^2}{4}\right \rfloor N.\]

    This explains the balanced product in the general bound [cn-0024] and its equality construction [cn-0025]. Arbitrary subspace families need not admit one basis of this kind; the exterior-algebra comparison [cn-0072] explains why taking leading coordinates does not remove that restriction.

    Proof dependencies
    None.
    Provenance
    Elementary special case of OpenAI [cn-0042], Lemma 2.1, written on 12 October 2026 as a warm-up for the comparison with Scott and Wilmer [cn-0072]. The counting argument is supplied here.