Let \(W\) be a real vector space of dimension \(N\). Here \(W\) is the ambient space of polynomial values. Choose a basis \(e_1,\ldots ,e_N\). A univariate polynomial map \(P:\mathbb R\to W\) has one scalar polynomial for each coordinate of its value:

This definition is independent of the chosen basis: a change of coordinates takes real linear combinations of the scalar polynomials \(p_j\). For example, \(P(t)=(1+2t,3-t^2)\) is a polynomial map from \(\mathbb R\) to \(\mathbb R^2\). Its two coordinates are two scalar polynomial functions of the same variable.

Writing \(p_j(\xi )=\sum _{r=0}^{h}c_{jr}\xi ^r\) and collecting equal powers expresses the map in terms of its vector coefficients \(w_r\):

The paper's notation \(W[\xi ]\) encodes these maps by their coefficient expansions. For a subspace \(Z\subseteq W\), \(Z[\xi ]\) consists of the maps with every \(w_r\in Z\), so their values also lie in \(Z\). For \(P\ne 0\), its degree is the largest \(r\) with \(w_r\ne 0\); the zero map is included in every degree bound.

For degree at most \(h\), the coefficient tuple \((w_0,\ldots ,w_h)\) belongs to \(W^{h+1}\). Slot \(r\) corresponds to monomial \(\xi ^r\). Thus \(W[\xi ]_{\leq h}\cong W^{h+1}\). The polynomial coefficient matrix \(C=(c_{jr})\) has \(N\) rows, one for each coordinate function \(p_j\), and \(h+1\) columns, one for each monomial \(1,\xi ,\ldots ,\xi ^h\).

The distinction is between the coordinate index \(j\) of a value in \(W\) and the degree index \(r\) within each scalar polynomial \(p_j\). The monomial correspondence is with \(r\); the dimension \(N\) of the value space and the polynomial degree bound \(h\) are independent.

For example, with \(W=\mathbb R^2\),

Its coefficient matrix has columns corresponding, in order, to \(1,\xi ,\xi ^2\):

This is a degree-two polynomial map \(\mathbb R\to \mathbb R^2\); for instance \(P(1)=(3,2)\).

In the rank-sum application [cn-0027], \(W=\mathbb R^d\oplus \mathbb R^d\). A polynomial map has the form \(P(t)=(a(t),b(t))\), where \(a,b\) are \(\mathbb R^d\)-valued polynomial maps. Requiring \(P(t_i)\) to lie in the graph [cn-0026] of \(X_i\) means \(b(t_i)=X_i a(t_i)\). This explains why evaluation in the subspace argument must produce a vector in \(W\).

These auxiliary maps serve the interpolation proof; they do not approximate drawing arcs. The same definition works over any infinite field by replacing \(\mathbb R\) throughout. Infinitude ensures that a scalar polynomial is determined by its values, so degree and coefficients are well-defined for the map. See the field-of-scalars remark [cn-0065] for the algebraic inequality over arbitrary fields.

Proof dependencies

None.

Provenance

Notation used in OpenAI, 23 September 2026 [cn-0042], proof of Lemma 2.1; explanatory definition added on 9 October 2026.

Choose distinct real numbers \(t_1,\ldots ,t_m\) at which polynomials will be evaluated. These chosen evaluation points are called interpolation nodes, or simply nodes. A non-node is a real number \(t\notin \{t_1,\ldots ,t_m\}\).

In the constrained polynomial spaces [cn-0019], the conditions \(P(t_i)\in U_i\) are imposed at these points, so they are also called constraint nodes. They are auxiliary scalars: any distinct choices work, for example \(t_i=i\). With three nodes \(1,2,3\), the conditions concern \(P(1),P(2),P(3)\), while \(t=0\) is a non-node.

Proof dependencies

None.

Provenance

Terminology used in OpenAI, 23 September 2026 [cn-0042], Sections 2 and 4; explanatory definition added on 9 October 2026.

Let \(W\) be a finite-dimensional real vector space, the ambient space of polynomial values, and let \(U_1,\ldots ,U_m\subseteq W\) be subspaces. Choose distinct real interpolation nodes [cn-0063] \(t_1,\ldots ,t_m\), at which we impose conditions on those vector values. For a subspace \(Z\subseteq W\), write \(Z[\xi ]\) for the univariate polynomial maps [cn-0064] with coefficients in \(Z\): \(P(\xi )=\sum _{r=0}^{h}z_r\xi ^r\) with each \(z_r\in Z\).

