we-solve (beta)

Math-2328 · mathematics · Algebraic geometry

Higher-Dimensional Cancellation for Affine Domains

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Let $k$ be algebraically closed and let $A$ be a finitely generated $k$-domain of dimension $d>2$. If adjoining $m>0$ polynomial variables gives $A[t_1,\ldots,t_m]\cong k[x_1,\ldots,x_{m+d}]$, must $A$ already be a polynomial ring in $d$ variables over $k$?

Formulation references: [S1], [S2].

Short English statement

Let $k$ be algebraically closed and let $A$ be a finitely generated $k$-domain of dimension $d>2$. If adjoining $m>0$ polynomial variables gives $A[t_1,\ldots,t_m]\cong k[x_1,\ldots,x_{m+d}]$, must $A$ already be a polynomial ring in $d$ variables over $k$?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

Math-2328-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2328

Manuscript 1 (family 047, 2026-09-23): The explicit finite-type complex domain has d=4 and A[w] is the polynomial ring in five variables while A is not polynomial. This is exactly a permitted algebraically closed-field example with m=1 and d>2, so it disproves the universal cancellation implication.

Higher-Dimensional Cancellation for Affine Domains

OpenAI's claim

An explicit complex affine fourfold is claimed to become affine five-space after one stabilization while itself failing to be affine four-space, with stable-coordinate and nontrivial affine-fibration consequences. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
In $P=\mathbb C[p,s,u,F,J]$, define \[ x=s^2+u^3+p^2F,\qquad H=x^2F-(1+2sx)J-p^2J^2-pu,\qquad A=P/(H). \] OpenAI claims that $A$ is integral of dimension four and for an independent variable $w$, \[ A[w]\simeq\mathbb C^{[5]},\qquad A\not\simeq\mathbb C^{[4]}. \] The notation $\mathbb C^{[j]}$ denotes a polynomial algebra in $j$ variables. It also claims that $H$ is a coordinate of $P[w]$ but not of $P$, where coordinate means an element belonging to a polynomial coordinate system. These assertions give one-variable cancellation and stable-coordinate counterexamples in the indicated dimensions. Writing $X=\operatorname{Spec}A$, the affine-fibration corollary claims that \[ \pi:X\to\mathbb A^1,\quad x\mapsto p(x),\qquad \rho:\mathbb A^5\to\mathbb A^2,\quad z\mapsto(p(z),H(z)) \] are smooth and surjective with relative dimension three; every fiber over a base point $y$ is $\mathbb A^3_{\kappa(y)}$, yet neither map is locally a product with $\mathbb A^3$ in the Zariski topology. Thus the examples satisfy faithful flatness and geometric integrality of the fibers.

Outline of the argument

Manuscript 1 (family 047, 2026-09-23): A locally nilpotent derivation and an explicit inverse polynomial change give the cylinder isomorphism. To obstruct cancellation, a valuation along the exceptional parameter computes the associated graded affine modification; the resulting rigidity distinguishes the original coordinate ring from a polynomial algebra.

Formal verification

For family 047, the scope page documents the following selections. The selected construction is a four-dimensional complex domain whose one-variable polynomial extension is a five-variable polynomial ring, while the original ring is not polynomial. The other affine-fibration and stable-coordinate consequences are separate. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ComplexCancellation.lean. Declarations: OAI.ComplexCancellation.main.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →