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.
Enumerate Reidemeister move neighbors from a knot code
Definition
Input: A valid normalized oriented planar-diagram code for a connected one-component knot diagram, with crossings. A positive-crossing-count code records its finite crossing labels, four darts at each crossing, edge pairings, clockwise rotations, strand orientations, over/under pairs, crossing signs, and one outer face. A crossingless code records one oriented circle and its outer face.
Output: A finite ordered list of pairs , where is a valid normalized one-component knot code and records either the finite crossing/edge relabeling identifying the unchanged planar-isotopy class or a local disk boundary, move type, and orientation/sign variant witnessing one oriented R1, R2, or R3 move from to . Different labelings of the same candidate may appear more than once.
Finite comparison rules: Two normalized codes represent the same code class when some bijection of their finite crossing labels and edge labels carries all dart incidences, crossing rotations, orientations, signs, component cycles, and outer-face data of one code to the other. For a move-site test use the finite spherical cellulation returned by reconstruction and mark a point at infinity in its distinguished outer face. For the crossingless circle, insert one auxiliary degree-two vertex and use its two complementary face disks; this vertex is suppressed in all comparisons.
For each of , enumerate every distribution of distinct cut points among diagram edges and every linear order of the points on each edge. Use one representative of each order (for example equally spaced interior points); their numerical positions are immaterial. In each face disk enumerate noncrossing pairings of all boundary occurrences of these cut points by interior arcs. In the distinguished face also record which complementary region contains the marked point at infinity. Glue the face arcs at the cut points and retain only choices forming a single simple closed curve. Cutting the finite cellulation along these arcs and flooding across incident cell pieces identifies the two sides; select the side not containing infinity. This is the candidate closed move disk. Its entire diagram intersection, including every vertex, edge segment and possible closed component inside it, must be isomorphic relative to its cyclically ordered boundary points to one side of a standard R1, R2 or R3 template with the chosen orientation/sign variant. In particular no additional diagram portion is permitted inside the disk. All tests are finite incidence and cyclic-order comparisons. The same construction is performed for the other code, requiring the opposite side of the same template and an isomorphism of the outside records fixing the ordered boundary points, all decorations and the infinity region. Store the cut orders, face pairings, selected regions, template variant and outside isomorphism as the certificate.
The local templates and their exact orientation/sign variants are those in the oriented Reidemeister-move definition.
Instructions:
- Validate with the planar-code validation procedure. If it is invalid, return its first invalid-code result.
- Set and run the bounded normalized-diagram enumerator with bound . It returns a finite list of reconstructed one-component knot-diagram candidates.
- For each candidate, form the finite set of normalized code representatives obtained by assigning crossing labels and edge labels in every permitted order and applying the code's normalization rule.
- For each representative , apply the finite comparison rules. Append with a relabeling certificate if it is the same code class as , or with the successful local-site certificate if a comparison certifies one R1, R2, or R3 move between them. Preserve the enumerator order and retain duplicates.
- Return the accumulated list.
The bound includes every one-move result because R1 changes crossing count by one, R2 by two, and R3 by zero. This procedure lists candidates one move away; it does not decide whether two arbitrary codes are related by any number of moves.
Depends on
Used by
Dependency tree · two levels
8 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, University of Chicago course notes (2025), §1.2, pp. 5–7 (standard reference, not scraped)
- Jeff Erickson, Planar Graphs, Computational Topology lecture notes (2023) (standard reference, not scraped)