Definition. Crossing count and ordinary crossing number [cn-0005]

For an admissible drawing [cn-0004] \(D\), its crossing count \(c(D)\) is the number of points belonging to two distinct edge interiors. Every crossing point is counted: a pair that crosses three times contributes three. This is neither a count of crossing edge pairs nor a parity count. See Pach–Tóth [cn-0053] for the distinctions between these invariants.

The ordinary crossing number is

\[\operatorname {cr}(G)=\min \{c(D):D\text { is an admissible drawing of }G\}.\]

For the complete bipartite graphs studied here, the axis construction [cn-0036] supplies an admissible drawing. The attainable counts form a nonempty subset of the nonnegative integers, so their least element is attained. The Lean definition uses the infimum of this set; existence and attainment are proved separately.

Counting only crossings between edges with no common endpoint gives the separately defined independent crossing number [cn-0066].

Proof dependencies
Admissible drawings [cn-0004]
Provenance
OpenAI, 23 September 2026 [cn-0042], Section 1; reconstructed as a reading account on 9 October 2026. Lean source: DrawingDefinition.