The constrained polynomial space, for \(h\geq 0\), is

Each constraint means \(\sum _{r=0}^{h}t_i^r z_r\in U_i\). This sum already belongs to \(Z\), so the permitted value lies in \(U_i\cap Z\). The coefficients form a tuple in \(Z^{h+1}\), and these are linear conditions on that tuple.

Its evaluation space and dimension increment are

For a fixed \(t_*\notin \{t_1,\ldots ,t_m\}\), called a non-node [cn-0063], the spaces \(E_h(W;t_*)\) are nested. After identifying their dimensions [cn-0020], write \(\ell _h=k_h(W)-k_{h-1}(W)\) for the evaluation-filtration increment. Nonnegativity of these increments is a consequence of nesting.

Lean uses a strict degree bound: its space indexed by \(h+1\) corresponds to the paper's \(\mathcal P_h\). The Lean guide [cn-0038] records this shift.

Proof dependencies

Univariate polynomial maps [cn-0064]; Interpolation nodes [cn-0063]

Provenance

OpenAI, 23 September 2026 [cn-0042], proof of Lemma 2.1; reconstructed as a reading account on 9 October 2026. Lean source: PolynomialFiltration.

Status: proof-account

Statement. For the constrained polynomial spaces [cn-0019], evaluation at a non-node \(t\) has kernel \((\xi -t)\mathcal P_{h-1}(Z)\), and hence

Evaluation at the \(m\) constraint nodes identifies \(\mathcal P_{m-1}(Z)\) with \(\bigoplus _i(U_i\cap Z)\). Consequently

Proof. A polynomial map vanishing at \(t\) is divisible by \(\xi -t\), coordinate by coordinate in \(Z\). At each constraint node, division rescales its value by the nonzero scalar \((t_i-t)^{-1}\), so membership in \(U_i\) is preserved. Multiplication proves the reverse inclusion. Rank-nullity yields the first identity.

For values \(z_i\in U_i\cap Z\), the Lagrange interpolant

belongs to \(\mathcal P_{m-1}(Z)\) and has those values. Uniqueness follows because a scalar polynomial of degree at most \(m-1\) with \(m\) distinct roots is zero, applied to each coordinate. Taking dimensions and telescoping the increments proves the second identity.

Proof dependencies

Polynomial spaces and increments [cn-0019]

Provenance

OpenAI, 23 September 2026 [cn-0042], equations (2.2)–(2.3); reconstructed as a reading account on 9 October 2026. Lean source: Interpolation.

Status: proof-account

Statement. Let \(A(\xi )\) be an \(r\times r\) real polynomial matrix. If \(\operatorname {rank}A(t)\leq r-q\), then \((\xi -t)^q\) divides \(\det A(\xi )\). If distinct nodes \(t_j\) have deficiencies at least \(q_j\) and the determinant is nonzero, then

Proof. Choose \(q\) independent vectors in the kernel of \(A(t)\) and extend them to a basis. Right multiplication by this constant change-of-basis matrix makes \(q\) columns vanish at \(t\). Every entry of those columns is divisible by \(\xi -t\), so multilinearity gives a factor \((\xi -t)^q\) in the determinant. The change of basis only multiplies the determinant by a nonzero constant.

For distinct nodes these powers are relatively prime, so their product divides the determinant. Comparing degrees proves the inequality. The zero-size case uses the empty determinant \(1\). This is the multiplicity step that turns nodewise rank loss into a global degree bound.

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], determinant-divisibility step in Lemma 2.1; reconstructed as a reading account on 9 October 2026. Lean source: RankMultiplicity.

Status: proof-account

Statement. In the polynomial setup [cn-0019], suppose \(U_j\cap V_j=0\). Then

Proof. Let \(\pi _j:W\to W/V_j\) be the quotient map. For any non-node \(t\), its kernel on \(E_h(W;t)\) contains \(E_h(V_j;t)\). The evaluation identity [cn-0020] gives

