Status: proof-account

Statement. Every admissible drawing [cn-0004] of a finite simple graph can be replaced by a normalized drawing [cn-0008] with no greater crossing count [cn-0005].

Proof. Isolate finitely many marks. Mark the vertices and crossings. On each injectively parameterized edge choose disjoint parameter neighborhoods of its marks, with disjoint closures. The compact remainder of that edge avoids each corresponding mark. Compactness and finiteness therefore allow disjoint closed round disks around the marks, such that all visits to a disk occur inside its chosen parameter neighborhood and nonincident edges avoid the disk.

At an interior mark remove the interval from the first to the last visit to its disk. At an initial vertex remove the initial interval through the last visit; at a terminal vertex remove the final interval from the first visit. The retained pieces are disjoint compact arcs, with distinct boundary endpoints and interiors outside all disks. This use of first and last visits avoids assuming finitely many intersections with a disk boundary.

Give those compact pieces pairwise disjoint open neighborhoods. At each boundary endpoint take a short radial outward spur. A sufficiently small exterior collar connects its tip to a nearby point of the original arc without entering any disk. The resulting connection lies in an open set. Cover its compact image by small balls in that set, subdivide the parameter interval, and replace each short subarc by a straight segment within its ball. This gives a polygonal path with the required endpoints. Subdivide its finite segment arrangement and take a simple graph path to erase loops and overlaps. Disjoint neighborhoods keep the replacements disjoint.

Inside a crossing disk connect the two endpoint pairs by straight chords. Four distinct boundary points give at most one transverse crossing. Inside a vertex disk choose a new vertex off the finitely many lines through pairs of boundary points, and connect all points to it by straight spokes. Assemble the exterior pieces and disk pieces in their original edge order. Each edge is simple, no interior contains a vertex, and every new crossing lies in an old crossing disk. There is at most one crossing per such disk and no third edge there.

Remove adjacent crossings. Suppose \(vu\) and \(vw\) cross at \(x\). In a small disk containing just that crossing, exchange their prefixes from \(v\) and reconnect each exchanged prefix to the appropriate original suffix. The new connections pair adjacent boundary points, so disjoint chords remove the crossing. Outside the disk the two walks use each old open track exactly once in total.

Subdivide their tracks at bends and crossings, and delete closed subwalks until each walk is simple. At a remaining old crossing, either the two tracks belong to different walks, in which case retained passages remain straight through, or both belong to one walk, in which case a new turn can occur only where the other walk and all third edges are absent. The same reasoning applies to meetings with third edges. Thus this simplification adds no crossings or improper meetings. It preserves the abstract endpoints and strictly reduces the point count.

Repeat while an adjacent crossing remains. The nonnegative integer count decreases at every step, so the process terminates. Straightness near the remaining vertices and crossings is preserved. This proves the assertion. The paper discusses the standard ordinary-crossing reduction with reference to Fulek et al. [cn-0049]; the continuous-arc construction is written out in its Appendix A.

