ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-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.

Trefoil Seifert matrix and basis changes

Example

Assume the Axiom of Choice and take the genus-one Seifert surface for the trefoil described as $K_{1}$ in Cattabriga–Francaviglia, Example 6.2.11. In their basis $f_{1}, f_{2}$ , their negative-first Seifert form has matrix $A = (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array})$ , and they identify $K_{1}$ as the trefoil. Their convention is $α (x, y) = lk (x^{-}, y)$ ; the positive-first convention here is $θ (x, y) = lk (x^{+}, y)$ . In the swapped basis $a_{1} = f_{2}$ , $a_{2} = f_{1}$ , the positive-first Seifert matrix is

V = (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array}), V - V^{T} = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array}), \det (V - t V^{T}) = 1 - t + t^{2} .

The determinant-one basis change $P_{0} = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ gives $P_{0}^{T} V P_{0} = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ . It changes the off-diagonal entries but not the diagonal entries. The determinant-one basis change $P_{1} = (\begin{array}{cc} 1 & 1 \\ 2 & 3 \end{array})$ gives $P_{1}^{T} V P_{1} = (\begin{array}{cc} 3 & 5 \\ 4 & 7 \end{array})$ , changing every entry. For either $P$ , the transformed Alexander presentation matrix is $P^{T} (V - t V^{T}) P$ , so it presents an isomorphic $Λ$ -module.

Example references

Cattabriga–Francaviglia, Example 6.2.11 and Theorem 6.2.9

The positive-push convention used for $V$

The matrix presentation of the one-variable Alexander module

Facts & Assumptions

Given: Full AC, the cited genus-one oriented trefoil surface, its negative-first matrix in the source basis, and the positive-first convention of this run.

[A1]

Full AC supplies the choice hypotheses of the Seifert-surface and normal-form interfaces. The Axiom of Choice, AC implies DC implies countable choice

[F1]

The source's genus-one example gives $A = (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array})$ for $α (x, y) = lk (x^{-}, y)$ and identifies its $K_{1}$ as a trefoil. Cattabriga–Francaviglia, Example 6.2.11, printed p. 45

[F2]

The positive-first matrix is defined by $V_{i j} = lk (a_{i}^{+}, a_{j})$ , linking is symmetric, and moving both curves through a disjoint collar preserves linking. Seifert pairing and matrix of an oriented knot, Well-definedness of the Seifert pairing

[F3]

For an integral basis change $P$ , the new Seifert matrix is $P^{T} V P$ and the Alexander presentation matrix is $V - t V^{T}$ . Seifert matrices of ambient-isotopic pairs are S-equivalent, A Seifert matrix presents the one-variable Alexander module

Proof

1.1A1F1F2givenalgebra

Under [A1], apply the Seifert-pairing convention to the source's supplied oriented surface and basis. In the original source basis, $A_{i j} = lk (f_{i}^{-}, f_{j})$ . By symmetry and a simultaneous positive normal translation, this equals $lk (f_{j}^{+}, f_{i})$ , which is the $(j, i)$ entry of the positive-first matrix in the same basis. Thus that matrix is $A^{T}$ . Let $S = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ be the basis swap. Then $S^{T} A^{T} S = A$ , so the positive-first matrix in the swapped basis is the displayed $V$ .

2.1F2F3step 1.1algebra

Direct multiplication gives $V - V^{T} = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ . Also $V - t V^{T} = (\begin{array}{cc} 1 - t & t \\ - 1 & 1 - t \end{array})$ , whose determinant is $(1 - t)^{2} + t = 1 - t + t^{2}$ . The skew-part identity agrees with the oriented genus-one handle intersection block in the stated positive-normal convention.

2.2F3step 1.1algebra

For $P_{0}$ , $V P_{0} = (\begin{array}{cc} 1 & 1 \\ - 1 & 0 \end{array})$ and $P_{0}^{T} (V P_{0}) = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ . For $P_{1}$ , $V P_{1} = (\begin{array}{cc} 1 & 1 \\ 1 & 2 \end{array})$ and $P_{1}^{T} (V P_{1}) = (\begin{array}{cc} 3 & 5 \\ 4 & 7 \end{array})$ . Both determinants are $1$ , so both are integral basis changes; the second matrix differs from $V$ in all four entries.

3.1F3step 2.1step 2.2algebra∎

For either unimodular $P$ , $(P^{T} V P) - t (P^{T} V^{T} P) = P^{T} (V - t V^{T}) P$ . Right multiplication by $P$ does not change the image of the map on $Λ^{2}$ , and left multiplication by the automorphism $P^{T}$ identifies the two cokernels. The module presentation is therefore independent of these basis changes, as asserted.

Remarks

The following schematic is the closure of a two-strand braid with three crossings. Gaps mark under-strands and the uninterrupted local arc at each crossing is the over-strand. It identifies the knot picture only; the matrix and determinant calculations above use the cited source matrix and the explicit convention translation in step 1.1.

\begin{tikzpicture}[scale=0.85,>=stealth]
  \draw[thick] (-1,3)--(-1.35,2.8).. controls (-1.55,2) and (-1.55,1) ..(-1.35,0.2)--(-1,0);
  \draw[thick] (1,3)--(1.35,2.8).. controls (1.55,2) and (1.55,1) ..(1.35,0.2)--(1,0);
  \draw[thick] (-1,3)--(0,2.5)--(1,2)--(0,1.5)--(-1,1)--(0,0.5)--(1,0);
  \draw[thick] (1,3)--(0,2.5)--(-1,2)--(0,1.5)--(1,1)--(0,0.5)--(-1,0);
  \draw[white,line width=4pt] (0.28,2.64)--(-0.28,2.36);
  \draw[thick] (-0.28,2.64)--(0.28,2.36);
  \draw[white,line width=4pt] (0.28,1.64)--(-0.28,1.36);
  \draw[thick] (-0.28,1.64)--(0.28,1.36);
  \draw[white,line width=4pt] (0.28,0.64)--(-0.28,0.36);
  \draw[thick] (-0.28,0.64)--(0.28,0.36);
  \node at (0,3.35) {$\text{two braid strands}$};
  \node at (0,-0.35) {$\text{three crossings; closure arcs at the sides}$};
\end{tikzpicture}

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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

Dale Rolfsen, Knots and Links, Chapter 8.A–8.B (standard reference, not scraped)
Alessia Cattabriga and Stefano Francaviglia, Knot Theory and Applications: Lecture Notes, Example 6.2.11 and Theorem 6.2.9 (standard reference, not scraped)