How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Disconnected projection components admit a separating Jordan curve
Statement
Let be the nonempty finite projection graph of a regular link diagram. If is disconnected, there is a simple closed curve such that has points on both sides of .
Statement references
Facts & Assumptions
Given: A nonempty finite disconnected projection graph .
A regular projection is a finite graph with finitely many transverse double points and no triple points; crossingless link components are embedded circles (Regular oriented link diagrams).
A smooth Jordan curve in the plane has one bounded and one unbounded complementary region, with the curve as their common boundary; this separation is established in Proof 2.1 of Choice-free smooth Jordan disk parameters and prescribed collars. For a smooth curve on , delete a point off the curve and use a stereographic chart. Adding that point back to the unbounded region leaves it connected and does not meet the closure of the bounded region, so there are exactly two complementary components on . The smooth boundary collar shows that every transverse crossing switches components. Only separation, rather than disk parameters for both spherical sides, is needed here.
Proof
Choose one connected component of . Around each of its finitely many vertices take a small closed disk, and around each edge take a narrow closed strip joining the incident vertex disks; for a crossingless circle take an annular neighborhood. Round the finitely many corners. Because the graph is finite and its distinct components are disjoint compact sets, the disks and strips can be chosen so that their union is a compact connected subsurface of with smooth finite boundary, contains in its interior, and misses every other component of .
Choose points and in another component of . Choose a piecewise-smooth path from to transverse to the finite smooth boundary . Its endpoints lie respectively in the interior of and outside , so it crosses an odd number of times. The boundary has finitely many disjoint simple closed components; at least one, call it , is met an odd number of times. The curve lies in , since contains in its interior and misses every other component. By [F2], every transverse crossing of switches sides, so and lie on opposite sides of .
The construction uses finitely many neighborhoods and applies also when is a crossingless circle; therefore it proves the asserted separation for every nonempty disconnected regular projection. Its chosen separating curve is a smooth boundary component of .
Depends on
Used by
Dependency tree · two levels
4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Danny Calegari, Introduction to Knot Theory, §5.2 and Exercise 5.14, printed pp. 42–43 (standard reference, not scraped)
- William W. Menasco, Closed incompressible surfaces in alternating knot and link complements, Topology 23 (1984), §2, pp. 38–41 (standard reference, not scraped)