Theorem. The lower bound when the second part is odd [cn-0035]

Status:

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

\[R^{ik}=\Phi (J^{ik}),\qquad X_i=R^{i1},\qquad Y_k=R^{11}-R^{1k}.\]

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:

\[2d_m s^2\leq \sum _{i\ne k}\operatorname {rank}R^{ik}\leq \sum _{i\ne k}c_{ik}=2c(D).\]

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.