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.
Termination and finite output of the Seifert diagram procedure
Statement
Assume the Axiom of Countable Choice. For every finite regular oriented diagram with exactly one component, the Seifert diagram procedure terminates after one finite smoothing scan and one finite band-record scan. It returns exactly one disk record for each Seifert circle and exactly one band record for each original crossing. Termination alone asserts no embeddedness, boundary equality, or genus minimality.
Statement references
Facts & Assumptions
Given: and a regular oriented knot diagram .
The Axiom of Countable Choice is the sequence principle stated in the item. (The Axiom of Countable Choice ())
The procedure performs one oriented smoothing at each crossing, records the Seifert circles, and then records one band for each crossing. (Seifert disk-and-band construction from an oriented knot diagram)
A regular oriented diagram has finitely many double points, all transverse, and no triple points. (Regular oriented link diagrams)
Smoothing every crossing produces a finite disjoint union of oriented simple closed curves. (Seifert smoothing and Seifert circles of an oriented link diagram)
Proof
By [F2], has a finite crossing set of cardinality . The first loop in [F1] visits each crossing once and performs one smoothing, so it ends after iterations. No smoothing introduces a new crossing to be processed.
By [F3], the completed smoothing has a finite set of Seifert circles of cardinality . The second loop in [F1] records one disk per circle and one band per original crossing, so it also has finitely many iterations and returns exactly with the prescribed records. No topological correctness claim follows from this finite termination argument.
Depends on
Used by
Dependency tree · two levels
15 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, §3.2, pp.24–26 (standard reference, not scraped)
- Alessia Cattabriga and Stefano Francaviglia, Knot Theory and Applications: Lecture Notes, §4.3, pp.21–23 (standard reference, not scraped)