Jacobian Conjecture: Verification Notebook

This notebook is a self-contained mathematical and computational companion to the Jacobian Conjecture section in the paper.

The task template, including the prompt given to the agents, is available here.

The outline is as follows:

1. Problem Definitions
2. S1. Independent reconstruction through a cuspidal ruling.
3. S2. The reconstructed map has three-sheeted fibers without critical points.
4. Additional findings

The required packages are:

SymPy
IPython

1. Problem Definitions

The Jacobian conjecture asked whether a polynomial map that is locally invertible everywhere must also be globally invertible. More precisely, it asserted that every polynomial map $F\colon\mathbb C^n\to\mathbb C^n$ with nonzero constant Jacobian determinant is a polynomial automorphism. On 19 July 2026, it was announced that a three-dimensional counterexample had been produced with Claude Fable, thereby disproving the conjecture in every dimension at least three. The breakthrough then prompted researchers to seek a conceptual explanation for the map: in particular, why its apparently miraculous Jacobian cancellation occurs and how three generic inverse sheets can coexist with local invertibility everywhere.

The public file construction.json stores the reconstructed map as sparse rational polynomials, its three witness points, and independent finite specializations used later. A term with powers = [i,j,k] means $c x^i y^j z^k$ .

These shared objects are used by all verification cells below. The next cell authenticates the data file and reconstructs the polynomials over the exact rational field.

Show code

Code cell 3 · In [1]

from __future__ import annotations

from fractions import Fraction
from hashlib import sha256
import json
from pathlib import Path

import sympy as sp
from IPython.display import Markdown, display

DATA_PATH = Path("construction.json")
EXPECTED_DATA_SHA256 = "ba0d49ac35c97eb24d0082457d5602a66761344d80db30c722de1ed06eb78e67"

if not DATA_PATH.is_file():
    raise FileNotFoundError(
        "construction.json is required next to verification.ipynb"
    )
actual_hash = sha256(DATA_PATH.read_bytes()).hexdigest()
assert actual_hash == EXPECTED_DATA_SHA256, (actual_hash, EXPECTED_DATA_SHA256)
bundle = json.loads(DATA_PATH.read_text(encoding="utf-8"))
assert bundle["schema_version"] == 1
assert bundle["arithmetic_domain"] == "QQ"

x, y, z, a = sp.symbols("x y z a")

def QQ(value):
    """Parse a public integer or rational string exactly."""
    return sp.Rational(str(value))

def sparse_polynomial(terms, variables=(x, y, z)):
    expression = sp.Integer(0)
    for term in terms:
        coefficient = QQ(term["coefficient"])
        powers = tuple(int(power) for power in term["powers"])
        assert len(powers) == len(variables) and all(power >= 0 for power in powers)
        monomial = sp.Integer(1)
        for variable, power in zip(variables, powers):
            monomial *= variable**power
        expression += coefficient * monomial
    return sp.expand(expression)

def exact_point(values):
    return tuple(QQ(value) for value in values)

def matrix_is_zero(vector):
    return all(sp.expand(entry) == 0 for entry in vector)

public_map = bundle["reconstructed_map"]
F = sp.Matrix([sparse_polynomial(terms) for terms in public_map["polynomials"]])
public_points = [exact_point(item["point"]) for item in public_map["witnesses"]]
public_images = [exact_point(item["image"]) for item in public_map["witnesses"]]

print(f"Authenticated {DATA_PATH.name}: {actual_hash}")
print("Reconstructed map:")
for name, expression in zip(("P", "Q", "R"), F):
    print(f"  {name} = {expression}")

Saved output 1

Authenticated construction.json: ba0d49ac35c97eb24d0082457d5602a66761344d80db30c722de1ed06eb78e67
Reconstructed map:
  P = x**3*z + 9*x**2*y + 6*x
  Q = x**3*y**2*z + 9*x**2*y**3 - 2*x**2*y*z - 12*x*y**2 + x*z + y
  R = x**3*y**3*z + 9*x**2*y**4 - 3*x**2*y**2*z - 21*x*y**3 + 3*x*y*z + 12*y**2 - z

2. S1. Independent reconstruction through a cuspidal ruling.

Theorem 2.1 (exact counterexample certificate).

Let $b=xy-1$ and

F(x,y,z)= \bigl(6x+9x^2y,\;y(9b^2+6b-2),\;3y^2b(3b-1)\bigr) +z\bigl(x^3,\;xb^2,\;b^3\bigr).

Then $F$ has component degrees $(4,6,7)$ , contains $16$ nonzero monomials, and

\det JF=-6.

Moreover, the three distinct rational points

\left(-\frac67,-\frac76,-\frac{4753}{216}\right),\qquad \left(\frac34,\frac73,-\frac{980}{27}\right),\qquad \left(\frac3{28},\frac73,\frac{2548}{27}\right)

all map to $(1,7/3,0)$ .