Choose a fixed basis of \(\mathcal P_h(W)\), evaluate it at the variable \(\xi \), and project by \(\pi _j\). This is a polynomial matrix. Every minor exceeding the displayed rank bound vanishes at all non-nodes, an infinite set, and is therefore the zero polynomial. The same rank bound holds at \(t_j\). Finally \(E_h(W;t_j)\subseteq U_j\), and \(\pi _j\) is injective on \(U_j\) by disjointness. Thus projection does not reduce its dimension there.

The proof uses vanishing polynomial minors to specialize the rank bound. It does not assume that a generic basis stays independent at a constraint node.

Proof dependencies

Polynomial setup [cn-0019]; Evaluation identity [cn-0020]

Provenance

OpenAI, 23 September 2026 [cn-0042], equation (2.5); reconstructed as a reading account on 9 October 2026. Lean source: NodeRankLoss.

Status: proof-account

Statement. In the polynomial setup [cn-0019], assume \(U_j\cap V_j=0\) for every \(j\). At each degree \(h\geq 0\),

Proof. Fix a non-node \(t_*\). At stage \(e\), choose \(\ell _e\) polynomial maps of degree at most \(e\) whose evaluations at \(t_*\) extend the previously chosen basis of the evaluation space. Through stage \(h\) there are \(r_h=k_h(W)\) columns, independent at \(t_*\). Some \(r_h\)-row square minor \(\Delta _h\) is therefore nonzero at \(t_*\).

Expanding its determinant and using the degree of each column gives

At \(t_j\), the node-rank bound [cn-0022] gives rank at most \(k_h(W)-k_h(V_j)\) for the full evaluated column matrix. Restricting rows cannot increase rank, so the square minor has deficiency at least \(k_h(V_j)\). By determinant multiplicity [cn-0021],

Compare degrees. If \(r_h=0\), all \(k_h(V_j)=0\) by inclusion of evaluation spaces at a non-node, and the empty determinant \(1\) gives the same conclusion.

Proof dependencies

Evaluation filtration [cn-0019]; Evaluation dimensions [cn-0020]; Determinant multiplicity [cn-0021]; Node-rank loss [cn-0022]

Provenance

OpenAI, 23 September 2026 [cn-0042], equations (2.4) and (2.6); reconstructed as a reading account on 9 October 2026. Lean source: StageDegreeBound.

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

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],

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

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.

Status: proof-account

Statement. The constant in the subspace inequality [cn-0024] cannot be decreased.

Proof. Write \(W=P\oplus Q\) and divide the \(m\) indices into groups of sizes \(a=\lfloor m/2\rfloor \) and \(b=\lceil m/2\rceil \). In the first group set \((U_i,V_i)=(P,Q)\); in the second set \((U_i,V_i)=(Q,P)\). Every designated pair is disjoint. Only indices from different groups contribute, with total

For example, three indices split \(1+2\) give total \(2\dim W\). This construction makes the balanced product \(e(m-e)\) in the proof less mysterious.

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], Remark 2.2; reconstructed as a reading account on 9 October 2026.

For a linear map \(X:\mathbb R^d\to \mathbb R^d\), its graph subspace is

The map \(v\mapsto (v,Xv)\) identifies \(\ker (X-Y)\) with \(\Gamma _X\cap \Gamma _Y\). Therefore \(\dim (\Gamma _X\cap \Gamma _Y)=d-\operatorname {rank}(X-Y)\). In particular, these two graph subspaces are disjoint exactly when \(X-Y\) is invertible. This is the conversion used by the rank-sum corollary [cn-0027].

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], proof of Corollary 2.3; reconstructed as a reading account on 9 October 2026. Lean source: IndexedMatrixRankSum.

Status: proof-account

Statement. Let \(X_i,Y_i\) be real \(d\times d\) matrices for \(1\leq i\leq m\), with every \(X_i-Y_i\) invertible. For the balanced count [cn-0006] \(d_m\),

The sum is over ordered pairs.

Proof. Apply the subspace inequality [cn-0024] in \(W=\mathbb R^d\oplus \mathbb R^d\) to the graph subspaces [cn-0026] \(U_i=\Gamma _{X_i}\) and \(V_j=\Gamma _{Y_j}\). Their intersection dimensions equal \(d-\operatorname {rank}(X_i-Y_j)\), giving

