OAI.Zarankiewicz.mainTarget_proof

The theorem states, as an admitted result, that the defined proposition MainTarget holds, which is the Zarankiewicz crossing-number formula for complete bipartite graphs. Define axisPairs(r) = ⌊r/2⌋·⌊(r−1)/2⌋. MainTarget says that for all positive integers m and n, there is an admissible drawing of the complete bipartite graph K_{m,n} in the plane ℝ×ℝ with exactly axisPairs(m)·axisPairs(n) crossings, and every admissible drawing has at least axisPairs(m)·axisPairs(n) crossings. An admissible drawing assigns distinct plane points to the m+n vertices, and to each pair (i,j) of a left and right vertex an injective continuous path from the left vertex to the right vertex, whose interior points avoid all vertices. It must also satisfy three conditions: the set of crossing points is finite, where a crossing point lies in the interiors of two distinct edges; at each such point the two edge interiors meet properly, meaning that some local homeomorphism chart of the plane sends the point to the origin, one edge interior to the horizontal axis and the other to the vertical axis near it; and no point lies in the interiors of three pairwise distinct edges. The crossing count is the number of crossing points.