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.
Planar-code validation and diagram reconstruction
Definition
Input: A finite tagged Gauss code, signed Dowker–Thistlethwaite code, or oriented planar-diagram code in the conventions of this page. The crossing count is a nonnegative integer. When , the code includes the finite crossing labels, edge-end incidences, strand arrows, over/under data, crossing signs, and a distinguished outer face. When , the only admissible input for this procedure is the one-component crossingless code specified in the code definition.
Output: Either Invalid(reason, witness), where reason is the first
failed check below and witness identifies the offending field, label, or
crossing, or Valid(diagram, components, faces, outerFace). Here diagram is
a finite gluing record consisting of one crossing disk per vertex, one
rectangular edge band for each pair of darts under , and one cap disk
per cycle of the face permutation. Each band is attached at its recorded dart ports, and each
crossing disk records its clockwise order, strand orientations, over/under
pair, and sign. components lists the oriented link cycles, faces lists the
face-permutation cycles, and outerFace is the selected cycle. The gluing
record represents a polygonal spherical diagram; deleting a point in its
selected face gives the plane model. The procedure tests realizability of
this code only; it does not compare the represented link with another code.
Instructions:
-
Read the tag and crossing count. If the tag is unknown or is not a nonnegative integer, return
invalid-headerwith that field. -
If , accept only one empty Gauss component word, the empty signed-DT code, or the single
Loop[1]PD record, each with exactly one orientation marker,ccworcw. Returninvalid-crossingless-codeotherwise. If the outer-face marker is not exactlyoutside, returninvalid-outer-facewith that marker. For an accepted input return the standard circle with the marked orientation, one component, its two sphere faces, and theoutsideface selector. Do not run crossing-graph tests. -
For a Gauss code with , if a component word is empty, return
invalid-empty-component-wordwith the first such component index. Check that every label lies in , occurs exactly twice in total, and occurs once with each over/under sign. Check that its separate crossing-sign vector has length and entries in . Returninvalid-crossing-labelfor the first out-of-range label,invalid-crossing-visit-countwith the label and its over/under counts for any visit failure, orinvalid-crossing-sign-vectorwith the first bad position. Turn successive visits on each component word into directed edge labels, including each cyclic last-to-first edge, numbering these segments in the listed component order and then in traversal order, and form the crossing records from the over/under visits and the stored crossing signs. -
For a signed DT code, check that its pairing list and sign vector each have length , each pairing value has absolute value in , every such absolute value occurs once, and every sign is or . Return
invalid-dt-pairingwith the first bad index for a pairing failure, orinvalid-crossing-sign-vectorwith the first bad position for a sign failure. The odd visit is crossing ; if it is the over-visit and if it is the under-visit. At the even visit paired with , use crossing label and the opposite over/under sign. Decode visits in order into the corresponding signed Gauss word and continue with step 3. -
For a PD code, check that there are exactly crossing records and four dart occurrences at each record. Return
invalid-crossing-recordwith the first bad record otherwise. Use the edge labels and arrows in the records to form the paired-dart involution, crossing rotations, over/under pairs, and crossing signs. -
In every nonempty encoding, check that each edge label has exactly two occurrences, one incoming and one outgoing; each crossing has exactly four incident darts; the opposite pairs are exactly one over-strand and one under-strand; each strand has one incoming and one outgoing end; and the cyclic order matches the stored crossing sign. Return, in that order,
invalid-edge-incidence,invalid-crossing-valence,invalid-over-under-pair,invalid-strand-orientation, orinvalid-crossing-sign-order, with the first offending label or crossing. -
Starting at each as-yet unvisited outgoing dart, cross its edge by to the incoming dart at the other endpoint and continue through the opposite dart of that same strand. Stop only when the starting outgoing dart is reached. If an end is missing, a dart repeats before that return, or any dart remains uncovered after all cycles are traced, return
invalid-component-closurewith the first such dart. Then test the crossing graph for connectedness; if it is disconnected, returndisconnected-crossing-graph. -
Compute on all darts by finite table lookup and list its cycles. Put , , and the number of cycles. If , return
non-spherical-face-countwith . If the supplied outer-face identifier is not one of these cycles, returninvalid-outer-facewith that identifier. -
For a passing code, choose the lexicographically first spanning tree in the finite edge ordering. Root it at the least crossing label and attach its tree bands in increasing distance from that root, using the recorded cyclic gaps. Then attach the remaining edge bands in increasing edge-label order. Use the distinguished face for the plane projection, replace each crossing disk by its prescribed transverse crossing, attach one cap disk along each face cycle, and lift the over-strand above the under-strand. Return this finite gluing record, the directed components, the face cycles, and the outer-face identifier.
Definition references
Planar-diagram, Gauss, and signed Dowker–Thistlethwaite codes — exact accepted input formats, signs, and face permutation.
Realizability and face validation for planar-diagram codes — the spherical realization criterion used at steps 8–9.
Hass–Lagarias–Pippenger, §§1, 3 — finite link-diagram graph input and crossing data.
Erickson, “Planar Graphs” — permutation-based face computation and outer-face convention.
Depends on
Used by
- Breadth-first Reidemeister search Algorithm
- Enumerate diagrams up to a crossing bound Algorithm
- Enumerate Reidemeister move neighbors from a knot code Algorithm
- Haken–Jaco–Tollefson normal-surface unknot search Algorithm
- A crossing label occurring once is invalid Counterexample
- Trefoil Gauss traversal and rotation reconstruction Example
- Linear-size good exterior triangulation from a planar knot code Lemma
- Planar-code validation and reconstruction procedure properties Theorem
Dependency tree · two levels
6 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
- Joel Hass, Jeffrey C. Lagarias, and Nicholas Pippenger, The Computational Complexity of Knot and Link Problems, Journal of the ACM 46 (1999) (standard reference, not scraped)
- Jeff Erickson, Planar Graphs, Computational Topology lecture notes (2023) (standard reference, not scraped)