Each of the \(m\) diagonal terms is \(d\). Remove them and use \(m^2-m-2\lfloor m^2/4\rfloor =2d_m\), checked separately for even and odd \(m\). This yields the assertion. The full rank of the diagonal differences is the only hypothesis involving the matrices.

Proof dependencies

Balanced count [cn-0006]; Subspace inequality [cn-0024]; Graph subspaces [cn-0026]

Provenance

OpenAI, 23 September 2026 [cn-0042], Corollary 2.3, equation (2.7); reconstructed as a reading account on 9 October 2026. Lean source: IndexedMatrixRankSum.

Status: proof-account

Statement. Let \(K\) be any field and \(W\) an \(N\)-dimensional \(K\)-vector space. For \(m\geq 1\) and \(K\)-linear subspaces \(U_i,V_i\subseteq W\) satisfying \(U_i\cap V_i=0\), the subspace inequality [cn-0024] holds with dimensions over \(K\):

Consequently the rank-sum corollary [cn-0027] holds for matrices over \(K\), with ranks over \(K\). No characteristic-zero assumption is needed for these two algebraic statements.

Proof. First suppose \(K\) is infinite. Run the paper's polynomial argument over \(K\), choosing distinct interpolation nodes in \(K\). The proof uses the following field-independent steps.

• Evaluation and interpolation [cn-0020] use division by nonzero node differences and the bound on the number of roots of a nonzero scalar polynomial.
• Specialization of the rank bound [cn-0022] uses polynomial minors vanishing at every non-node. Infinitude of \(K\) makes that an infinite set, so the minors vanish identically.
• Determinant multiplicity [cn-0021] uses a constant change of basis and factors \(\xi -t_j\) from vanishing columns. This requires no derivatives or division by factorials.
• The degree budget [cn-0023] and its summation [cn-0024] compare ordinary nonnegative integers: dimensions, degrees, and multiplicities. They require no order on \(K\).

These steps prove the inequality over every infinite field. For a finite field \(K\), pass to the infinite extension \(L=K(u)\), the rational-function field in an indeterminate \(u\). Set \(W_L=L\otimes _K W\), and let \(U_{i,L},V_{j,L}\) be the \(L\)-spans of the corresponding subspaces. Dimensions and intersection dimensions are preserved:

For completeness, choose bases of \(U_i,V_j\) and express their columns in a basis of \(W\). Each such matrix and their concatenation have the same rank over \(K\) and \(L\): every minor is an element of \(K\), and passage to \(L\) preserves whether it is zero. Apply \(\dim (U\cap V)=\dim U+\dim V-\dim (U+V)\). This proves the displayed equality and preserves the disjointness hypothesis. The inequality over \(L\) therefore gives exactly the claimed inequality over \(K\).

Finally apply the generalized inequality to the graph subspaces in \(K^d\oplus K^d\), just as in the rank-sum proof [cn-0027]. The graph-kernel identification and rank-nullity hold over every field.

Role of the polynomial maps. The maps [cn-0064] \(P(t)\) encode subspace constraints in this algebraic argument. They do not approximate the edge curves of a drawing. In the crossing-number application, \(W=\mathbb R^d\oplus \mathbb R^d\) with \(d=s^2\) for \(n=2s+1\). The actual drawing arcs [cn-0003] have the separate form \(\gamma _e:[0,1]\to \mathbb R^2\); their normalization is handled in the topological branch [cn-0060].

Using the complex numbers. Identifying the drawing plane \(\mathbb R^2\) with \(\mathbb C\) lets us write the same continuous arcs with complex values. It does not impose holomorphicity or alter the real subspaces in the rank argument. Independently, that algebraic argument can be carried out over \(\mathbb C\), by extending the real matrices and subspaces to complex scalars; their ranks and intersection dimensions are preserved as above. These are two different uses of \(\mathbb C\).

Proof dependencies

Subspace inequality [cn-0024]; Rank-sum corollary [cn-0027]

Provenance

Editorial extension of the argument in OpenAI, 23 September 2026 [cn-0042], Lemma 2.1 and Corollary 2.3, added on 9 October 2026. The paper and archived Lean declarations state the real case; the extension below is justified here and has not been formalized locally.