Finite generation of one-parameter polynomial Vassiliev algebras

E. Lanina and A. Sleptsov, Algebraic structures of Vassiliev invariants for knot families, arXiv:2508.02385v2, Nuclear Physics B 1022 (2026), 117268, conjecture in the abstract (main.tex, line 165):

We conjecture that such 1-parametric algebra of Vassiliev invariants is always finitely generated, while in the case of more parameters, we provide example of the knot family with infinite number of generators.

Section 4.1, “Generic one-parametric family” (main.tex, line 1166), asks:

Can this force such a 1-parametric algebra of Vassiliev invariants to be infinitely generated? Examples and reasonings provide the intuition that a 1-parametric algebra of polynomial Vassiliev invariants always has only a finite number of generators. Still, we currently lack strict mathematical proof.

The source restricts attention to rational-valued invariants (main.tex, line 350), defines primary invariants as generators of the algebra restricted to a family (line 356), and represents the one-parameter restrictions by polynomials with rational coefficients (lines 1114–1117). These passages are recorded in the literature note.

Issue #22008 fixes the algebraic reading: for every index type $\iota:\mathrm{Type}$ and every family $p:\iota\to\mathbb Q[X]$, there is a finite set $s$ of indices such that

$\mathbb Q[p_i\mid i\in s]=\mathbb Q[p_i\mid i:\iota]$.

Here $\mathbb Q[S]$ denotes the smallest rational subalgebra containing $S$. Thus the generators can be chosen from the original family of restricted invariants. This is the statement of claim, proved by result.

The source's primary invariants generate the descended algebra: every restricted invariant is a polynomial in them. Finite generation would replace the full family of rational polynomial restrictions by finitely many of those restrictions. The source contrasts this question for one parameter with its infinitely generated two-parameter example. The distinction concerns algebra generation; it does not by itself determine whether the invariants distinguish knots or recover a family parameter.

Issue #22008 records a bounded literature check: the v2 source explicitly leaves the proof missing; a search for the authors with “finitely generated” found only the source; Crossref, OpenAlex and INSPIRE were reported to list zero citations; and MathDB and formal-conjectures were reported to have no match. The external search readings are not independently reproduced here.

not-found-in-searched-scope.

The general finiteness theorem for subalgebras of a polynomial ring in one variable over a field is classical commutative algebra, obtained from the Artin–Tate lemma. The settlement identifies the published conjecture as a consequence of that theorem; it does not claim a new general commutative-algebra theorem.

The lemma names below belong to D5.S3.Topology.KnotFamilyVassilievFiniteGeneration; the helper lemmas are private. Throughout the general argument, $k$ is a field and $a$ is a $k$-subalgebra of $k[X]$.

1. The constant case (fg_of_constant). Under the hypothesis that every $f\in a$ has natural degree zero, each such polynomial is the constant polynomial with its zeroth coefficient. Hence $a$ is the scalar subalgebra, which is generated by the empty set. Natural degree zero includes the zero polynomial.
2. Integrality (integral_X). Given $f\in a$ with $0<\operatorname{natDegree}(f)$, its leading coefficient $c$ is nonzero. The polynomial $q=c^{-1}f$ is monic of positive degree and belongs to $a$. Mapping its coefficients from $k$ into $a$ gives a monic polynomial whose evaluation at $X$ is the image of the element $q\in a$, hence is integral over $a$. The monic evaluation criterion gives that $X$ is integral over $a$. Equivalently, with a new indeterminate $T$, the monic polynomial $c^{-1}(f(T)-f(X))$ over $a$ vanishes at $X$.
3. Module finiteness (finite_of_integral_X). Under the hypothesis that $X$ is integral over $a$, the $a$-subalgebra generated by $X$ is all of $k[X]$, and the integral singleton generates a finite $a$-module. Thus $k[X]$ is a finite $a$-module.
4. Artin–Tate (fg_of_finite, subalgebra_fg). Given that $k[X]$ is a finite $a$-module, fg_of_finite applies Mathlib's Algebra.fg_of_fg_of_fg to $k\to a\to k[X]$: the base field is Noetherian, $k[X]$ is a finitely generated $k$-algebra, and the inclusion of $a$ is injective. It concludes that $a$ is finitely generated over $k$. The constant case and the case with a positive-degree member exhaust all $a$, giving subalgebra_fg for every field $k$ and every $k$-subalgebra of $k[X]$.
5. A finite original subfamily (finite_subfamily, result). For any index type $\iota$, any $p:\iota\to k[X]$, and the hypothesis that $k[\operatorname{range}p]$ is finitely generated, finite_subfamily gives a finite set of indices generating that algebra. Its membership induction applies to each $x\in k[\operatorname{range}p]$: an original value uses a singleton, a scalar uses the empty set, and a sum or product uses the union of the two finite supports. Taking the union of these supports over a finite algebra-generating set gives the required finite index set. result specializes to $k=\mathbb Q$ and uses subalgebra_fg to discharge the finite-generation hypothesis, for every $\iota:\mathrm{Type}$ and $p:\iota\to\mathbb Q[X]$.