Proof. Differentiate the three displayed polynomials and expand the determinant in $\mathbb Q[x,y,z]$ . Since the determinant is a nonzero constant, the complex inverse function theorem makes $F$ locally biholomorphic everywhere. Since a polynomial automorphism is injective, the displayed collision proves that $F$ has no polynomial inverse. $\square$

Corollary 2.2 (all dimensions at least three).

The Jacobian conjecture fails in every dimension $n\geq3$ .

Proof. Theorem 2.1 gives dimension three. For $n>3$ , append $n-3$ unchanged coordinates to $F$ . The new Jacobian matrix is block diagonal with blocks $JF$ and $I_{n-3}$ , so its determinant remains $-6$ . The same collision persists when the appended coordinates are equal. $\square$

The next cell checks the determinant, degrees, term count, and three rational preimages exactly.

Show code

Code cell 5 · In [2]

jacobian = F.jacobian((x, y, z))
determinant = sp.expand(jacobian.det())
degrees = tuple(sp.Poly(component, x, y, z).total_degree() for component in F)
term_counts = tuple(len(sp.Poly(component, x, y, z).terms()) for component in F)
images = [
    tuple(sp.expand(component.subs(dict(zip((x, y, z), point)))) for component in F)
    for point in public_points
]

expected = public_map["expected"]
assert determinant == QQ(expected["jacobian_determinant"]) == -6
assert degrees == tuple(expected["component_degrees"]) == (4, 6, 7)
assert term_counts == tuple(expected["component_term_counts"]) == (3, 6, 7)
assert sum(term_counts) == expected["total_terms"] == 16
assert len(set(public_points)) == 3
assert images == public_images
assert len(set(images)) == 1
assert images[0] == exact_point(expected["common_image"]) == (1, QQ("7/3"), 0)
assert jacobian.subs({x: 0, y: 0, z: 0}) == sp.diag(6, 1, -1)



rows = [
    f"| $({sp.latex(point[0])},{sp.latex(point[1])},{sp.latex(point[2])})$ "
    f"| $({sp.latex(image[0])},{sp.latex(image[1])},{sp.latex(image[2])})$ |"
    for point, image in zip(public_points, images)
]
display(Markdown(
    "| Rational source point | Exact image |\n|---|---|\n" + "\n".join(rows)
))
print("det(JF) =", determinant)
print("component degrees =", degrees, "; term counts =", term_counts)

Saved output 1

Rational source point	Exact image
$(- \frac{6}{7},- \frac{7}{6},- \frac{4753}{216})$	$(1,\frac{7}{3},0)$
$(\frac{3}{4},\frac{7}{3},- \frac{980}{27})$	$(1,\frac{7}{3},0)$
$(\frac{3}{28},\frac{7}{3},\frac{2548}{27})$	$(1,\frac{7}{3},0)$

Saved output 2

det(JF) = -6
component degrees = (4, 6, 7) ; term counts = (3, 6, 7)

2.1 Linear equivalence to the announced map

Theorem 2.3 (exact source–target equivalence).

Let $H=(H_1,H_2,H_3)$ be the publicly announced map

\begin{aligned} H_1&=(1+xy)^3z+y^2(1+xy)(4+3xy),\\ H_2&=y+3x(1+xy)^2z+3xy^2(4+3xy),\\ H_3&=2x-3x^2y-x^3z. \end{aligned}

Define the invertible linear maps

T(x,y,z)=(x,-y,-3z),\qquad L(A,B,C)=(3C,-B,3A).

Then

F\circ T=L\circ H.

Proof. Substitute $(x,-y,-3z)$ into each component of $F$ , expand, and compare with $(3H_3,-H_2,3H_1)$ . The three polynomial differences vanish identically. Because $T$ and $L$ are invertible, this is an equivalence by rational-linear source and target changes. The determinant calculation is consistent:

\det JF=\frac{\det L\,\det JH}{\det T} =\frac{9(-2)}3=-6.

$\square$

The next cell verifies the source–target equivalence, the announced map’s determinant, and its published triple collision by exact calculation.

Show code

Code cell 7 · In [3]

one = sp.Integer(1)
H = sp.Matrix([
    (one + x*y)**3*z + y**2*(one + x*y)*(4 + 3*x*y),
    y + 3*x*(one + x*y)**2*z + 3*x*y**2*(4 + 3*x*y),
    2*x - 3*x**2*y - x**3*z,
])
F_after_T = sp.Matrix([component.subs({x: x, y: -y, z: -3*z}, simultaneous=True) for component in F])
L_after_H = sp.Matrix([3*H[2], -H[1], 3*H[0]])
equivalence_residual = sp.Matrix([sp.expand(left-right) for left, right in zip(F_after_T, L_after_H)])

T_matrix = sp.diag(1, -1, -3)
L_matrix = sp.Matrix([[0, 0, 3], [0, -1, 0], [3, 0, 0]])
det_H = sp.expand(H.jacobian((x, y, z)).det())
assert matrix_is_zero(equivalence_residual)
assert T_matrix.det() == 3 and L_matrix.det() == 9
assert det_H == -2
assert determinant == sp.cancel(L_matrix.det() * det_H / T_matrix.det())