Scope of normalization. For the replacement \(D'\), the proved comparison is \(c(D')\leq c(D)\). It does not give \(c(D')\leq c_-(D)\), where \(c_-(D)\) is the independent crossing count [cn-0066]. Thus the lemma justifies prohibiting adjacent crossings when minimizing the ordinary count, but does not prove \(\operatorname {cr}_-(G)=\operatorname {cr}(G)\).

The prefix exchange explains the distinction. In a complete bipartite graph take \(e=a_1b_1\), \(f=a_1b_2\), and \(g=a_2b_1\). If a prefix of \(e\) crossing \(g\) is reassigned to \(f\), that retained crossing changes from adjacent to independent: \(e\) and \(g\) share \(b_1\), whereas \(f\) and \(g\) have no common endpoint. No new crossing point is needed for the number of counted independent crossings to increase. The 2012 reference [cn-0049], p. 760, explicitly distinguishes these two minimization problems.

Proof dependencies

Admissibility [cn-0004]; Point count [cn-0005]; Normalized drawings [cn-0008]

Provenance

OpenAI, 23 September 2026 [cn-0042], Appendix A, Lemma A.1; reconstructed as a reading account on 9 October 2026. Lean source: LocallyTransverseNormalization.

Let \(C\) be a straight chord of a round disk, oriented from its starting endpoint \(c_-\) to its terminal endpoint \(c_+\). Write \(\partial C=\{c_-,c_+\}\) for its two-element endpoint set. The endpoint-coefficient function \(\epsilon _C:\partial C\to \{-1,+1\}\) is defined by

Thus \(\epsilon _C(u)\) is the endpoint coefficient of \(C\) at \(u\). For another oriented chord \(E\), the notation \(\epsilon _E(w)\) has the same meaning: \(-1\) at the start of \(E\) and \(+1\) at its end. Each chord's two coefficients sum to zero; this is the cancellation used in the local chord formula [cn-0014].

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], notation immediately before equation (3.3), inside the proof of Lemma 3.1; made explicit on 9 October 2026.

Status: proof-account

Statement. Let \(C,E\) be oriented straight chords of a round disk, with four distinct boundary endpoints. Write \(\partial C,\partial E\) for their endpoint sets and \(\epsilon _C(u),\epsilon _E(w)\) for their endpoint coefficients [cn-0068]: \(-1\) at the start of the corresponding chord and \(+1\) at its end. Choose a boundary cut avoiding the endpoints. The counterclockwise comparison sign [cn-0011] \(T(u,w)\) is \(+1\) if \(u\) precedes \(w\) when reading from the cut, and \(-1\) otherwise. Then their signed intersection [cn-0010] is

Proof. Moving the cut past an endpoint changes the expression by a multiple of the other chord's total endpoint coefficient, which is zero. Cut just before the start of \(C\). The expression simplifies to minus the sum of the coefficients of \(E\)'s endpoints on the open counterclockwise arc from the start to the end of \(C\). This boundary arc lies on the right of directed \(C\).

If the endpoints do not alternate, that sum is zero. If they alternate, \(E\) goes from right to left or from left to right across \(C\), giving respectively \(+1\) or \(-1\). These are precisely the determinant signs of the two chord directions.

Proof dependencies

Signed intersections [cn-0010]; Comparison signs [cn-0011]; Endpoint coefficients [cn-0068]

Provenance

OpenAI, 23 September 2026 [cn-0042], equation (3.3), inside the proof of Lemma 3.1; reconstructed as a reading account on 9 October 2026. Lean source: ChordPairing.

A polygonal walk \(\gamma =(e_1,\ldots ,e_r)\) in the plane is a finite ordered sequence of directed straight-segment traversals, with the end of each traversal equal to the start of the next. It is closed if its final endpoint equals its initial endpoint. Stationary steps can be omitted. Different portions of the walk may meet or cross, and a segment may be traversed more than once. Each traversal retains its position in the sequence and its direction.

Let \(\gamma =(e_1,\ldots ,e_r)\) and \(\eta =(f_1,\ldots ,f_s)\) be two such walks. Assume every meeting between them is transverse and away from all segment endpoints. For a pair of traversals, set \(I(e_i,f_j)=0\) if they are disjoint; at a crossing set it equal to the sign of the determinant of their two directed segment vectors, in the order \(e_i,f_j\). This is the same sign convention [cn-0010] used for graph edges. Their mutual signed intersection is

The sum has one term for each pair of traversals, one from each walk. A crossing between two portions of \(\gamma \) alone, or between two portions of \(\eta \) alone, is not included. If \(\eta \) passes through a crossing of two portions of \(\gamma \), both pairings with \(\eta \) are included, with their respective signs. Similarly, traversing a segment twice in the same direction counts its intersections with the other walk twice. The closed-walk lemma [cn-0015] states that this mutual sum is zero when both walks are closed.

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], final topological step in the proof of Lemma 3.1; notation and multiplicities made explicit on 9 October 2026. Lean source: PolygonalWalks, definition polygonIntersection.

Status: proof-account

Statement. Let \(\gamma ,\eta \) be two closed polygonal walks [cn-0069] in the plane. Assume every meeting between them is transverse and away from all their corners. Their mutual signed intersection [cn-0069], counting segment traversals with multiplicity, satisfies

Either walk may cross itself, as in a figure-eight. Such self-crossings need not be removed: the sum \(I(\gamma ,\eta )\) includes only pairs with one traversal from each walk. A crossing between two portions of \(\gamma \) alone, or of \(\eta \) alone, is not a summand. If the other walk also passes through that point, all mutual pairs of traversals are counted separately with their signs.

Proof. For the first walk, cone every oriented segment \([u,w]\) to a point \(o\), forming the oriented triangle \([o,u,w]\). Choose \(o\) away from the finitely many lines that cause degenerate triangles, nontransverse cone-segment intersections, or encounters with corners of the second walk.

A closed second walk has equally many entrances into and exits from each triangle, with opposite intersection signs along its oriented boundary. Each triangle boundary therefore has total signed intersection zero. Sum the oriented triangle boundaries: the extra cone segments cancel in oppositely oriented pairs, leaving the first walk. Its intersection sum is zero. This cancellation concerns the auxiliary cone segments; self-crossings of either original walk remain in place throughout the argument.

Proof dependencies

Polygonal walks and mutual signed intersections [cn-0069]

Provenance

