Theorem. The crossing-number formula: statement and assembly [cn-0007]

Status:

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

\[\operatorname {cr}(K_{m,n})=d_m d_n.\]

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.