Status: proof-account

Statement. For all positive integers \(m,n\), the ordinary crossing number [cn-0005] of \(K_{m,n}\) [cn-0002] is its Zarankiewicz number [cn-0006]:

This is Theorem 1.1 of the paper [cn-0042]. The notes below reconstruct its proof. The label “proof-account” records that role; it does not assert that the accompanying Lean code was compiled in this workspace. See the verification record [cn-0039].

Proof. The balanced-axis construction [cn-0036] gives the upper bound. If either part has at most two vertices, the claimed value is zero and nonnegativity gives equality. For odd \(n\geq 3\), the odd lower bound [cn-0035] proves the reverse inequality by converting signed intersections into a rank sum. For even \(n>2\), vertex deletion [cn-0037] reduces the lower bound to the odd case. These cases exhaust the positive integers.

The proof introduction [cn-0070] explains the subspace inequality, the matrix sizes and star indices, and the conversion from ranks to crossing counts. The guided account [cn-0001] includes the final proof assembly in full.

Proof dependencies

Complete bipartite graphs [cn-0002]; Crossing number [cn-0005]; Zarankiewicz number [cn-0006]; Odd lower bound [cn-0035]; Upper bound [cn-0036]; Even reduction [cn-0037]

Provenance

OpenAI, 23 September 2026 [cn-0042], Theorem 1.1 and Section 5; reconstructed as a reading account on 9 October 2026. Lean source: Main.

The first ingredient is an inequality about subspaces. Fix an integer \(m\geq 1\), a real vector space \(W\) of finite dimension \(N\), and two indexed families of linear subspaces \(U_1,\ldots ,U_m\) and \(V_1,\ldots ,V_m\) of \(W\). Suppose \(U_i\cap V_i=\{0\}\) for every \(i\). The subspace-intersection inequality [cn-0024] states that

The sum runs over all \(m^2\) ordered pairs of indices. Its diagonal terms, with \(i=j\), are zero by hypothesis; intersections with \(i\ne j\) can have positive dimension. Thus (1.2) bounds the total of these intersection dimensions in terms of the number of pairs of subspaces and the dimension of their common ambient space.

To prove this inequality, choose distinct real interpolation nodes [cn-0063] \(t_1,\ldots ,t_m\) and consider univariate polynomial maps [cn-0064] \(P:\mathbb R\to W\) subject to \(P(t_i)\in U_i\). The constrained evaluation spaces [cn-0019] record how their values can vary as the degree increases. Determinant multiplicity [cn-0021] turns the restrictions at the nodes into a bound on polynomial degrees. The algebraic branch [cn-0061] gives the complete argument leading to (1.2).

The useful consequence for crossings is a bound on matrix ranks. Fix a positive integer \(d\), and let \(X_1,\ldots ,X_m\) and \(Y_1,\ldots ,Y_m\) be real \(d\times d\) matrices. Here \(\operatorname {rank}\) is the dimension of the image of the corresponding linear map on \(\mathbb R^d\). Assume every diagonal difference \(X_i-Y_i\) is invertible. Apply (1.2) in the ambient space \(W=\mathbb R^d\oplus \mathbb R^d\), of dimension \(N=2d\), to the graph subspaces [cn-0026]

A vector belongs to both graphs exactly when its first coordinate \(v\) satisfies \((X_i-Y_j)v=0\). Hence

In particular, invertibility of \(X_i-Y_i\) gives the required diagonal disjointness. Recall the balanced pair count [cn-0006] \(d_r=\lfloor r/2\rfloor \lfloor (r-1)/2\rfloor \) for a positive integer \(r\). Substituting the displayed dimension formula into (1.2) and removing the \(m\) diagonal rank terms gives the rank-sum corollary [cn-0027]:

This sum is again over ordered pairs. The integer \(d\) is the size of the matrices; the subscripted integer \(d_m\) is the balanced pair count determined by \(m\). We will construct matrices whose off-diagonal ranks are bounded by crossings and whose diagonal differences are invertible.

For the main part of the drawing argument, assume \(m\geq 3\) and \(n=2s+1\geq 3\), where \(s\) is a positive integer. Set \(d=s^2\); then \(d=d_n\). The second algebraic ingredient is the linear rank detector [cn-0032]