OpenAI, 23 September 2026 [cn-0042], final topological step in the proof of Lemma 3.1; reconstructed as a reading account on 9 October 2026. Lean source: ClosedPolygonIntersection.

Status: proof-account

Statement. For the endpoint-corrected matrix [cn-0013] \(J\) of a normalized drawing and signed edge vectors [cn-0012] \(z,y\) of oriented simple graph cycles,

Proof. Put disjoint small round disks around the vertices, meeting edges only in straight spokes. Replace each passage of the first cycle through a disk by a chord. Outside the disks keep its original tracks, obtaining a closed polygonal walk \(\gamma \).

For the second cycle construct two walks \(\eta _+,\eta _-\), shifting its tracks a small distance left and right relative to each fixed edge orientation. Join the shifted endpoints inside each vertex disk by chords. To construct the exterior tracks, also isolate bends and crossings in disjoint small disks and shift each intervening straight stretch parallel to itself.

In a crossing disk the shifted strand avoids its original strand and crosses the other original strand once with the original sign. In a bend disk both shifted ends lie in the same component of the complement of the original bent arc, so a polygonal connector in that component avoids the original arc. Distinct remaining compact stretches have positive separation. With a single sufficiently small shift, no additional intersections or contacts at seams and corners arise.

Consequently, the exterior mutual signed intersection [cn-0069] of \(\gamma \) with each shifted walk is \(z^TIy\). This also handles common edges: a shifted track avoids its own original copy. When both cycles use both strands of an original crossing, the two ordered contributions are counted separately with their traversal coefficients.

In a vertex disk, the endpoint coefficients [cn-0068] are \(\sigma _{ve}z_e\) and \(\sigma _{vf}y_f\). An incoming traversal starts its chord and contributes \(-1\); an outgoing traversal ends it and contributes \(+1\). Apply the chord formula [cn-0014] in each shift. For different spokes their order sign is \(T_v(e,f)\) in both shifts. For a common spoke, the shifted endpoint lies on opposite sides of the original endpoint in the two boundary orders, so its two comparison signs average to zero. This is exactly the convention \(T_v(e,e)=0\); opposite cycle traversals change coefficients, not that cancellation.

Thus the averaged local contribution at \(v\) is

Each total intersection of \(\gamma \) with \(\eta _+\) or \(\eta _-\) is zero by the closed-walk lemma [cn-0015]. Average those two zero totals. Adding the exterior term to the local contributions gives \(z^TJy\), proving the identity.

Proof dependencies

Cycle vectors [cn-0012]; Corrected matrix [cn-0013]; Chord formula [cn-0014]; Closed-walk intersections [cn-0015]

Provenance

OpenAI, 23 September 2026 [cn-0042], Lemma 3.1; reconstructed as a reading account on 9 October 2026. Lean source: CyclePairing.

An \(n\times n\) real matrix is row-plus-column, or additive, if its entries have the form \(H(p,q)=r_p+c_q\) for some vectors \(r,c\in \mathbb R^n\). Write \(\mathcal L\) for this linear subspace. It is the ambiguity removed by the detector.

Equivalently, every rectangular difference vanishes:

Indeed the additive form gives cancellation. Conversely, fix \(p_0,q_0\); the vanishing identity gives \(H(p,q)=H(p,q_0)+H(p_0,q)-H(p_0,q_0)\), which has the required form.

Proof dependencies

None.

Provenance

OpenAI, 23 September 2026 [cn-0042], equation (3.5) and the proof of Lemma 3.2; reconstructed as a reading account on 9 October 2026. Lean source: AdditiveBlockRelation.

Status: proof-account

Statement. The star blocks [cn-0013] of a normalized drawing satisfy

where \(\mathcal L\) is the space of row-plus-column matrices [cn-0017]. Any fixed first-class vertex may replace the reference vertex \(a_1\).

Proof. Call the displayed matrix \(H\). For \(i,k\ne 1\), \(p\ne p'\), and \(q\ne q'\), take the four-cycle vector with entries \(+1\) on \(ip,1p'\) and \(-1\) on \(ip',1p\), and the analogous vector using \(k,q,q'\). Expanding cycle pairing [cn-0016] gives

If one of the index differences is trivial, the rectangular difference vanishes directly. Thus all rectangular differences of \(H\) vanish, and the characterization in the definition [cn-0017] shows that \(H\in \mathcal L\). Shared vertices or edges of the chosen four-cycles cause no exception because the cycle lemma explicitly permits them.

Proof dependencies

Star blocks [cn-0013]; Cycle pairing [cn-0016]; Additive matrices [cn-0017]

Provenance

OpenAI, 23 September 2026 [cn-0042], Lemma 3.2, equation (3.6); reconstructed as a reading account on 9 October 2026. Lean source: AdditiveBlockRelation.