H_points = [
    (0, 0, QQ("-1/4")),
    (1, QQ("-3/2"), QQ("13/2")),
    (-1, QQ("3/2"), QQ("13/2")),
]
H_images = [tuple(sp.expand(component.subs(dict(zip((x, y, z), point)))) for component in H) for point in H_points]
assert len(set(H_points)) == 3 and len(set(H_images)) == 1
assert H_images[0] == (QQ("-1/4"), 0, 0)


print("F(T(x,y,z)) - L(H(x,y,z)) =", tuple(equivalence_residual))
print("det(T), det(L), det(JH), det(JF) =", T_matrix.det(), L_matrix.det(), det_H, determinant)

Saved output 1

F(T(x,y,z)) - L(H(x,y,z)) = (0, 0, 0)
det(T), det(L), det(JH), det(JF) = 3 9 -2 -6

Station Reference. Research Center Eval #114 supplies the reconstructed map, witness points, and exact certificate.

Related Work. The conjecture originates with Keller (1939). The reductions of Bass, Connell, and Wright (1982), Yagzhev (1980), and Drużkowski (1983) reduce it to cubic normal forms. Wang (1980) proved the degree-two case, and Moh (1983) proved the two-variable case through degree $100$ . The two-dimensional characteristic-zero case remains open; in characteristic $p$ , the map $x\mapsto x-x^p$ already has derivative $1$ without being injective. Van den Essen (2000) surveys the classical theory. Alpöge (2026) announced the counterexample before this run, and Freitas Ramos et al. (2026) formally verified its determinant and collision certificate. The exact linear equivalence above shows that the Station output is an independent reconstruction of the announced map in different coordinates, not a new counterexample or equivalence class.

3. S2. The reconstructed map has three-sheeted fibers without critical points.

3.1 The cuspidal ruling forces the determinant cancellation

Put

b=xy-1,\qquad D=x^2\partial_x-\partial_y,

and write $F=f+zn$ , where

n=(x^3,xb^2,b^3),\qquad f=\bigl(6x+9x^2y,\;y(9b^2+6b-2),\;3y^2b(3b-1)\bigr).

Projectively, $n$ lies on the cuspidal cubic

[r:s]\longmapsto[r^3:rs^2:s^3],

because its coordinates $(U,V,W)=(x^3,xb^2,b^3)$ satisfy $V^3=UW^2$ .

Lemma 3.1 (moving-frame identities).

Define

m=(-3x^2,\;2-3b^2,\;3yb(1-b)),\qquad C=n\times m=(b^3,-3x^2b,2x^3).

Then

D(n)=3xn,\qquad n_x=bm+3yn,\qquad D(f)=m+18yn, \qquad C\cdot f_x=-6.

Proof. Each identity follows by differentiating the displayed polynomials and collecting terms in $b=xy-1$ . $\square$

Theorem 3.2 (structural determinant proof).

The ruled map $F=f+zn$ has $\det JF=-6$ .

Proof. Since $F_z=n$ , the Jacobian determinant is $\det(F_x,F_y,n)$ . Lemma 3.1 gives

F_y-x^2F_x=-m-(18y+3xz)n,

and $F_x=f_x+z(bm+3yn)$ . Therefore multilinearity and alternation of the determinant give

\begin{aligned} \det(F_x,F_y,n) &=-\det(F_x,m,n)\\ &=-\det(f_x,m,n)\\ &=(n\times m)\cdot f_x=-6. \end{aligned}

Every $z$ -dependent term vanishes because it repeats either the $m$ or $n$ direction. This is the geometric reason for the cancellation among the sixteen expanded monomials. $\square$

The next cell verifies every moving-frame identity and the resulting determinant calculation.

Show code

Code cell 10 · In [4]

b = x*y - 1
n = sp.Matrix([x**3, x*b**2, b**3])
f = sp.Matrix([6*x + 9*x**2*y, y*(9*b**2 + 6*b - 2), 3*y**2*b*(3*b - 1)])
m = sp.Matrix([-3*x**2, 2 - 3*b**2, 3*y*b*(1-b)])
C = sp.Matrix([b**3, -3*x**2*b, 2*x**3])

def D(vector):
    return vector.applyfunc(lambda entry: sp.expand(x**2*sp.diff(entry, x) - sp.diff(entry, y)))

assert matrix_is_zero(D(n) - 3*x*n)
assert matrix_is_zero(n.diff(x) - (b*m + 3*y*n))
assert matrix_is_zero(D(f) - (m + 18*y*n))
assert matrix_is_zero(n.cross(m) - C)
assert sp.expand(C.dot(f.diff(x))) == -6
assert sp.expand(n[1]**3 - n[0]*n[2]**2) == 0

