Alphabeta MathHow 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.
A crossing label occurring once is invalid
Statement refuted
For every positive integer , every finite signed word with labels in in which each declared label occurs at least once is a Gauss code of a closed regular oriented diagram.
Statement references
Planar-diagram, Gauss, and signed Dowker–Thistlethwaite codes — each crossing label occurs exactly once over and once under.
Planar-code validation and diagram reconstruction — visit-count check and its ordered failure reason.
Planar-code validation and reconstruction procedure properties — exact invalid-code return behavior.
Knot Atlas, “Gauss Codes” — each crossing is recorded on both visits, with over/under signs.
Hass–Lagarias–Pippenger, §3 — a regular diagram crossing is a four-valent vertex.
Facts & Assumptions
Given: The declared crossing count and the one-entry word .
Planar-diagram, Gauss, and signed Dowker–Thistlethwaite codes: for each crossing label , a Gauss code contains exactly two visits to , one over and one under.
Planar-code validation and diagram reconstruction: for a nonempty Gauss input, after range checking, the procedure counts the two over/under visits and returns invalid-crossing-visit-count at the first label whose counts are not , before any graph or face test.
Planar-code validation and reconstruction procedure properties: each invalid return is the first failed predicate in the stated procedure order.
Counterexample
Given: The declared crossing count and the one-entry word .
The only declared label is , which lies in . The word has one entry, and its negative sign makes that entry an under-visit. Hence its visit-count pair is , not the required in [F1].
The range check passes, so the validator reaches its Gauss visit-count check. By [F2] and [F3] it returns invalid-crossing-visit-count with before constructing a crossing graph or computing faces. Therefore mere presence of every declared label does not make a signed word a Gauss code.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Knot Atlas, Gauss Codes manual (standard reference, not scraped)
- 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)