Its input and output sizes serve different purposes: an input matrix will compare the \(n\) edges in one vertex star with the \(n\) edges in another, while the output will enter the rank-sum inequality above. Three properties of \(\Phi \) make this possible.

First, let \(\mathcal L\subseteq \mathbb R^{n\times n}\) be the space of row-plus-column matrices [cn-0017]: matrices \(H\) whose entries have the form \(H(p,q)=r_p+c_q\) for some vectors \(r,c\in \mathbb R^n\). The detector annihilates [cn-0033] both \(\mathcal L\) and every diagonal input matrix. Adding either kind of matrix to \(H\) therefore leaves \(\Phi (H)\) unchanged.

Second, the contribution of a single input entry to \(\Phi (H)\) has rank at most one, and a diagonal input entry contributes zero. Consequently the support rank bound [cn-0033] gives, for every \(H\in \mathbb R^{n\times n}\),

The right-hand side counts the nonzero off-diagonal entries of \(H\). This is how a bound on matrix entries will become a bound on crossings.

Third, for a linear order \(\prec \) on \(\{1,\ldots ,n\}\), let \(S_\prec \) be its half-order matrix [cn-0011]: its entry is \(+1/2\) when \(p\prec q\), \(-1/2\) when \(q\prec p\), and \(0\) when \(p=q\). The order-invertibility lemma [cn-0034] proves

The same map \(\Phi \) works for all these orders. The detector branch [cn-0062] constructs it from barycentric weights [cn-0030] and bivariate evaluation vectors [cn-0028], using one fixed tuple of distinct real nodes. Two-triangle interpolation [cn-0029] supplies the invertibility argument.

We now obtain the input matrices from a drawing. Write the vertex classes of \(K_{m,n}\) [cn-0002] as \(\{a_1,\ldots ,a_m\}\) and \(\{b_1,\ldots ,b_n\}\). Begin with any admissible drawing [cn-0004] \(D_0\). By normalization [cn-0009], replace it by a normalized drawing [cn-0008] \(D\), with polygonal edges and no adjacent-edge crossings, such that its crossing count [cn-0005] satisfies \(c(D)\leq c(D_0)\). A lower bound for \(c(D)\) will therefore give the same lower bound for \(c(D_0)\).

Orient the edge \(a_i b_p\) from \(a_i\) to \(b_p\), and abbreviate it to \(ip\). We use \(i,k\in \{1,\ldots ,m\}\) for first-class vertices and \(p,q\in \{1,\ldots ,n\}\) for second-class vertices. The star at \(a_i\) [cn-0002] consists of its \(n\) incident edges \(i1,\ldots ,in\).

At each vertex \(v\), choose a gap between outward spokes and read them counterclockwise from that gap. The resulting spoke comparison sign [cn-0011] \(T_v(e,f)\) is \(+1\) if the spoke of \(e\) precedes that of \(f\), \(-1\) for the reverse order, and \(0\) if \(e=f\). For two distinct oriented edges \(e,f\), let \(I(e,f)\) be their signed interior intersection count [cn-0010], summing the signs of all their crossing points.

The endpoint-corrected intersection matrix [cn-0013] \(J\) is a real \(mn\times mn\) matrix whose rows and columns are indexed by edges. Set \(J(e,e)=0\). If \(e,f\) are independent, set \(J(e,f)=I(e,f)\); if they share a vertex \(v\), add the endpoint term \(\tfrac 12T_v(e,f)\). This form of the endpoint term uses our orientation: at any shared vertex, both incident edges point outward or both point inward.

Group the edges by their first-class endpoints. The resulting \(n\times n\) star block [cn-0013] \(J^{ik}\) compares the star at \(a_i\) with the star at \(a_k\):

The endpoint corrections make the cycle-pairing identity [cn-0016] hold. Its topological input is that the mutual signed intersection [cn-0069] of two closed polygonal walks meeting transversely away from their corners in the plane is zero [cn-0015]. Applying the cycle identity to suitable four-cycles gives the additive block relation [cn-0018]