The classical input is E. Artin and J. T. Tate, A Note on Finite Ring Extensions (1951), DOI 10.2969/jmsj/00310074; see the Artin–Tate literature note and Mathlib's Mathlib/RingTheory/Adjoin/Tower.lean. The univariate subalgebra theorem is attributed to this commutative-algebra route, not to Lanina–Sleptsov.

The settlement would miss the conjecture if the descended algebra were not generated by rational polynomial restrictions in one parameter, if generation had to preserve the order filtration, or if only arbitrary polynomial generators rather than original invariant restrictions were obtained.

The source supplies the rational-polynomial premise and uses ordinary generation: its twist-knot discussion (main.tex, line 1228) says that the second invariant “generates all Vassiliev invariants for the whole family of twist knots.” The finite set in claim consists of indices of the supplied family itself. The module does not define knots, construct their invariants, or establish polynomiality for a knot family; those are the source-to-algebra correspondence, not hypotheses proved by result.

The canonical source is D5/S3/Topology/KnotFamilyVassilievFiniteGeneration.lean (119 lines).

• Proof. It proves result : claim.
• General theorem. It also proves subalgebra_fg: for every field $k$ and every $k$-subalgebra $a$ of $k[X]$, a.FG. Here Subalgebra.FG means that a finite set of polynomials generates $a$ as a $k$-subalgebra.
• Reuse. The Artin–Tate lemma is Mathlib's Algebra.fg_of_fg_of_fg; its literature attribution is Artin–Tate (1951), as recorded above.
• Axioms. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.
• Open registration. The §3.9 registration of subalgebra_fg is unresolved in issue #22051.

Frozen state: Golden/Frozen/state/D5/S3/Topology/KnotFamilyVassilievFiniteGeneration.lean.json, statement sha256:3cb341ce66439691985ef87ce57b7a82aa668e7a2dfe929233b02b68560a4bb4.

Declaration statements:

• result: sha256:801a9fa0c4905afaad0631c3d5c510f7e133a0e12402c0f82dc514faa339187e;
• claim: sha256:3c7c62610e4bc6e74916694a67ae7c98f501aa1ab0a6d1fe62c9aa58b1f5de5f.

Tier 1 conjecture in a 2026 journal article, preregistered in issue #22008 before any Lean. theorem; resolution proved.

The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2. There is no digestion atom.

What the settlement shows

Proved by result: for every index type $\iota:\mathrm{Type}$ and every family $p:\iota\to\mathbb Q[X]$, there exists a finite set $s$ of indices such that the rational subalgebra generated by the values $p_i$ with $i\in s$ equals the rational subalgebra generated by all values of $p$.

Computed, not formalized: no numerical or symbolic experiments are used.

Argued, not formalized:

