The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.
Complex polynomial maps in finite dimension n ≥ 1. A local derivative condition is being compared with global polynomial invertibility; the two-variable restriction is a separate question.
Definitions
Polynomial inverse
An inverse whose coordinates are polynomials, with both compositions equal to the identity. Two distinct inputs with the same image rule out such an inverse.
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
Check the counterexample
Exact rational arithmetic: the three inputs have the same image, and the Jacobian determinant is the constant −2. A polynomial inverse would make F injective, so none exists.
Input (x, y, z)
F(x, y, z)
det JF there
(0, 0, −1/4)
(−1/4, 0, 0)
−2
(1, −3/2, 13/2)
(−1/4, 0, 0)
−2
(−1, 3/2, 13/2)
(−1/4, 0, 0)
−2
All (x, y, z)
—
−2 (expands to a constant)
This checks the stated witness by direct computation. It says nothing about two variables, where the question is open.
Visual setup
Three inputs, one image
The displayed rational points have the same image under the explicit map F. Segments indicate mapping, not paths in ℂ³.
Reading boundary. The layout is symbolic; it is not a projection of the six-real-dimensional domain. It says nothing about the two-variable case.
Select a statement below for its scope and evidence. The text view describes the complete drawing.
Text version
Three input points (0,0,−1/4), (1,−3/2,13/2) and (−1,3/2,13/2) map to (−1/4,0,0), despite det JF = −2.
Coordinates in the drawing are illustrative unless the caption specifies an exact example.
Inspect the counterexample
●Proved
A constant determinant with three inputs sharing an output
A concrete failure of injectivity and hence of a polynomial inverse. The coordinate degrees are 7, 6 and 4; a cubic fiber relation does not make this a cubic coordinate map.
Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.
A concrete failure of injectivity and hence of a polynomial inverse.
Gao 2026Formalized
Theorem · Counterexample
●ProvedGao 2026
A constant determinant with three inputs sharing an output
Set s=xy and u=1+s. The map F(x,y,z)=u3z+y2u(4+3s)y+3xu2z+3xy2(4+3s)2x−3x2y−x3z has detJF=−2. The distinct inputs (0,0,−1/4), (1,−3/2,13/2) and (−1,3/2,13/2) all map to (−1/4,0,0).
Assumptions
Use the displayed map over a characteristic-zero field.
In this problem
A concrete failure of injectivity and hence of a polynomial inverse. The coordinate degrees are 7, 6 and 4; a cubic fiber relation does not make this a cubic coordinate map.
The source witnesses this existence statement using the three-variable counterexample.
alerad/alpoge-lean project 2026Formalized
Theorem · Supporting result
●Provedalerad/alpoge-lean project 2026
No polynomial inverse for the three-variable witness
There exists a polynomial map F: Q3 → Q3 with constant Jacobian determinant −2 and no two-sided polynomial compositional inverse.
Assumptions
Polynomial maps and composition are taken over ℚ.
In this problem
The source witnesses this existence statement using the three-variable counterexample. Analytic derivative correspondence and further geometric interpretations are outside this formal result.
Set s=xy and u=1+s. The map F(x,y,z)=u3z+y2u(4+3s)y+3xu2z+3xy2(4+3s)2x−3x2y−x3z has detJF=−2. The distinct inputs (0,0,−1/4), (1,−3/2,13/2) and (−1,3/2,13/2) all map to (−1/4,0,0).
Three variables over the rationals, also viewed over the complexes. This witness does not settle the two-variable question.
Reported in sources: Formal polynomial determinant, fiber collision and no-inverse results have public pinned Lean sources. Analytic derivative correspondence is outside their stated scope; no local proof build is recorded.
OpenMath assessment: The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.
Source comparison and page curation only; independent mathematical review is pending.
OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027
The endpoint witnesses the statement over ℚ with three variables. The explicit rational points also give the complex non-injectivity; analytic correspondence was not formalized by this project.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Selected literature; source observations and coverage limits are retained in the publication details.
Contributors
The discovery report credits Levent Alpöge, Akhil Mathew for asking the question and Fable for work leading to the example. The July 20 ULAM verification manuscript prints no author name. Separate analysis: Shuhong Gao. Formalization: the alerad/alpoge-lean project’s reported AI-assisted workflow.
The manuscript cites Levent Alpöge’s announcement, credits Akhil Mathew for asking the question and Fable for the work leading to the example. No named author is printed on this verification manuscript; these discovery credits are not its bibliographic authorship.