frame_column_identity = sp.Matrix([
    sp.expand(entry) for entry in (F.diff(y) - x**2*F.diff(x) + m + (18*y + 3*x*z)*n)
])
assert matrix_is_zero(frame_column_identity)
assert sp.expand(sp.Matrix.hstack(F.diff(x), F.diff(y), F.diff(z)).det()) == -6


print("All moving-frame residuals vanish exactly; (n x m) . f_x =", sp.expand(C.dot(f.diff(x))))

Saved output 1

All moving-frame residuals vanish exactly; (n x m) . f_x = -6

3.2 The inverse is generically a cubic

For $a\in\mathbb Q^\times$ , define the normalized family

\begin{aligned} P_a&=ax+\frac{3a}{2}x^2y+x^3z,\\ Q_a&=\frac a6y-2axy^2+\frac{3a}{2}x^2y^3+xz-2x^2yz+x^3y^2z,\\ R_a&=2ay^2-\frac{7a}{2}xy^3+\frac{3a}{2}x^2y^4-z+3xyz-3x^2y^2z+x^3y^3z. \end{aligned}

The paper’s map is $F_6$ .

Lemma 3.3 (dense coordinates).

Set

u=xy,\quad w=x^2z,\quad A=a+\frac{3a}{2}u+w,\quad t=A(u-1),\quad X=xA,

I=t^2+\frac{2a}{3}t-\frac a3A,\qquad J=t^3+\frac a2t^2-\frac a2At.

On $X\ne0$ ,

F_a=\left(X,\frac IX,\frac J{X^2}\right).

Proof. Expanding $X$ , $I-XQ_a$ , and $J-X^2R_a$ gives respectively $P_a$ , $0$ , and $0$ . The identities are polynomial after clearing the displayed powers of $X$ , so the expansion proves them identically. $\square$

Theorem 3.4 (constant Jacobian and no affine critical points).

For $a\ne0$ ,

\det JF_a=-\frac{a^2}{6}.

Proof. On the dense set $xA\ne0$ , factor the map into four coordinate changes. Their determinants are

x^3,\qquad -A,\qquad \frac{a^2}{6}A^2,\qquad X^{-3},

whose product is $-a^2/6$ because $X=xA$ . Both sides are polynomials in $(x,y,z)$ , so equality on a dense set proves the identity everywhere. In particular, no point of affine three-space is critical. $\square$

Theorem 3.5 (generic degree three).

For a target $(X,Y,Z)$ with $X\ne0$ , put $I=XY$ and $J=X^2Z$ . Every preimage determines a root of

p(t)=t^3+at^2-3It+2J=0,

and, generically, a root recovers a preimage through

