ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Hopf and Whitehead link linking-number computations

Example

Assume ${A C}_{ω}$ . Read a braid word in the standard geometric braid group product convention: the rightmost factor is traversed first from bottom to top, and the closure joins corresponding top and bottom endpoints. A positive Artin half twist has crossing sign $+ 1$ .

The closure of the positive two-strand braid $σ_{1}^{2}$ is the positive Hopf link. Its endpoint permutation is the identity, so it has two components, and both crossings are mixed positive crossings. Hence its linking number is $(1 + 1) / 2 = 1$ .

The standard Whitehead link is the closure of the three-strand braid $β = σ_{1} σ_{2}^{- 1} σ_{1} σ_{2}^{- 2} .$ Its endpoint permutation is $(1 3)$ , so its components are the cycles ${1, 3}$ and ${2}$ . In bottom-to-top traversal order the crossing letters are $σ_{2}^{- 1}, σ_{2}^{- 1}, σ_{1}, σ_{2}^{- 1}, σ_{1}$ . The first, second, third, and fifth crossings are mixed, with signs $- 1, - 1, + 1, + 1$ ; the fourth is a self-crossing. The mixed sum is $0$ , so the linking number is $0$ . The five-crossing braid diagram is a representative, not a claim that the displayed braid word is the unique presentation.

Example references

Eric W. Weisstein, “Whitehead Link,” Wolfram MathWorld

Positive Artin generator convention

Braid closure and cycle components

Countable-choice hypothesis for the integer output

Diagram

The two-strand braid in the figure is read upward. At each positive generator crossing, the left-to-right strand passes under and is interrupted by the grey-white gap; the right-to-left strand passes over. Between the crossings, label $2$ is on the left and label $1$ on the right. The outside arcs close the top endpoints to the matching bottom endpoints.

Facts & Assumptions

Given: ${A C}_{ω}$ , the two displayed braid words, and the crossing-sign convention of this pair.

[A1]

The Axiom of Countable Choice, written ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The endpoint permutation of a geometric braid records the endpoint of each labelled strand, and the components of its closure are exactly the cycles of that permutation (Geometric braids in the disc with setwise endpoints, The closure of a geometric braid).

[F2]

Stacking induces the braid-group product, with endpoint permutations multiplying in the same product order (Stacking of geometric braids is a well-defined associative operation on isotopy classes).

[F3]

The positive geometric half twist is the generator $σ_{i}$ and is calibrated to crossing sign $+ 1$ ; its inverse has the opposite crossing sign (The elementary geometric half twist, its support disc, and its opposite, Oriented crossing signs, diagram writhe, and blackboard framing).

[F4]

For an accepted two-component diagram, the algorithm returns half the signed sum of its mixed crossings (Compute oriented linking number from a diagram, The diagram linking-number scan terminates and returns the stated integer).

Verification

1.1A1F1F2F3F4algebra

For the two-strand braid, $π (σ_{1}^{2}) = (1 2)^{2} = i d$ by [F1] and [F2]. Its two closure cycles are therefore the two singleton components, and each of the two positive generator crossings is mixed. By [F3] their signs are $+ 1, + 1$ ; [F4] gives linking number $1$ .

1.2F1F2algebra

For the Whitehead word, each squared generator contributes the identity endpoint permutation, leaving $π (β) = (1 3)$ ; hence [F1] gives component cycles ${1, 3}$ and ${2}$ . Traversing from bottom to top, the first two $σ_{2}^{- 1}$ crossings exchange labels $2$ and $3$ , so they are mixed; the following $σ_{1}$ exchanges $1$ and $2$ , so it is mixed; the next $σ_{2}^{- 1}$ exchanges $1$ and $3$ , so it is a self-crossing; the final $σ_{1}$ exchanges $2$ and $3$ , so it is mixed.

2.1A1F3F4step 1.2algebra∎

By [F3], the mixed signs of the Whitehead word are $- 1, - 1, + 1, + 1$ in that traversal, whose sum is $0$ . The algorithm in [F4] therefore returns $0 / 2 = 0$ , as claimed. These are finite crossing checks; the general invariance proof is separate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

Eric W. Weisstein, Whitehead Link, Wolfram MathWorld (standard reference, not scraped)
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)