Lemma. The subspace-intersection inequality [cn-0024]
Status: proof-account
Statement. Let \(W\) be a real vector space of dimension \(N\), and let \(U_i,V_i\subseteq W\), \(1\leq i\leq m\), be subspaces with \(m\geq 1\) 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.\]This bound is sharp: for every \(m\geq 1\) and \(N\geq 0\), there are such families attaining equality.
Proof. Choose distinct nodes and use the constrained spaces [cn-0019]. Sum the degree budget [cn-0023] over \(0\leq h\leq m-1\). By the interpolation identity [cn-0020],
\[\begin {aligned}
\sum _{i,j}\dim (U_i\cap V_j)
&=\sum _{h=0}^{m-1}\sum _j k_h(V_j)\\
&\leq \sum _{h=0}^{m-1}\sum _{e=0}^h e\ell _e
=\sum _{e=0}^{m-1}e(m-e)\ell _e.
\end {aligned}\]The equality at the right counts how many stages \(h\) include a column introduced at degree \(e\). Since \(e(m-e)\leq \lfloor m^2/4\rfloor \), \(\ell _e\geq 0\), and
\[\sum _{e=0}^{m-1}\ell _e=k_{m-1}(W)=\dim E_{m-1}(W;t_*)\leq N,\]the claimed bound follows. Sharpness follows from the construction in cn-0025 [cn-0025], which attains equality for every \(m\) and \(N\). The paper compares the determinant-multiplicity method with subspace designs [cn-0050], but the proof here supplies its own argument for these arbitrary subspaces.
The real field matches the paper's statement. The field-of-scalars remark [cn-0065] proves that this algebraic inequality holds over every field.
A short counting proof [cn-0073] handles subspaces spanned by subsets of one common basis. The comparison with Scott and Wilmer [cn-0072] examines whether exterior-algebra methods can replace the general proof; a projection argument [cn-0074] refines \(N\) to \(\max _i(\dim U_i+\dim V_i)\).
- Proof dependencies
- Constrained spaces [cn-0019]; Interpolation identity [cn-0020]; Degree budget [cn-0023]; Sharpness construction [cn-0025]
- Provenance
- OpenAI, 23 September 2026 [cn-0042], Lemma 2.1, equation (2.1), and Remark 2.2; reconstructed as a reading account on 9 October 2026, with sharpness made explicit in the statement on 11 October 2026. Lean source for the inequality: SubspaceIntersection.