A=\frac{p'(t)}a,\quad x=\frac XA,\quad u=1+\frac tA,\quad y=\frac ux, \quad w=A-a-\frac{3a}{2}u,\quad z=\frac w{x^2}.

The map consequently has generic function-field degree exactly three.

Proof. Eliminating $A$ from Lemma 3.3 gives the cubic and $p'(t)=aA$ ; the recovery formulas then follow from the definitions. Since $X$ is invertible on this chart, $K=\mathbb Q(X,I,J)=\mathbb Q(X,Y,Z)$ . The recovery formulas show that the source function field is $K(t)$ . It remains to prove that $p$ is irreducible over $K$ . A reducible cubic has a root in $K$ . Since $p$ is monic, such a root is integral over the integrally closed UFD $\mathbb Q(X,I)[J]$ , and hence lies in that polynomial ring. If its $J$ -degree is positive, the cubic term has strictly larger $J$ -degree than every other term and cannot cancel. If its $J$ -degree is zero, the term $2J$ cannot cancel. Thus no root exists, so $p$ is irreducible and $[K(t):K]=3$ . In characteristic zero its generic roots are distinct, and the recovery formulas give three generic inverse points. $\square$

Proposition 3.6 (what happens over $X=0$ for $F_6$ ).

For a target $(0,Y,Z)$ , put $\Delta=9Y^2-48Z$ . There is always the preimage

(0,Y,12Y^2-Z).

If $\Delta\ne0$ , there are exactly two additional preimages over $\mathbb C$ , obtained from

x^2\Delta=36,\quad u=\frac32+\frac{xY}{4},\quad y=\frac ux, \quad z=-\frac{6+9u}{x^2}.

If $\Delta=0$ , there are no additional affine preimages.

Proof. Since $P_6=xA$ , every preimage lies in one of two branches. On $x=0$ , the equations are $Q_6=y$ and $R_6=12y^2-z$ , giving the unique point displayed above. On $x\ne0$ , one must have $A=0$ . Substitution gives

Q_6=\frac{4u-6}{x},\qquad R_6=\frac{3(u-1)(u-2)}{x^2}.

Solving $Q_6=Y$ gives the stated $u$ , and then $R_6=Z$ is exactly $x^2\Delta=36$ . This quadratic has two roots when $\Delta\ne0$ and none when $\Delta=0$ . Thus the apparent collision of quotient roots over $X=0$ is separated by the affine scale coordinate $x$ ; it never creates a critical point because Theorem 3.4 holds globally. $\square$

For fixed $X\ne0$ , a repeated cubic root has $p'(t)=aA=0$ , while $x=X/A$ ; the corresponding inverse point therefore leaves affine space instead of becoming critical. Proposition 3.6 gives the separate affine analysis required when $X=0$ .

The next cell checks the normalized family, dense-coordinate identities, cubic recovery, and exceptional fibers exactly.

Show code

Code cell 12 · In [5]

Pa = a*x + sp.Rational(3, 2)*a*x**2*y + x**3*z
Qa = (
    a*y/6 - 2*a*x*y**2 + sp.Rational(3, 2)*a*x**2*y**3
    + x*z - 2*x**2*y*z + x**3*y**2*z
)
Ra = (
    2*a*y**2 - sp.Rational(7, 2)*a*x*y**3 + sp.Rational(3, 2)*a*x**2*y**4
    - z + 3*x*y*z - 3*x**2*y**2*z + x**3*y**3*z
)
Fa = sp.Matrix([Pa, Qa, Ra])
det_Fa = sp.factor(Fa.jacobian((x, y, z)).det())
assert det_Fa == -a**2/6

u = x*y
w = x**2*z
A = a + sp.Rational(3, 2)*a*u + w
t = A*(u-1)
X = x*A
I = t**2 + sp.Rational(2, 3)*a*t - a*A/3
J = t**3 + a*t**2/2 - a*A*t/2
dense_residuals = (sp.expand(Pa-X), sp.expand(I-X*Qa), sp.expand(J-X**2*Ra))
assert dense_residuals == (0, 0, 0)
assert sp.expand(t**3 + a*t**2 - 3*I*t + 2*J) == 0
assert sp.expand(3*t**2 + 2*a*t - 3*I - a*A) == 0

# Four exact coordinate-change determinants in the proof of Theorem 3.4.
u0, w0, A0, t0, X0, I0, J0 = sp.symbols("u0 w0 A0 t0 X0 I0 J0")
A_uw = a + sp.Rational(3, 2)*a*u0 + w0
t_uw = A_uw*(u0-1)
change_1 = sp.Matrix([x, x*y, x**2*z]).jacobian((x, y, z)).det()
change_2 = sp.Matrix([x, A_uw, t_uw]).jacobian((x, u0, w0)).det()
I_At = t0**2 + sp.Rational(2, 3)*a*t0 - a*A0/3
J_At = t0**3 + a*t0**2/2 - a*A0*t0/2
change_3 = sp.Matrix([x*A0, I_At, J_At]).jacobian((x, A0, t0)).det()
change_4 = sp.Matrix([X0, I0/X0, J0/X0**2]).jacobian((X0, I0, J0)).det()
assert sp.expand(change_1 - x**3) == 0
assert sp.expand(change_2 + A_uw) == 0
assert sp.expand(change_3 - a**2*A0**2/6) == 0
assert sp.cancel(change_4 - X0**-3) == 0

def specialized_family(a_value):
    return tuple(sp.expand(component.subs(a, QQ(a_value))) for component in Fa)

def evaluate_map(map_components, point):
    substitutions = dict(zip((x, y, z), point))
    return tuple(sp.expand(component.subs(substitutions)) for component in map_components)

family_cases = bundle["family_checks"]["spot_checks"] + [bundle["family_checks"]["a3_transfer"]]
verified_case_rows = []
for case in family_cases:
    a_value = QQ(case["a"])
    map_components = specialized_family(a_value)
    points = [exact_point(point) for point in case["points"]]
    case_images = [evaluate_map(map_components, point) for point in points]
    expected_image = exact_point(case["common_image"])
    assert len(set(points)) == 3 and case_images == [expected_image]*3
    assert sp.expand(sp.Matrix(map_components).jacobian((x, y, z)).det()) == -a_value**2/6
    verified_case_rows.append((a_value, tuple(QQ(r) for r in case["roots"]), expected_image))

# Exact exceptional-locus identities for Proposition 3.6.
Ysym, rsym = sp.symbols("Ysym rsym", nonzero=True)
F6 = specialized_family(6)
Zsym = sp.Symbol("Zsym")
branch_x0 = evaluate_map(F6, (0, Ysym, 12*Ysym**2-Zsym))
assert tuple(sp.expand(value) for value in branch_x0) == (0, Ysym, Zsym)

# Before solving for a target, verify the complete x != 0, A = 0 branch used in the proof.
u_branch, x_branch = sp.symbols("u_branch x_branch", nonzero=True)
y_branch = u_branch/x_branch
z_branch = -(6 + 9*u_branch)/x_branch**2
branch_A0_general = evaluate_map(F6, (x_branch, y_branch, z_branch))
expected_A0_general = (
    0,
    (4*u_branch-6)/x_branch,
    3*(u_branch-1)*(u_branch-2)/x_branch**2,
)
assert all(
    sp.cancel(left-right) == 0
    for left, right in zip(branch_A0_general, expected_A0_general)
)

usym = sp.Rational(3, 2) + rsym*Ysym/4
ysym = usym/rsym
zsym = -(6 + 9*usym)/rsym**2
Zbranch = sp.Rational(3, 16)*Ysym**2 - sp.Rational(3, 4)/rsym**2
branch_A0 = evaluate_map(F6, (rsym, ysym, zsym))
assert all(sp.cancel(left-right) == 0 for left, right in zip(branch_A0, (0, Ysym, Zbranch)))



print("det(JF_a) =", det_Fa)
print("Dense-coordinate residuals =", dense_residuals)
print("Verified exact split fibers:")
for row in verified_case_rows:
    print("  a =", row[0], "; roots =", row[1], "; target =", row[2])

Saved output 1

det(JF_a) = -a**2/6
Dense-coordinate residuals = (0, 0, 0)
Verified exact split fibers:
  a = 1 ; roots = (1, 2, -4) ; target = (2, 5/3, 1)
  a = 2 ; roots = (1, 3, -6) ; target = (-1, -7, 9)
  a = -3 ; roots = (1, 3, -1) ; target = (3, 1/9, 1/6)
  a = 6 ; roots = (0, 1, -7) ; target = (1, 7/3, 0)
  a = 3 ; roots = (0, 1, -4) ; target = (1, 4/3, 0)

Station Reference. The successful agent’s tick-35 analysis contains the ruled-map search and moving-frame derivation. Evals #114 and #123 supply the resulting map, normalized family, dense-coordinate identities, and inverse-cubic calculations.

Related Work. Tao (2026), Gallagher (2026), Shaska (2026), and Speyer (2026) gave geometric, cubic-fiber, graded, and tangent-sweep explanations of the announced map before this reconstruction. The cuspidal ruling and three-sheeted inverse verified here independently recover that explanatory structure.

4. Additional findings

These are additional results that may be interesting but are not included in the spotlight.

4.1 Infinitely many rational triple fibers

The cubic inverse derived in S2 explains why the reconstructed map generically has three preimages, but it does not by itself exhibit rational fibers. We use Vieta’s formulas to choose three distinct rational inverse roots and recover the corresponding source points explicitly. This produces infinitely many rational targets with three distinct rational preimages and shows that the collision displayed in the main certificate belongs to an explicit arithmetic family. The parametrization turns the three-sheeted structure of the map into a direct generator of exact collision witnesses.

Theorem 4.1 (Vieta parametrization).

Fix $a\in\mathbb Q^\times$ . Choose distinct rational numbers $r_1,r_2,r_3$ satisfying $r_1+r_2+r_3=-a$ , and define

I=-\frac{r_1r_2+r_1r_3+r_2r_3}{3},\qquad J=-\frac{r_1r_2r_3}{2}.

For $X\in\mathbb Q^\times$ , put

A_i=\frac{3r_i^2}{a}+2r_i-\frac{3I}{a},\quad x_i=\frac X{A_i},\quad u_i=1+\frac{r_i}{A_i},\quad y_i=\frac{u_i}{x_i},

w_i=A_i-a-\frac{3a}{2}u_i,\qquad z_i=\frac{w_i}{x_i^2}.

Whenever $A_1A_2A_3\ne0$ , the three points are distinct and

F_a(x_i,y_i,z_i)=\left(X,\frac IX,\frac J{X^2}\right).

For fixed $r_1,r_2,r_3$ , varying $X\in\mathbb Q^\times$ gives infinitely many rational triple fibers.

Proof. Vieta’s formulas make the $r_i$ the roots of $t^3+at^2-3It+2J$ . Directly, $x_iy_i=u_i$ , $x_i^2z_i=w_i$ , the definition of $A_i$ is recovered, and $A_i(u_i-1)=r_i$ . Lemma 3.3 therefore gives the common image. The regular function $t=A(xy-1)$ takes the distinct values $r_i$ , so the source points are distinct. The construction produces infinitely many distinct target fibers explicitly: take $(r_1,r_2,r_3)=(0,a,-2a)$ , for which $(A_1,A_2,A_3)=(-2a,3a,6a)$ , and vary $X\in\mathbb Q^\times$ . The resulting targets $(X,2a^2/(3X),0)$ are pairwise distinct. $\square$

The next cell constructs and verifies a rational triple fiber from the Vieta parameters.

Show code

Code cell 15 · In [6]

def points_from_roots(a_value, roots, X_value):
    a_value = QQ(a_value)
    roots = tuple(QQ(root) for root in roots)
    X_value = QQ(X_value)
    assert a_value != 0 and X_value != 0
    assert len(set(roots)) == 3 and sum(roots) == -a_value
    I_value = -sum(roots[i]*roots[j] for i in range(3) for j in range(i+1, 3))/3
    J_value = -roots[0]*roots[1]*roots[2]/2
    points = []
    A_values = []
    for root in roots:
        A_value = 3*root**2/a_value + 2*root - 3*I_value/a_value
        assert A_value != 0
        x_value = X_value/A_value
        u_value = 1 + root/A_value
        y_value = u_value/x_value
        w_value = A_value - a_value - sp.Rational(3, 2)*a_value*u_value
        z_value = w_value/x_value**2
        A_values.append(A_value)
        points.append((x_value, y_value, z_value))
    target = (X_value, I_value/X_value, J_value/X_value**2)
    images = [evaluate_map(specialized_family(a_value), point) for point in points]
    assert len(set(points)) == 3 and images == [target]*3
    return tuple(points), target, tuple(A_values)

# Symbolic witness to the infinitude sentence in Section 4.1.
infinite_roots = (0, a, -2*a)
infinite_I = -sum(
    infinite_roots[i]*infinite_roots[j]
    for i in range(3) for j in range(i+1, 3)
)/3
infinite_J = -infinite_roots[0]*infinite_roots[1]*infinite_roots[2]/2
infinite_A = tuple(
    sp.factor(3*root**2/a + 2*root - 3*infinite_I/a)
    for root in infinite_roots
)
assert sp.factor(infinite_I - 2*a**2/3) == 0
assert infinite_J == 0
assert infinite_A == (-2*a, 3*a, 6*a)

generated_points, generated_target, generated_A = points_from_roots(1, (1, 2, -4), 2)
stored_nonzero_J = bundle["family_checks"]["spot_checks"][0]
assert generated_points == tuple(exact_point(point) for point in stored_nonzero_J["points"])
assert generated_target == exact_point(stored_nonzero_J["common_image"])
assert generated_target == (2, QQ("5/3"), 1)

print("Generated nonzero-J triple fiber over", generated_target)
for point in generated_points:
    print(" ", point)

Saved output 1

Generated nonzero-J triple fiber over (2, 5/3, 1)
  (-2/5, -2, -45)
  (1/3, 4, 27)
  (1/15, 13, 12465/2)

Station Reference. Eval #123 records the Vieta parametrization, recovery law, and exact examples.

Related Work. The cubic-fiber conclusion coincides with the post-announcement explanation of Gallagher (2026), which describes the cubic-fiber structure of the announced counterexample. The result here independently derives, in the notebook’s normalization, an explicit Vieta parametrization of infinitely many rational triple fibers.

4.2 Rigidity within the normalized dense-chart ansatz

We ask whether the reconstructed map can be deformed by varying the six coefficients in its normalized dense-chart representation while preserving polynomiality and a nonzero constant Jacobian. We prove that the polynomial-extension conditions first force three linear relations among the coefficients, after which the Jacobian equations leave a single nondegenerate branch—the coefficients of the reconstructed family itself. Thus the cancellation is forced within this coordinate design rather than arising from an accidental choice of parameters. The theorem closes the coefficient-deformation search inside this six-parameter ansatz.

Theorem 4.2 (unique nondegenerate branch in the normalized ansatz).

Fix $a\ne0$ and set

u=xy,\quad w=x^2z,\quad A=a+\beta u+w,\quad t=A(u-1),\quad X=xA,

I=t^2+ct+dA,\qquad J=t^3+et^2+fAt+gA^2.

If $I/X$ and $J/X^2$ extend polynomially and $(X,I/X,J/X^2)$ has nonzero constant Jacobian, then necessarily

\beta=\frac{3a}{2},\quad c=\frac{2a}{3},\quad d=-\frac a3, \quad e=\frac a2,\quad f=-\frac a2,\quad g=0.

Conversely, setting $\beta=3a/2$ , $c=2a/3$ , $d=-a/3$ , $e=a/2$ , $f=-a/2$ , and $g=0$ gives $F_a$ and determinant $-a^2/6$ .

Proof. Cancelling the common powers of $A$ gives

\frac IX=\frac{A(u-1)^2+c(u-1)+d}{x},

\frac J{X^2}=\frac{A(u-1)^3+e(u-1)^2+f(u-1)+g}{x^2}.

Divisibility by $x$ and $x^2$ is equivalent to

d=c-a,\qquad f=\beta-3a+2e,\qquad g=\beta-2a+e.

After these substitutions, two nonconstant Jacobian coefficients force

e=\frac{3c-a}{2},\qquad \beta=\frac{5a-3c}{2}.

All remaining nonconstant coefficients then vanish except

-\frac{(a-c)(2a-3c)}2,

while the constant coefficient is $-a(a-c)/2$ . The branch $c=a$ has zero determinant. Since $a\ne0$ , the unique nondegenerate branch is $c=2a/3$ , which gives exactly the six parameters above. Direct substitution proves the converse. $\square$

The next cell derives the determinant support and verifies the unique nondegenerate branch.

Show code

Code cell 18 · In [7]

beta, c, d, e, fpar, g = sp.symbols("beta c d e f g")
u_ans = x*y
w_ans = x**2*z
A_ans = a + beta*u_ans + w_ans
b_ans = u_ans - 1
t_ans = A_ans*b_ans
X_ans = x*A_ans
I_ans = t_ans**2 + c*t_ans + d*A_ans
J_ans = t_ans**3 + e*t_ans**2 + fpar*A_ans*t_ans + g*A_ans**2

Q_numerator = sp.expand(A_ans*b_ans**2 + c*b_ans + d)
R_numerator = sp.expand(A_ans*b_ans**3 + e*b_ans**2 + fpar*b_ans + g)
assert sp.expand(Q_numerator.subs(x, 0)) == a-c+d
assert sp.expand(R_numerator.subs(x, 0)) == -a+e-fpar+g
assert sp.expand(sp.diff(R_numerator, x).subs(x, 0)/y) == 3*a-beta-2*e+fpar

extension = {d: c-a, fpar: beta-3*a+2*e, g: beta-2*a+e}
Q_extended_numerator = sp.expand(Q_numerator.subs(extension))
R_extended_numerator = sp.expand(R_numerator.subs(extension))
Q_extended = sp.cancel(Q_extended_numerator/x)
R_extended = sp.cancel(R_extended_numerator/x**2)
assert sp.denom(Q_extended) == 1 and sp.denom(R_extended) == 1

det_ansatz = sp.expand(sp.Matrix([X_ans, Q_extended, R_extended]).jacobian((x, y, z)).det())
ansatz_terms = {
    powers: sp.factor(coefficient)
    for powers, coefficient in sp.Poly(det_ansatz, x, y, z).terms()
}
assert len(ansatz_terms) == 7

expected_terms = bundle["normalized_ansatz_certificate"]["determinant_after_extension"]["terms"]
locals_for_parse = {"a": a, "beta": beta, "c": c, "e": e}
for item in expected_terms:
    powers = tuple(item["powers"])
    expected_coefficient = sp.sympify(item["coefficient"], locals=locals_for_parse)
    assert sp.expand(ansatz_terms[powers] - expected_coefficient) == 0

linear_forcing = {e: (3*c-a)/2, beta: (5*a-3*c)/2}
reduced_terms = {
    powers: sp.factor(coefficient.subs(linear_forcing))
    for powers, coefficient in ansatz_terms.items()
}
nonconstant_reduced = {
    powers: coefficient for powers, coefficient in reduced_terms.items()
    if powers != (0, 0, 0) and coefficient != 0
}
assert set(nonconstant_reduced.values()) == {-sp.factor((a-c)*(2*a-3*c)/2)}
assert sp.factor(reduced_terms[(0, 0, 0)]) == -a*(a-c)/2

unique_branch = {c: 2*a/3, e: a/2, beta: 3*a/2}
final_parameters = {
    beta: 3*a/2, c: 2*a/3, d: -a/3,
    e: a/2, fpar: -a/2, g: 0,
}
assert sp.factor(det_ansatz.subs(linear_forcing).subs(c, a)) == 0
assert sp.factor(det_ansatz.subs(final_parameters)) == -a**2/6
assert matrix_is_zero(sp.Matrix([
    sp.expand(X_ans.subs(final_parameters)-Pa),
    sp.expand(Q_extended.subs(final_parameters)-Qa),
    sp.expand(R_extended.subs(final_parameters)-Ra),
]))

print("Complete determinant support after polynomial extension:")
for powers, coefficient in sorted(ansatz_terms.items(), reverse=True):
    print(" ", powers, ":", coefficient)
print("Unique nondegenerate branch gives det =", sp.factor(det_ansatz.subs(final_parameters)))

Saved output 1

Complete determinant support after polynomial extension:
  (4, 2, 1) : -3*a + 2*beta - 3*c + 4*e
  (3, 3, 0) : -beta*(3*a - 2*beta + 3*c - 4*e)
  (3, 1, 1) : -2*(a - 3*c + 2*e)
  (2, 2, 0) : -3*a**2 - 3*a*c + 4*a*e + 6*beta*c - 4*beta*e
  (2, 0, 1) : 5*a - 2*beta - 3*c
  (1, 1, 0) : -2*a**2 + 5*a*beta + 3*a*c - 2*a*e - 2*beta**2 - 2*beta*c
  (0, 0, 0) : a*(2*a - beta - c)
Unique nondegenerate branch gives det = -a**2/6

Station Reference. Eval #123 supplies the normalized ansatz, extension conditions, determinant certificate, and branch audit.

Related Work. The recent geometric accounts of Tao (2026), Gallagher (2026), Shaska (2026), and Speyer (2026) explain the cubic, graded, and tangent-sweep structure of the counterexample. The theorem classifies coefficients inside one six-parameter dense-chart ansatz; this coordinate-specific rigidity statement appears new.