# Zariski cancellation and affine fibrations over the complex numbers

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An explicit failure of complex affine-space cancellation](../../preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf)

## Scope

Affine-space cancellation asks whether $X\times\mathbb A^1\cong\mathbb A^{n+1}$ forces $X\cong\mathbb A^n$. The formalized result gives an explicit finite-type complex domain $A$ of Krull dimension four with $A[w]\cong\mathbb C[x_1,\ldots,x_5]$ but $A\not\cong\mathbb C[x_1,\ldots,x_4]$. Thus adjoining one variable erases a genuine algebraic distinction.

The separate stable-coordinate and general line-bundle lifting consequences are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Complex affine-space cancellation counterexample | [ComplexCancellation.lean](../ComparatorChallenges/ComplexCancellation.lean) |