Here \(a_1\) is a fixed reference vertex, and \(\mathcal L\) is the row-plus-column space defined above. Apply \(\Phi \) to each block and write \(R^{ik}=\Phi (J^{ik})\), a \(d\times d\) matrix. Since \(\Phi \) annihilates \(\mathcal L\), the relation becomes \(R^{ik}=R^{i1}+R^{1k}-R^{11}\). Thus setting

gives precisely the required difference form \(R^{ik}=X_i-Y_k\). These are the matrices to which we apply the rank-sum corollary.

On the diagonal, all edges in the star at \(a_i\) share that vertex, so normalization has removed their interior crossings. Therefore \(J^{ii}\) is exactly the half-order matrix [cn-0011] of the spoke order at \(a_i\). The detector's invertibility property gives \(\operatorname {rank}R^{ii}=d\); equivalently, every \(X_i-Y_i\) is invertible. This concerns diagonal star blocks, each an \(n\times n\) matrix, rather than diagonal entries within an input matrix.

For \(i\ne k\), let \(c_{ik}\) be the number of crossing points between an edge in the star at \(a_i\) and an edge in the star at \(a_k\). In \(J^{ik}\), entries with \(p=q\) can have an endpoint correction at \(b_p\), but the detector annihilates these diagonal input entries. For \(p\ne q\), the two edges \(ip,kq\) are independent, so \(J^{ik}(p,q)=I(ip,kq)\). Each nonzero such entry requires at least one crossing of that pair. The support rank bound therefore yields

The count \(c_{ik}\) includes every crossing point, even when the same two edges cross repeatedly. Cancellation between positive and negative crossings can make a signed entry smaller or zero; it does not invalidate this rank bound.

The odd-size lower bound [cn-0035] now follows by putting the two rank estimates together, using \(d=d_n\):

Both sums run over ordered pairs of distinct first-class indices. Every crossing of the normalized drawing involves two distinct first-class stars and is counted once in each order, which explains the factor \(2\) on the right. Dividing by \(2\) gives \(c(D)\geq d_m d_n\), and hence \(c(D_0)\geq d_m d_n\).

For even \(n>2\), the vertex-deletion argument [cn-0037] transfers the lower bound from odd second-class sizes. The balanced-axis construction [cn-0036] gives a drawing with exactly \(d_m d_n\) crossings, supplying the matching upper bound. If either class has at most two vertices, this upper bound is zero. Together these steps prove the crossing-number formula [cn-0007].

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], Section 1, from the paragraph containing equation (1.2) to the end of the introduction; rewritten with explicit notation and links on 9 October 2026.

Status: proof-account

Statement. For \(m\geq 3\) and \(n=2s+1\geq 3\), every admissible drawing [cn-0004] of \(K_{m,n}\) has crossing count [cn-0005] at least \(d_m d_n\), with \(d_n=s^2\) [cn-0006].

Proof. Normalize [cn-0009] the drawing without increasing its count. Form the corrected star blocks [cn-0013], fix any one tuple of distinct detector nodes, and set

The additive block relation [cn-0018] and detector annihilation [cn-0033] give \(R^{ik}=X_i-Y_k\). On the diagonal, \(J^{ii}\) is the spoke half-order matrix because normalization has removed all crossings between edges of the same star. By invertibility for every order [cn-0034], \(\operatorname {rank}(X_i-Y_i)=s^2\).

For \(i\ne k\), let \(c_{ik}\) count crossing points between the stars at \(a_i,a_k\). The entries \(J^{ik}(p,p)\) may contain terms at their shared second-class endpoint, but the detector kills all diagonal entries. For \(p\ne q\), the edges are independent, so \(J^{ik}(p,q)\) is just their signed crossing count. A nonzero entry requires at least one crossing of that pair. The rank-one support bound therefore gives \(\operatorname {rank}R^{ik}\leq c_{ik}\). Repeated crossings and cancellation of signs can only decrease this rank estimate.

Apply the rank-sum corollary [cn-0027], then sum the crossing bounds over ordered pairs:

The final equality uses normalization: every crossing involves two distinct first-class stars and contributes once to each of their two orders. Divide by two. The original drawing has at least as many crossings as its normalized replacement, so the lower bound holds for it as well.

