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.
The diagram linking-number scan terminates and returns the stated integer
Statement
Assume the Axiom of Countable Choice. On every finite regular oriented diagram
with exactly two components, the crossing-scan algorithm halts after one
iteration per crossing and returns the integer half-sum of the mixed crossing
signs. On an input with any other number of components it returns
invalid-input after the finite component-count check.
Statement references
Facts & Assumptions
Given: The Axiom of Countable Choice and a finite regular oriented diagram with its declared component set.
The Axiom of Countable Choice, written (The Axiom of Countable Choice ()).
A regular oriented diagram has finitely many transverse double points and finitely many link components (Regular oriented link diagrams).
On the two-component input the procedure scans each crossing once, adds its sign exactly when its branches lie on distinct components, and returns half the resulting sum (Compute oriented linking number from a diagram).
For every regular two-component diagram, the mixed crossing sum is even and its half is the integer linking number (The mixed crossing sum is even and defines linking number).
Proof
The component-count check terminates because the input declares a finite component set. It returns invalid-input when that cardinality is not two. Otherwise the finite crossing list has some length by [F1], and the algorithm performs exactly one update for each of those crossings with no recursive call or unbounded search. Hence the scan halts after exactly iterations.
In the accepted case, the update in [F2] adds precisely each summand of and no self-crossing. Thus the returned value is ; [F3] shows this is an integer and is the linking number specified in the lemma. All arithmetic is a finite integer sum.
Depends on
Used by
- Pairwise linking numbers do not classify labeled links Counterexample
- Framed knots, self-linking, and the Seifert framing Definition
- Hopf and Whitehead link linking-number computations Example
- The Borromean string link has nonzero triple Milnor invariant Example
- The degree-one derivative of linking number Example
- Piccirillo’s Conway diagrams give a dualizable handle link Lemma
- Small framed push-offs define a well-defined self-linking number Lemma
- The one-term relation and framing Lemma
- A dualizable handle link gives two zero-trace descriptions Theorem
- Blackboard self-linking equals diagram self-writhe Theorem
- Linking number and Fox coloring finite complexity Theorem
- Linking number equals signed intersection with a spanning surface Theorem
- Linking number is invariant and writhe changes under a kink Theorem
Dependency tree · two levels
17 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), §3.3, pp. 26–29 (standard reference, not scraped)
- Mohamed Elhamdadi, Mustafa Hajij, and Kyle Istvan, Framed Knots, arXiv:1910.10257v6 (2020), §3, pp. 3–9 (standard reference, not scraped)