Papers With

← All papers
First page of Discriminant Varieties for Stick Knots and Links

Discriminant Varieties for Stick Knots and Links

Alexander Kolpakov, Igor Rivin

math.GT Aug 2, 2026 · v1 math.AG math.AT
formalization geometry combinatorics
Read PDF arXiv abstract
TL;DR
A Lean 4 development verifies the algebraic and finite-combinatorial core of the stick-knot chamber bounds, taking topological inputs as named hypotheses.
Abstract
How many knot types can be built from a fixed budget of straight sticks? We prove that the answer has factorial-scale growth, settling its order for the first time. No previously published general upper bound improves on the exponential-in-the-square estimate obtained from crossing-number enumeration; we replace it with a factorial-scale upper bound, which is optimal at the level of growth order. The proof turns polygonal self-intersection into a sparse real-algebraic chamber problem in only linearly many dimensions, while a complementary braid construction supplies factorially many distinct knots. The result creates a direct bridge between knot topology, real algebraic geometry, fewnomial structure, and permutation combinatorics.
Problem

Determine the growth order of the number of knot types realizable with a fixed budget of N straight sticks. No prior general upper bound improved on an exponential-in-the-square estimate.

Approach

Polygonal self-intersection is recast as a sparse real-algebraic chamber problem in linearly many dimensions using a normalized Stiefel parameter space and determinantal crossing walls. Sign-condition bounds give a factorial-scale upper bound, while a braid construction using Garside normal forms and doubly alternating permutations supplies a matching lower bound. A Lean 4 development checks the algebraic identities, the binomial sign-condition estimate, a finite Cauchy–Schwarz step, and the final arithmetic, conditional on named topological and combinatorial hypotheses.

Results

The number of knot types has factorial-scale growth, log|K_N| = Θ(N log N), with upper bound C_N ≤ 2(AN)^{3N-12} = N^{3N+o(N)} and lower bound |K_N| ≥ N^{(2/3+o(1))N}. The headline asymptotic theorem is not formalized end-to-end in Lean.