Why this does not establish the independent-count bound. If adjacent crossings are retained, the same formula for the corrected matrix [cn-0013] gives \(J^{ii}=S_i+I^{ii}\), where \(S_i\) is the spoke half-order matrix and \(I^{ii}(p,q)=I(ip,iq)\) records signed interior crossings within the star at \(a_i\). The invertibility lemma [cn-0034] applies to \(S_i\); it does not establish invertibility of \(\Phi (S_i+I^{ii})\). Although the off-diagonal support estimate counts independent crossings, the diagonal rank step therefore cannot simply be applied to an unnormalized drawing.

This hypothesis is explicit in the Lean declaration diagonal_detector_isUnit, which takes \(\mathtt {NoAdjacentCrossings}\ D\). Moreover, normalization [cn-0009] compares the replacement's total count with the original total count, not with its independent count [cn-0066]. An extension to \(\operatorname {cr}_-\) would require an additional argument.

Proof dependencies

Admissible drawings [cn-0004]; Crossing count [cn-0005]; Balanced factors [cn-0006]; Normalization [cn-0009]; Corrected matrix [cn-0013]; Additive block relation [cn-0018]; Rank sum [cn-0027]; Annihilation and rank bound [cn-0033]; Order invertibility [cn-0034]

Provenance

OpenAI, 23 September 2026 [cn-0042], Section 5.2, equations (5.2)–(5.4); reconstructed as a reading account on 9 October 2026. Lean source: OddNormalizedLowerBound.

Status: proof-account

Statement. If the lower bound \(c(D')\geq d_m d_{n-1}\) holds for every admissible drawing [cn-0004] of \(K_{m,n-1}\), and \(n>2\) is even, then every drawing of \(K_{m,n}\) has crossing count [cn-0005] at least \(d_m d_n\).

Proof. Normalize [cn-0009] without increasing the count. Delete each of the \(n\) second-class vertices in turn. Each remaining drawing has at least \(d_m d_{n-1}\) crossings. Every crossing of the normalized drawing has two distinct second-class endpoints, so survives precisely \(n-2\) of the deletions. Therefore

The equality follows from the balanced factors [cn-0006]: for \(n=2s\), \(d_n=s(s-1)\) and \(d_{n-1}=(s-1)^2\). Divide by \(n-2>0\). The case \(n=2\) is instead settled by the zero-factor upper bound. The paper cites Kleitman, Section 3 [cn-0052] and Woodall, Theorem 1 and Corollary 1.1 [cn-0057] for this deletion count.

Proof dependencies

Admissibility [cn-0004]; Crossing count [cn-0005]; Balanced factors [cn-0006]; Normalization [cn-0009]; Odd lower bound [cn-0035]

Provenance

OpenAI, 23 September 2026 [cn-0042], Section 5.3; reconstructed as a reading account on 9 October 2026. Lean source: DeletionCount.

Status: proof-account

Statement. For positive integers \(m,n\), there is an admissible drawing [cn-0004] of \(K_{m,n}\) [cn-0002] with exactly the Zarankiewicz count [cn-0006] \(d_m d_n\).

Proof. Put the first-class vertices on the vertical axis, split evenly between its positive and negative rays. Put the second-class vertices on the horizontal axis with the same balanced split. Choose distinct nonzero positions and draw straight edges. Every edge interior lies in an open quadrant.

If a quadrant has \(u\) first-class and \(v\) second-class vertices on its bounding rays, each choice of two from each ray forms a convex quadrilateral. Exactly its two diagonals cross. Thus the quadrant contributes \(\binom u2\binom v2\) crossings, provided triple concurrence is avoided. Summing the four products gives

To avoid triple concurrence, note that three edges concurrent in their interiors have six distinct endpoints: adjacent straight edges do not meet in their interiors. For each such triple, concurrence imposes a nonzero polynomial condition on its axis intercepts. Holding two segments fixed and varying an intercept of the third shows that this condition is not identically zero. The product of the finitely many polynomials cannot vanish on the open set of permitted positions. Choose positions outside its zero set. The resulting crossings are transverse and no three edges meet, so the drawing is admissible.

This is the classical construction, cited in the paper through Woodall, page 658 [cn-0057] and Zarankiewicz [cn-0058].

Proof dependencies

Complete bipartite graphs [cn-0002]; Admissibility [cn-0004]; Balanced pair counts [cn-0006]

Provenance

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