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.

Worked Seifert-algorithm counts for the trefoil, figure-eight, and kinked unknot

Example

Assume the Axiom of Countable Choice. Let $D_{T}$ be the standard closure of the two-strand braid $σ_{1}^{3}$ , let $D_{8}$ be the standard closure of the three-strand braid $σ_{1} σ_{2}^{- 1} σ_{1} σ_{2}^{- 1}$ , and let $D_{U}$ be the round unknot diagram with one Reidemeister-I kink. Here each $σ_{i}$ is the elementary geometric half twist of adjacent strands and closure joins the bottom endpoints to the corresponding top endpoint set. These are the standard trefoil, figure-eight, and kinked-unknot diagrams. Their Seifert-algorithm data and output-surface genera are

Diagram	Seifert circles $s$	Crossings $c$	Output genus $g (F)$
Trefoil	2	3	1
Figure-eight	3	4	1
Kinked unknot	2	1	0

Thus the corresponding knot genera are at most $1$ , at most $1$ , and exactly $0$ , respectively. The first two rows compute particular spanning surfaces and do not assert that those surfaces have minimum genus.

The arrows orient the first diagram, and at each crossing the unbroken strand is the overpass.

The picture is a projection schematic: the white gaps mark the underpassing strand, and each closing arc joins a bottom endpoint to the top endpoint on the same side. The smoothing and surface claims below are proved from the finite strand and band data, not from the picture.

Example references

The finite smoothing and band procedure

The output genus formula and knot-genus upper bound

The elementary geometric half twists

Braid-word multiplication and endpoint permutations

Components of a braid closure are cycles of its endpoint permutation

Facts & Assumptions

Given: ${A C}_{ω}$ and the three finite oriented knot diagrams described above.

[F1]

Each crossing is replaced by the unique orientation-compatible noncrossing smoothing, giving finitely many oriented Seifert circles. (Seifert smoothing and Seifert circles of an oriented link diagram)

[F2]

The algorithm smooths every crossing once, records one disk per circle and one band per crossing. (Seifert disk-and-band construction from an oriented knot diagram)

[F3]

For a one-component diagram, the realized surface is connected, oriented, embedded, and has one boundary component equal to the knot. (Seifert disks and bands form an embedded oriented spanning surface)

[F4]

A connected one-boundary disk-and-band surface with $s$ disks and $c$ bands has genus $(1 - s + c) / 2$ , and its knot genus is at most that value. (Euler characteristic and genus of a Seifert disk-and-band surface)

[F5]

Knot genus is the minimum genus of an admissible Seifert surface, so every such surface gives an upper bound. (Seifert surfaces and smooth knot genus)

[F6]

Under ${A C}_{ω}$ , a connected compact oriented surface with $b$ boundary circles satisfies $χ = 2 - 2 g - b$ . (Finite surface normal forms, Jordan disks, and torsion control)

[F7]

The elementary half twist at adjacent positions has endpoint permutation the corresponding transposition, and its opposite is the inverse half twist. (The elementary geometric half twist, its support disc, and its opposite)

[F8]

Endpoint permutations multiply under braid stacking, and the standard closure has one component for each cycle of that permutation. (The isotopy classes of geometric braids based at $Q$ form a group, and the endpoint permutation is a homomorphism, The closure of a geometric braid)

[A1]

The Axiom of Countable Choice is the sequence principle stated in the item. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

Verification

1.1givenF1F2F7F8algebra

The word $σ_{1}^{3}$ has three crossings, and its endpoint permutation is $(12)^{3} = (12)$ by [F7] and [F8], so its closure is one knot component. Smoothing each braid crossing continues its oriented strand to the adjacent lower segment, leaving the identity two-strand closure with two cycles; hence $c = 3$ and $s = 2$ .

1.2givenF1F2F7F8algebra

The word $σ_{1} σ_{2}^{- 1} σ_{1} σ_{2}^{- 1}$ has four crossings. Since $σ_{i}$ and $σ_{i}^{- 1}$ both induce the adjacent transposition, its endpoint permutation is $(12) (23) (12) (23)$ , a $3$ -cycle; [F8] therefore makes its closure one knot component. Smoothing each crossing straightens its adjacent oriented strands, leaving the identity three-strand closure with three cycles. Hence $(s, c) = (3, 4)$ .

1.3givenF1algebra

The kinked unknot diagram has one crossing; its oriented smoothing separates the small kink loop from the remaining circle, so $(s, c) = (2, 1)$ . In the zero-crossing boundary case, the round unknot has one smoothing circle and no bands, so $(s, c) = (1, 0)$ .

2.1F3F4F5F6F8A1step 1.1step 1.2step 1.3algebra∎

By [F3], all three outputs are connected oriented spanning surfaces. Applying [F4] gives $(1 - 2 + 3) / 2 = 1$ , $(1 - 3 + 4) / 2 = 1$ , and $(1 - 2 + 1) / 2 = 0$ . For the round unknot the disk surface has genus $0$ , and all surface genera are nonnegative by [F6]; therefore its minimum is exactly $0$ . For the trefoil and figure-eight, [F5] yields only the upper bound $g (K) \leq 1$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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.1–3.2, pp.21–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)