• The knot-family bridge. Suppose every invariant under consideration restricts to a rational polynomial $p_i(n)$ on the same one-parameter family. Evaluation on its parameter set preserves scalars, sums and products. Applying that homomorphism to the equality in result shows that every restricted invariant is a polynomial in finitely many original restricted invariants. This implication needs no injectivity of evaluation; for an infinite set of rational parameter values the usual polynomial root bound additionally identifies polynomial representatives uniquely. The identification of the source's invariant algebra with this evaluation image is not formalized.
• Decisive mechanism and scope. For a field $k$ and a subalgebra $a\subseteq k[X]$ containing $f$ of positive natural degree, integral_X makes $X$ integral over $a$; with that integrality hypothesis, finite_of_integral_X makes $k[X]$ a finite $a$-module; with that module-finiteness hypothesis, fg_of_finite makes $a$ finitely generated. The separate compiled theorem subalgebra_fg includes every field, without a characteristic-zero assumption. At the rational-family level, result imposes no nonvanishing, algebraic-independence, growth, or order-degree condition on $p$; constant, zero and empty families are included. The application therefore does not require the source's genericity assumptions or growth heuristic.
• Finite generation need not mean one generator. Consider the algebraic example $A=\mathbb Q[X^2,X^3]$. Every nonconstant element of $A$ has degree at least two. If $A=\mathbb Q[g]$, then $g$ is nonconstant, and the degrees of $X^2$ and $X^3$, being polynomials in $g$, are both positive multiples of $\deg g$. This forces $\deg g=1$, a contradiction. This is an argument about a polynomial algebra, not a claimed knot-family realization. Neither a minimal number of invariant generators nor a bound on their orders is supplied by result.
• One variable is a substantive boundary. The analogous assertion for arbitrary subalgebras of $\mathbb Q[X,Y]$ has the algebraic obstruction $B=\mathbb Q[X,XY,XY^2,\ldots]$. Every element of $B$ has a constant term plus terms divisible by $X$. From any putative finite algebra-generating set subtract its constants. Products of two resulting generators are divisible by $X^2$, so the coefficients of $X$ in the generated algebra lie in the finite-dimensional rational span of the generators' coefficients of $X$. But $B$ contains every $XY^j$, whose coefficients of $X$ are the linearly independent polynomials $Y^j$. This gives an obstruction to finite generation in two variables. It is not a verification of the paper's two-parameter knot example.
• Effect on the source's further statements. For one-parameter families satisfying the rational-polynomial premise, the finiteness of primary generators discussed in Section 4, the one-parameter part of Section 6, and the Conclusion follows via the evaluation argument above, including degenerate families with vanishing low-order invariants. The explicit generator counts and order cutoffs in Section 4.1 require their own hypotheses and arguments. Finite generation does not imply recovery of the parameter: $\mathbb Q[X^2]$ contains only even powers and does not contain $X$. Thus the “Complete invariant” discussions require a separate parameter-recovery or separation argument; the general completeness conjecture for Vassiliev invariants is not settled. The paper's two-parameter infinite-generation example and its question about fewer than $k$ algebraically independent invariants in a $k$-parameter knot family are also outside this settlement.

The literature check is bounded and does not establish exhaustive worldwide novelty or priority. The citation counts, keyword-search coverage, MathDB search, formal-conjectures search, and repository-search reading reported in #22008 are not independently reproduced. The v1 comparison reported there is not checked against v1 here. The v2 conjecture and the cited rationality, polynomiality and generation passages are checked directly in main.tex, together with the relevant discussions in Sections 4–6 and the Conclusion.

The source-to-knot interpretation, actual polynomiality and formulas for knot invariants, generator counts and order cutoffs, parameter recovery and knot separation, multivariate knot examples, and the arguments in “Argued, not formalized” are not formalized by this module. The interior of Artin–Tate's 1951 paper is not read here; its attribution uses the literature note and the pinned Mathlib statement and references. The registration readouts reported in #22051 are not independently reproduced; the registration of subalgebra_fg remains open there. No Blueprint emission or repository-wide check is claimed.