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.
Normal-surface unknot recognition examples
1 · Prerequisites
- Abelian Categories
- Asymptotic Cones and the Sublinear Triangle Criterion
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Chain Complexes and Homology
- Chain Homotopy and the Homotopy Category
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Crossing signs, writhe, and linking number
- Cw Complexes and Cellular Homology
- Determinants of Matrices over a Commutative Ring
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Exactness and the Member Calculus
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Function Space Topologies and the Exponential Law
- Geometric Braids and Artin Generators
- Graphs, Walks and Connectivity
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hereditary and Productive Behaviour of the Separation Axioms
- Homotopy and Homotopy Equivalence
- Limits and Colimits
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Long Exact Sequences in Homology
- Manifolds with Boundary Collars and Orientations
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normal-surface unknot recognition
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Oriented Links, Braid Closures, and Markov Equivalence
- Planar-diagram codes and knot-table enumeration
- Plane Graphs, Euler's Formula and the Five Colour Theorem
- Polynomial Rings, the Division Algorithm and Roots
- Preadditive and Additive Categories and Biproducts
- Properties of the Integral and the Working FTC
- Rank Theorems and Embedded Submanifolds
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Relative Homology Excision and Mayer Vietoris
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sard Theorem and Transversality
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Simplicial Complexes and Simplicial Homology
- Simplicial Subdivision and Simplicial Approximation
- Singular Chains and Singular Homology
- Smooth Manifolds and Smooth Maps
- Smooth Vector Bundles and Sections
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tensor Fields Exterior Algebra and Differential Forms
- Tensor Products of Modules
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Diagram Lemmas in an Abelian Category
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Trees, Forests and Spanning Trees
- Universal Properties, Representables and the Yoneda Lemma
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Logical flowchart
3 · Definitions, theorems and proofs
None yet.
4 · Examples, counterexamples and false statements
A boundary-parallel disk fails the meridian test
Statement refuted
Every connected admissible normal surface in a finite triangulated knot exterior with nonempty boundary and Euler characteristic one passes the odd-meridian-intersection test for an essential normal disk.
Statement references
Normal-surface coordinates and the Haken cone — normal vertex-link triangles and normal-coordinate conventions.
Finite normal-coordinate tests characterize essential disk candidates — the essential-boundary test in the normal-disk filter.
Hass–Lagarias–Pippenger, Lemma 4.2 and §5 — disk recognition and the meridian-intersection condition.
Erickson, “Normal Surfaces and Knots,” §§14.2–14.4 — boundary-parallel disks and normal-surface filtering.
Facts & Assumptions
Given: A finite simplicial triangulation of a compact knot exterior with torus boundary and a marked meridian curve in its boundary triangulation.
Let be any finite simplicially triangulated knot exterior with boundary torus and marked meridian . For a boundary vertex , its normal link is a properly embedded boundary-parallel disk: its boundary is the link of in , a contractible simple closed curve. The link is connected, has nonempty boundary and Euler characteristic one, but its boundary has even mod-two intersection with , so the normal-surface filter rejects this candidate. Rejecting this one boundary-parallel disk does not determine whether the knot is nontrivial.
Normal-surface coordinates and the Haken cone: a normal surface meets each tetrahedron in a union of triangle and quadrilateral disks, and its face arcs match. In a simplicial triangulation of a PL -manifold, the link of a boundary vertex is a triangulated disk.
Finite normal-coordinate tests characterize essential disk candidates: an admissible vector is an essential disk candidate exactly when it is connected, has nonempty boundary, Euler characteristic one, and odd mod-two meridian intersection.
Counterexample
The link of a boundary vertex in a triangulated -manifold is a closed disk: its local link is a -ball. In each tetrahedron containing the link meets that tetrahedron in the small triangle parallel to the opposite face; it misses tetrahedra not containing . Across each shared face these triangles have matching normal arcs, so [F1] makes the link a normal surface. Its boundary is , a simple closed curve in the small boundary-star disk of , hence contractible in . The local half-ball star shows the disk is boundary-parallel.
The link disk is connected, has nonempty boundary, and has Euler characteristic one. Its boundary is null-homotopic, so its projection to the product-circle factor has degree zero. After a transverse PL perturbation, the parity of intersections with a fibre meridian equals the parity of preimages of a regular point under that projection; a lift with zero net degree crosses the level an even number of times. Hence the intersection parity is zero.
The disk therefore passes the first three tests in [F2] but fails the odd-intersection test, so the filter rejects this candidate. This conclusion concerns this boundary-parallel disk only; it does not rule out any other normal essential disk in and therefore does not classify the knot.
Worked case: a normal disk in the zero-crossing unknot exterior
Example
For the crossingless oriented unknot code, triangulate its solid-torus exterior by triangulating as one triangle with vertices and as the three-edge cycle . In the prism over , write and and use the tetrahedra The properly embedded normal disk at the midpoint of meets in the triangle cutting off , in the quadrilateral separating from , and in the triangle cutting off ; every other normal coordinate is zero. It is connected, has nonempty boundary and Euler characteristic one, and its boundary meets the marked original meridian once mod two.
\begin{tikzpicture}[scale=1]
\coordinate (A0) at (0,0); \coordinate (A1) at (2,0); \coordinate (A2) at (1,1.5);
\coordinate (B0) at (0.6,0.7); \coordinate (B1) at (2.6,0.7); \coordinate (B2) at (1.6,2.2);
\draw (A0)--(A1)--(A2)--cycle; \draw (B0)--(B1)--(B2)--cycle;
\draw (A0)--(B0) (A1)--(B1) (A2)--(B2);
\draw[dashed] (A0)--(B1) (A0)--(B2) (A1)--(B2);
\coordinate (M0) at (0.3,0.35); \coordinate (M1) at (2.3,0.35); \coordinate (M2) at (1.3,1.85);
\draw[red,very thick] (M0)--(M1)--(M2)--cycle;
\node[below left] at (A0) {$a_0^0$}; \node[below right] at (A1) {$a_1^0$}; \node[left] at (A2) {$a_2^0$};
\node[left] at (B0) {$a_0^1$}; \node[right] at (B1) {$a_1^1$}; \node[above] at (B2) {$a_2^1$};
\node[red] at (1.35,0.8) {$D^2\times\{s_*\}$};
\end{tikzpicture}
The dashed edges indicate the staircase prism subdivision specified by ; the red section is the geometric disk whose intersections with those tetrahedra give the stated triangle–quadrilateral–triangle vector. The formula for the tetrahedra, not the schematic projection, fixes the exact triangulation.
Example references
Normal-surface coordinates and the Haken cone — triangle and quadrilateral normal disk types.
Linear-size good exterior triangulation from a planar knot code — fixed crossingless solid-torus exterior model and marked meridian path.
Hass–Lagarias–Pippenger, §4 and §5 — unknot exterior and normal disk coordinates.
Facts & Assumptions
Given: The product triangulation of the exterior and its marked meridian path.
Normal-surface coordinates and the Haken cone: a triangle or quadrilateral normal disk meets tetrahedral faces in matching normal arcs; admissibility allows at most one quadrilateral type per tetrahedron.
Linear-size good exterior triangulation from a planar knot code: at zero crossings the exterior is a fixed triangulated solid torus with the original meridian represented by a three-edge fibre cycle.
Verification
For the prism over , write and . Use the staircase tetrahedra Their common faces are triangulated by the same ordered diagonals, so the three tetrahedra form the triangular-prism block; repeating this order on the three-cycle of gives the product triangulation in [F2].
The level disk at the midpoint of the product edge separates the bottom vertices from the top vertices . In it cuts off the single top vertex , giving one triangle; in it separates the pair from , giving one quadrilateral; in it cuts off the single bottom vertex , giving one triangle. It misses all tetrahedra in the other two prism blocks. Its intersections on shared faces agree because they are the same level section of the product, so the matching equations hold. Only one quadrilateral coordinate is nonzero, so [F1] gives an admissible normal disk vector.
The geometric surface is exactly , hence is a connected disk. Its boundary is the nonempty circle . The disk itself has Euler characteristic . The marked meridian passes through exactly one point of this boundary at , in the interior of the chosen fiber edge; the intersection is transverse and has parity .
Thus the explicit vector satisfies the matching, quadrilateral, connectedness, boundary, Euler-characteristic and mod-two meridian checks claimed in the statement.