A polynomial counterexample to weak Markus–Yamabe in dimension eight

Joshua Christl

Research note · 10 September 2026

A polynomial counterexample to weak Markus–Yamabe in dimension eight

By Joshua Christl

An everywhere Hurwitz Jacobian. Three distinct rational zeros. An explicit construction with a Lean certificate.

Read the PDF ↗ Read Lean code Download source ZIP ↓

HTML edition of the research note, with the full source snapshot in the appendices.

Abstract

We give an explicit degree-eight polynomial vector field $X:\R^8\to\R^8$ with Jacobian characteristic polynomial $(\lambda+1)^8$ at every point and three distinct rational zeros. Thus $X$ is a noninjective Hurwitz map. Appending coordinates $-u$ gives counterexamples in every dimension $n\ge8$ . The proposed improvement is from dimension fourteen to dimension eight. The certificate is checked in Lean, including the passage from polynomial partial derivatives to actual real coordinate derivatives. The complete project source needed for that certificate is included below.

01 The previous paper and the proposed improvement

Castañeda, Honorato and Valenzuela–Henríquez’s August 5, 2026 preprint, The weak Markus–Yamabe conjecture fails in dimension 14, constructs a degree-seven counterexample on $\R^{14}$ with three rational zeros and Jacobian spectrum $\{-1\}$ everywhere. Its abstract explicitly leaves dimensions $3\le n\le13$ open. See Conjecture 1.1, Theorem 1.3, and Sections 3–5 of that paper.

The dimension bound
Property	August paper	Present construction
Smallest dimension supplied	14	8
Polynomial degree	7	8
Jacobian spectrum everywhere	$\{-1\}$	$\{-1\}$
Distinct rational zeros exhibited	3	3
Dimensions covered by padding	$n\ge14$	$n\ge8$

This improves a dimension bound; it does not refute the paper’s theorem or improve its separate cubic-degree construction. Dimensions three through seven are not settled here. The claim concerns the weak conjecture about injectivity, rather than the classical formulation about global attraction.

Status of the claim. The explicit mathematical certificate below has been checked. The accompanying literature audit found no prior eight-dimensional construction as of September 10, 2026. Historical priority and independent expert review remain separate from the formal verification; no publication or acceptance is claimed by this note.

02 What a counterexample must establish

A $C^1$ map $X:\R^n\to\R^n$ is Hurwitz when every complex eigenvalue of $\J X(p)$ has negative real part for every $p\in\R^n$ . The weak conjecture says that such a map must be injective.

A counterexample therefore needs an explicit map, an everywhere-valid eigenvalue certificate, and two distinct inputs with equal outputs. A single constant matrix cannot serve: negative-real-part eigenvalues exclude zero, so that matrix would be invertible. The phenomenon here is global noninjectivity despite local invertibility everywhere.

03 The explicit counterexample

Always use the input and output coordinate order $(a,b,c,d,e,x,y,z)$ . Define

X(a,b,c,d,e,x,y,z)=\begin{pmatrix} -a-2x^3y^2+\frac12 x^3z\\ -b+d+15x^2y^3-6x^2yz\\ -c+e+9x^2y^4-3x^2y^2z\\ -d+12x^3y^4-3x^3y^2z\\ -e+4x^3y^5-x^3y^3z\\ a+\frac32 x^2y-x\\ b-3xz-y\\ c+5xy^3-3xyz-z-\frac14 \end{pmatrix}.

Its degree is eight: the monomial $4x^3y^5$ occurs, and no monomial has higher ordinary total degree. Define

\begin{aligned} p_0&=(0,0,0,0,0,0,0,-\tfrac14),\\ p_+&=(\tfrac{13}4,45,-\tfrac{297}8,-\tfrac{351}8,\tfrac{351}{16},1,-\tfrac32,\tfrac{31}2),\\ p_-&=(-\tfrac{13}4,-45,-\tfrac{297}8,\tfrac{351}8,\tfrac{351}{16},-1,\tfrac32,\tfrac{31}2). \end{aligned}

Theorem 1

The polynomial map above is smooth and Hurwitz, but is not injective. More precisely,

\det\bigl(\lambda I_8-\J X(p)\bigr)=(\lambda+1)^8\qquad(p\in\R^8,\ \lambda\in\C),

and $X(p_0)=X(p_+)=X(p_-)=0$ .

Proof. All components are polynomials, hence smooth. Differentiation and determinant expansion give the characteristic polynomial identity; the complete matrix and exact Lean certificate are in Appendix A, and an explanatory derivation follows below. A characteristic root must therefore be $-1$ , whose real part is negative. Substitution of the three rational points into the field gives zero in each component. Their $x$ coordinates are respectively $0,1,-1$ , so they are pairwise distinct. Consequently the map is not injective. □

Every higher dimension

For $n=8+k$ , put $\widehat X(p,u)=(X(p),-u)$ , where $u\in\R^k$ . Its Jacobian is block diagonal with blocks $\J X(p)$ and $-I_k$ . Its characteristic polynomial is $(\lambda+1)^{8+k}$ , and the three points $(p_0,0),(p_+,0),(p_-,0)$ still have the same image. This proves failure in every dimension $n\ge8$ .

04 How eight coordinates were obtained

The starting point is the three-dimensional Keller map reproduced in Section 3 of the August paper. A Keller map has constant nonzero Jacobian determinant. After normalizing the component order and scale, and making the source shear $z_{\rm old}=z-4y^2$ , write the resulting map as

F_i(v)=v_i+\sum_{j=1}^{\ell_i}H_{i,j}(v),\qquad v=(x,y,z),\quad(\ell_1,\ell_2,\ell_3)=(2,3,3).

The terms are explicitly

\begin{aligned} H_{1,1}&=-\tfrac32x^2y,&H_{1,2}&=2x^3y^2-\tfrac12x^3z,\\ H_{2,1}&=3xz,&H_{2,2}&=-15x^2y^3+6x^2yz,\\ H_{2,3}&=-12x^3y^4+3x^3y^2z,\\ H_{3,1}&=-5xy^3+3xyz,&H_{3,2}&=-9x^2y^4+3x^2y^2z,\\ H_{3,3}&=-4x^3y^5+x^3y^3z. \end{aligned}

The source shear has determinant one and the normalized original map has determinant one. Thus $\det\J F=1$ . Alternatively this identity is checked by differentiating the three displayed sums and expanding their determinant.

Give $x,y,z$ weights $w=(1,1,2)$ . Every $H_{i,j}$ has weighted degree $w_i+2j$ :

H_{i,j}(sx,sy,s^2z)=s^{w_i+2j}H_{i,j}(x,y,z).

Weights organize the terms differently from ordinary total degree. The source shear is what removes the obstructing term of relative weighted degree zero.

Introduce a chain $q_{i,1},\ldots,q_{i,\ell_i}$ for each component, with $q_{i,1}=v_i$ and $q_{i,\ell_i+1}=0$ . Take $\beta=(0,0,-1/4)$ and define chain equations

\begin{aligned} Y_{i,1}&=\beta_i-q_{i,1}+q_{i,2}-H_{i,1}(v),\\ Y_{i,j}&=-q_{i,j}+q_{i,j+1}-H_{i,j}(v)\quad(j\ge2). \end{aligned}

Identify the chain coordinates as

\begin{aligned} (q_{1,1},q_{1,2})&=(x,a),\\ (q_{2,1},q_{2,2},q_{2,3})&=(y,b,d),\\ (q_{3,1},q_{3,2},q_{3,3})&=(z,c,e). \end{aligned}

Reordering both coordinates and equations as $(a,b,c,d,e,x,y,z)$ gives exactly the displayed field. There are $2+3+3=8$ coordinates.

Why the collision survives

Solving the auxiliary equations gives $q_{i,j}=-\sum_{m=j}^{\ell_i}H_{i,m}(v)$ for $j\ge2$ . The remaining equations become $\beta-F(v)=0$ . The three base points are $(0,0,-1/4)$ , $(1,-3/2,31/2)$ and $(-1,3/2,31/2)$ , with common image $\beta$ . Back substitution gives precisely the displayed $p_0,p_+,p_-$ .

05 Why the Jacobian spectrum is constantly minus one

This argument explains the construction. The direct Lean determinant proof in the appendix is independent of it.

Step 1: a constant determinant

In chain order write $\J Y=-I_8+M$ . The five auxiliary equations are affine in the auxiliary coordinates; their Jacobian block $A$ is triangular with diagonal $-1$ . Eliminating these equations leaves $\beta-F(v)$ . If the full Jacobian is written in auxiliary/base block order as

\J Y=\begin{pmatrix}A&B\\C&D\end{pmatrix},

then its Schur complement satisfies $D-CA^{-1}B=-\J F(v)$ . Hence

\begin{aligned}\det\J Y&=\det A\,\det(-\J F)=(-1)^5(-1)^3=1,\\\det(I_8-M)&=1.\end{aligned}

Reordering coordinates and equations simultaneously does not change these determinants.

Step 2: weighted scaling

Assign $\nu_{i,j}=w_i+2(j-1)$ to chain coordinate $q_{i,j}$ , and let $D_s=\operatorname{diag}(s^{\nu_{i,j}})$ . The entries of $M$ depend only on $v$ . Its nonzero entries are chain constants $1$ , and terms $-\partial H_{i,j}/\partial v_r$ .

For a derivative entry, its weighted degree is $w_i+2j-w_r=2+\nu_{i,j}-\nu_{r,1}$ . For a chain constant in column $(i,j+1)$ , this expression is zero. Consequently, for $s\ne0$ ,

M(sx,sy,s^2z)=s^2D_sM(x,y,z)D_s^{-1}.

Combining this with Step 1 gives

\det(I_8-s^2M(v))=1\qquad(s\ne0).

For fixed real $v$ , the polynomial $r\mapsto\det(I_8-rM(v))-1$ vanishes at every positive real $r=s^2$ . It is therefore identically zero. It follows that $\det(tI_8-M(v))=t^8$ , initially for $t\ne0$ and then for all $t$ by polynomial identity. Finally,

\det(\lambda I_8-\J Y)=\det((\lambda+1)I_8-M)=(\lambda+1)^8.

This is the required identity; it holds over $\C$ because it is a polynomial identity with real coefficients.

What changed from the August construction

The existing method uses ordinary homogeneous pieces. The present construction uses the displayed source shear and weighted pieces, retaining only chain lengths $(2,3,3)$ . The derivative weights make the same spectral mechanism work with fewer coordinates. The explicit map and its certificate establish the improvement even without a general theorem about weighted chains.

06 Lean verification and exact scope

The final Lean theorem is:

theorem weak_markus_yamabe_false_in_eight :
    ∃ F : (Fin 8 → ℝ) → (Fin 8 → ℝ),
      ContDiff ℝ (⊤ : ℕ∞) F ∧ IsHurwitz F ∧ ¬ Function.Injective F

Here IsHurwitz quantifies over every real input and every complex characteristic root of the actual coordinate-derivative matrix. Smoothness ensures these partial derivatives are the classical Jacobian. The proof uses the explicit polynomial witness, rather than postulating a matrix with the desired spectrum.

Open the theorem in Proof Explorer ↗

The certificate’s six Lean modules
Module	Role
MarkusEight	Formula, displayed Jacobian, exact characteristic determinant.
MarkusPolynomial	Multivariate polynomial representation, all formal partial derivatives, evaluation and analytic derivative bridge.
CalculusLibrary	Evaluated formal partial derivatives are real coordinate derivatives.
VectorLibrary	Reduction lemmas for explicit eight-coordinate vectors.
MarkusResult	Three zeros, distinctness, smoothness, Hurwitz property and final existence theorem.
Library	Shared Mathlib import and project-owned supporting lemmas.

The kernel-checked determinant proof uses eval_det and ring. It does not assume a symbolic algebra program’s answer as an axiom. The independent SymPy script differentiates the map and verifies that $\J X+I_8$ has characteristic polynomial $t^8$ , then checks all three rational zeros.

Replay checked on September 10, 2026. The named Lean build and axiom audit completed successfully; the exact SymPy replay passed. Lean and Mathlib are pinned to version 4.33.1. The audited declarations depend only on propext, Classical.choice, and Quot.sound; they do not use sorryAx or a custom axiom.

The existence theorem formally closes the dimension-eight analytic claim. The ordinary-degree count and the padding argument for $n>8$ are the elementary written arguments above. The general weighted-chain construction and the historical novelty claim are not additional conclusions of the Lean theorem.

07 Reproducing the certificate

The source archive contains the six complete Lean modules, pinned Lake configuration, an audit file, the exact symbolic checker, and source hashes. With Lean/elan installed, run in its source directory:

lake exe cache get
lake build ProofExplorer.Jacobian.MarkusResult
lake env lean Audit.lean
# Optional independent calculation, with SymPy installed:
python3 check_symbolic.py

The explicit target is intentional: the configuration’s default target belongs to the larger Proof Explorer repository. No omitted project module is needed for this named target. The appendix prints the exact source snapshot; use the archive for compilation.

Source README · Source hashes · Download LaTeX

08 Source and claim checklist

Previous result. Á. Castañeda, G. Honorato and F. Valenzuela–Henríquez, The weak Markus–Yamabe conjecture fails in dimension 14, arXiv:2608.05392v1, 5 August 2026. The three-dimensional starting map is attributed there to Alpöge.
Proposed contribution. The explicit eight-dimensional polynomial field, obtained from a source shear and weighted chain lengths $(2,3,3)$ , with its exact derivative, determinant and collision certificate.
Formal source. The appendix is a snapshot of ProofExplorer/Jacobian/ in the Proof Explorer repository. Its six files are reproduced without proof edits. The larger shared Library.lean contains coefficient lemmas unrelated to this result; it is included in full to preserve the exact import closure.
What remains outside the claim. No result for dimensions three through seven, no claim of the smallest possible degree, and no independent priority or peer-review certification.

Audit command and output

import ProofExplorer.Jacobian.MarkusResult

#print axioms ProofExplorer.Jacobian.MarkusEight.characteristic_determinant
#print axioms ProofExplorer.Jacobian.MarkusEight.actual_jacobian
#print axioms ProofExplorer.Jacobian.MarkusEight.three_zeros
#print axioms ProofExplorer.Jacobian.MarkusEight.weak_markus_yamabe_false_in_eight

'ProofExplorer.Jacobian.MarkusEight.characteristic_determinant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.actual_jacobian' depends on axioms: [propext, Classical.choice, Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.three_zeros' depends on axioms: [propext, Classical.choice, Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.weak_markus_yamabe_false_in_eight' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

A–G Source appendices

The complete archived source, as printed in the PDF. Expand a module to read it here, or download its .lean file. The complete source ZIP includes the pinned build configuration and verification records.

A · MarkusEight.leanThe field, Jacobian, and determinant

import ProofExplorer.Jacobian.Library

/-! An eight-dimensional polynomial Hurwitz candidate, ordered (a,b,c,d,e,x,y,z).
The determinant and collision certificates are independent of the chain argument. -/
namespace ProofExplorer.Jacobian.MarkusEight
noncomputable section
variable {K : Type*} [Field K] [CharZero K]

def field (a b c d e x y z : K) : Fin 8 → K :=
  ![-a - 2*x^3*y^2 + x^3*z/2,
    -b + d + 15*x^2*y^3 - 6*x^2*y*z,
    -c + e + 9*x^2*y^4 - 3*x^2*y^2*z,
    -d + 12*x^3*y^4 - 3*x^3*y^2*z,
    -e + 4*x^3*y^5 - x^3*y^3*z,
    a + 3*x^2*y/2 - x,
    b - 3*x*z - y,
    c + 5*x*y^3 - 3*x*y*z - z - 1/4]

def jacobian (x y z : K) : Matrix (Fin 8) (Fin 8) K :=
  !![-1, 0, 0, 0, 0, -6*x^2*y^2 + 3*x^2*z/2, -4*x^3*y, x^3/2;
    0, -1, 0, 1, 0, 30*x*y^3 - 12*x*y*z, 45*x^2*y^2 - 6*x^2*z, -6*x^2*y;
    0, 0, -1, 0, 1, 18*x*y^4 - 6*x*y^2*z, 36*x^2*y^3 - 6*x^2*y*z, -3*x^2*y^2;
    0, 0, 0, -1, 0, 36*x^2*y^4 - 9*x^2*y^2*z, 48*x^3*y^3 - 6*x^3*y*z, -3*x^3*y^2;
    0, 0, 0, 0, -1, 12*x^2*y^5 - 3*x^2*y^3*z, 20*x^3*y^4 - 3*x^3*y^2*z, -x^3*y^3;
    1, 0, 0, 0, 0, 3*x*y - 1, 3*x^2/2, 0;
    0, 1, 0, 0, 0, -3*z, -1, -3*x;
    0, 0, 1, 0, 0, 5*y^3 - 3*y*z, 15*x*y^2 - 3*x*z, -3*x*y - 1]

def characteristicMatrix (t x y z : K) : Matrix (Fin 8) (Fin 8) K :=
  !![t + 1, 0, 0, 0, 0, 6*x^2*y^2 - 3*x^2*z/2, 4*x^3*y, -x^3/2;
    0, t + 1, 0, -1, 0, -30*x*y^3 + 12*x*y*z, -45*x^2*y^2 + 6*x^2*z, 6*x^2*y;
    0, 0, t + 1, 0, -1, -18*x*y^4 + 6*x*y^2*z, -36*x^2*y^3 + 6*x^2*y*z, 3*x^2*y^2;
    0, 0, 0, t + 1, 0, -36*x^2*y^4 + 9*x^2*y^2*z, -48*x^3*y^3 + 6*x^3*y*z, 3*x^3*y^2;
    0, 0, 0, 0, t + 1, -12*x^2*y^5 + 3*x^2*y^3*z, -20*x^3*y^4 + 3*x^3*y^2*z, x^3*y^3;
    -1, 0, 0, 0, 0, t - 3*x*y + 1, -3*x^2/2, 0;
    0, -1, 0, 0, 0, 3*z, t + 1, 3*x;
    0, 0, -1, 0, 0, -5*y^3 + 3*y*z, -15*x*y^2 + 3*x*z, t + 3*x*y + 1]

set_option maxRecDepth 10000 in
set_option maxHeartbeats 0 in
 theorem characteristic_determinant (t x y z : K) :
    (characteristicMatrix t x y z).det = (t+1)^8 := by
  unfold characteristicMatrix
  eval_det
  ring

end
end ProofExplorer.Jacobian.MarkusEight

Download MarkusEight.lean ↓

B · MarkusPolynomial.leanPolynomial and analytic derivatives

import ProofExplorer.Jacobian.MarkusEight
import ProofExplorer.Jacobian.CalculusLibrary

namespace ProofExplorer.Jacobian.MarkusEight
open MvPolynomial
noncomputable section
set_option maxHeartbeats 0
set_option maxRecDepth 10000
variable {K : Type*} [Field K] [CharZero K]

def polynomialMap : Fin 8 → MvPolynomial (Fin 8) K :=
  ![(((C (-1)) * (X 0)) + ((C (1/2)) * (X 7) * ((X 5) ^ 3)) + ((C (-2)) * ((X 5) ^ 3) * ((X 6) ^ 2))),
    ((X 3) + ((C (-1)) * (X 1)) + ((C (15)) * ((X 5) ^ 2) * ((X 6) ^ 3)) + ((C (-6)) * (X 6) * (X 7) * ((X 5) ^ 2))),
    ((X 4) + ((C (-1)) * (X 2)) + ((C (9)) * ((X 5) ^ 2) * ((X 6) ^ 4)) + ((C (-3)) * (X 7) * ((X 5) ^ 2) * ((X 6) ^ 2))),
    (((C (-1)) * (X 3)) + ((C (12)) * ((X 5) ^ 3) * ((X 6) ^ 4)) + ((C (-3)) * (X 7) * ((X 5) ^ 3) * ((X 6) ^ 2))),
    (((C (-1)) * (X 4)) + ((C (4)) * ((X 5) ^ 3) * ((X 6) ^ 5)) + ((C (-1)) * (X 7) * ((X 5) ^ 3) * ((X 6) ^ 3))),
    ((X 0) + ((C (-1)) * (X 5)) + ((C (3/2)) * (X 6) * ((X 5) ^ 2))),
    ((X 1) + ((C (-1)) * (X 6)) + ((C (-3)) * (X 5) * (X 7))),
    ((C (-1/4)) + (X 2) + ((C (-1)) * (X 7)) + ((C (5)) * (X 5) * ((X 6) ^ 3)) + ((C (-3)) * (X 5) * (X 6) * (X 7)))]

def polynomialJacobian : Matrix (Fin 8) (Fin 8) (MvPolynomial (Fin 8) K) :=
  !![(C (-1)), (C (0)), (C (0)), (C (0)), (C (0)), (((C (-6)) * ((X 5) ^ 2) * ((X 6) ^ 2)) + ((C (3/2)) * (X 7) * ((X 5) ^ 2))), ((C (-4)) * (X 6) * ((X 5) ^ 3)), ((C (1/2)) * ((X 5) ^ 3));
    (C (0)), (C (-1)), (C (0)), (C (1)), (C (0)), (((C (30)) * (X 5) * ((X 6) ^ 3)) + ((C (-12)) * (X 5) * (X 6) * (X 7))), (((C (-6)) * (X 7) * ((X 5) ^ 2)) + ((C (45)) * ((X 5) ^ 2) * ((X 6) ^ 2))), ((C (-6)) * (X 6) * ((X 5) ^ 2));
    (C (0)), (C (0)), (C (-1)), (C (0)), (C (1)), (((C (18)) * (X 5) * ((X 6) ^ 4)) + ((C (-6)) * (X 5) * (X 7) * ((X 6) ^ 2))), (((C (36)) * ((X 5) ^ 2) * ((X 6) ^ 3)) + ((C (-6)) * (X 6) * (X 7) * ((X 5) ^ 2))), ((C (-3)) * ((X 5) ^ 2) * ((X 6) ^ 2));
    (C (0)), (C (0)), (C (0)), (C (-1)), (C (0)), (((C (36)) * ((X 5) ^ 2) * ((X 6) ^ 4)) + ((C (-9)) * (X 7) * ((X 5) ^ 2) * ((X 6) ^ 2))), (((C (48)) * ((X 5) ^ 3) * ((X 6) ^ 3)) + ((C (-6)) * (X 6) * (X 7) * ((X 5) ^ 3))), ((C (-3)) * ((X 5) ^ 3) * ((X 6) ^ 2));
    (C (0)), (C (0)), (C (0)), (C (0)), (C (-1)), (((C (12)) * ((X 5) ^ 2) * ((X 6) ^ 5)) + ((C (-3)) * (X 7) * ((X 5) ^ 2) * ((X 6) ^ 3))), (((C (20)) * ((X 5) ^ 3) * ((X 6) ^ 4)) + ((C (-3)) * (X 7) * ((X 5) ^ 3) * ((X 6) ^ 2))), ((C (-1)) * ((X 5) ^ 3) * ((X 6) ^ 3));
    (C (1)), (C (0)), (C (0)), (C (0)), (C (0)), ((C (-1)) + ((C (3)) * (X 5) * (X 6))), ((C (3/2)) * ((X 5) ^ 2)), (C (0));
    (C (0)), (C (1)), (C (0)), (C (0)), (C (0)), ((C (-3)) * (X 7)), (C (-1)), ((C (-3)) * (X 5));
    (C (0)), (C (0)), (C (1)), (C (0)), (C (0)), (((C (5)) * ((X 6) ^ 3)) + ((C (-3)) * (X 6) * (X 7))), (((C (-3)) * (X 5) * (X 7)) + ((C (15)) * (X 5) * ((X 6) ^ 2))), ((C (-1)) + ((C (-3)) * (X 5) * (X 6)))]

set_option maxHeartbeats 0 in
theorem polynomial_jacobian_entries (i j : Fin 8) :
    pderiv j (polynomialMap (K := K) i) = polynomialJacobian i j := by
  apply MvPolynomial.funext
  intro u
  fin_cases i <;> fin_cases j <;>
    simp [polynomialMap, polynomialJacobian, Derivation.leibniz, smul_eq_mul,
      Library.mv_pderiv_numeral, map_ofNat] <;> ring

theorem polynomialMap_evaluation (p : Fin 8 → K) (i : Fin 8) :
    eval p (polynomialMap i) = field (p 0) (p 1) (p 2) (p 3) (p 4) (p 5) (p 6) (p 7) i := by
  fin_cases i <;> simp [polynomialMap, field] <;> ring

theorem polynomialJacobian_evaluation (p : Fin 8 → K) (i j : Fin 8) :
    eval p (polynomialJacobian i j) = jacobian (p 5) (p 6) (p 7) i j := by
  fin_cases i <;> fin_cases j <;> simp [polynomialJacobian, jacobian] <;> ring

/-- Analytic coordinate derivatives of the actual real polynomial field. -/
theorem analytic_jacobian (p : Fin 8 → ℝ) (i j : Fin 8) :
    HasDerivAt (fun t => let q := Function.update p j t
      field (q 0) (q 1) (q 2) (q 3) (q 4) (q 5) (q 6) (q 7) i)
      (jacobian (p 5) (p 6) (p 7) i j) (p j) := by
  have h := CalculusLibrary.eval_hasDerivAt (polynomialMap i) p j
  simpa only [polynomial_jacobian_entries, polynomialJacobian_evaluation,
    polynomialMap_evaluation] using h

end
end ProofExplorer.Jacobian.MarkusEight

Download MarkusPolynomial.lean ↓

C · MarkusResult.leanThe final existence theorem

import ProofExplorer.Jacobian.MarkusPolynomial
import ProofExplorer.Jacobian.VectorLibrary

namespace ProofExplorer.Jacobian.MarkusEight
noncomputable section
variable {K : Type*} [Field K] [CharZero K]
set_option maxHeartbeats 0
set_option maxRecDepth 10000

/-- The real vector field on its eight-dimensional coordinate space. -/
def vectorField (p : Fin 8 → K) : Fin 8 → K :=
  field (p 0) (p 1) (p 2) (p 3) (p 4) (p 5) (p 6) (p 7)

def zeroPoint : Fin 8 → K := ![0,0,0,0,0,0,0,-1/4]
def positivePoint : Fin 8 → K := ![13/4,45,-297/8,-351/8,351/16,1,-3/2,31/2]
def negativePoint : Fin 8 → K := ![-13/4,-45,-297/8,351/8,351/16,-1,3/2,31/2]

theorem three_zeros :
    vectorField (zeroPoint (K := K)) = 0 ∧
    vectorField (positivePoint (K := K)) = 0 ∧
    vectorField (negativePoint (K := K)) = 0 := by
  constructor
  · funext i; fin_cases i <;> norm_num [vectorField, field, zeroPoint, Matrix.cons_val]
  constructor
  · funext i; fin_cases i <;> norm_num [vectorField, field, positivePoint, Matrix.cons_val]
  · funext i; fin_cases i <;> norm_num [vectorField, field, negativePoint, Matrix.cons_val]

theorem three_points_distinct :
    zeroPoint (K := K) ≠ positivePoint ∧ zeroPoint (K := K) ≠ negativePoint ∧
    positivePoint (K := K) ≠ negativePoint := by
  constructor
  · intro h; have := congrFun h 5; norm_num [zeroPoint, positivePoint, Matrix.cons_val] at this
  constructor
  · intro h; have := congrFun h 5; norm_num [zeroPoint, negativePoint, Matrix.cons_val] at this
  · intro h; have := congrFun h 5; norm_num [positivePoint, negativePoint, Matrix.cons_val] at this

theorem not_injective : ¬ Function.Injective (vectorField (K := K)) := by
  intro h
  exact three_points_distinct.1 (h (three_zeros.1.trans three_zeros.2.1.symm))

theorem characteristicMatrix_eq (t x y z : K) :
    characteristicMatrix t x y z = Matrix.scalar (Fin 8) t - jacobian x y z := by
  apply Matrix.ext
  intro i j
  fin_cases i <;> fin_cases j <;>
    simp [characteristicMatrix, jacobian, Matrix.scalar, Matrix.diagonal] <;> ring

/-- Every complex characteristic root is exactly minus one. -/
theorem characteristic_root (t x y z : ℂ) :
    (Matrix.scalar (Fin 8) t - jacobian x y z).det = 0 ↔ t = -1 := by
  rw [← characteristicMatrix_eq, characteristic_determinant]
  constructor
  · intro h
    have hz : t+1=0 := eq_zero_of_pow_eq_zero h
    linear_combination hz
  · intro h; simp [h]


/-- Matrix of actual real coordinate derivatives, for any map on R^8. -/
def analyticJacobian (F : (Fin 8 → ℝ) → (Fin 8 → ℝ)) (p : Fin 8 → ℝ) :
    Matrix (Fin 8) (Fin 8) ℝ :=
  fun i j => deriv (fun t => F (Function.update p j t) i) (p j)

/-- The usual Hurwitz condition, expressed through complex characteristic roots. -/
def IsHurwitz (F : (Fin 8 → ℝ) → (Fin 8 → ℝ)) : Prop :=
  ∀ p (t : ℂ),
    (Matrix.scalar (Fin 8) t - (analyticJacobian F p).map Complex.ofReal).det = 0 → t.re < 0

theorem actual_jacobian (p : Fin 8 → ℝ) :
    analyticJacobian vectorField p = jacobian (p 5) (p 6) (p 7) := by
  apply Matrix.ext
  intro i j
  exact (analytic_jacobian p i j).deriv

theorem complexified_jacobian (x y z : ℝ) :
    (jacobian x y z).map Complex.ofReal = jacobian (x : ℂ) (y : ℂ) (z : ℂ) := by
  apply Matrix.ext
  intro i j
  fin_cases i <;> fin_cases j <;> simp [jacobian, Matrix.map_apply, Matrix.cons_val] <;> push_cast <;> ring

theorem vectorField_hurwitz : IsHurwitz vectorField := by
  intro p t ht
  rw [actual_jacobian, complexified_jacobian] at ht
  have h := (characteristic_root t (p 5) (p 6) (p 7)).mp ht
  rw [h]
  norm_num

theorem vectorField_smooth : ContDiff ℝ (⊤ : ℕ∞) (vectorField (K := ℝ)) := by
  apply contDiff_pi.2
  intro i
  fin_cases i <;> dsimp [vectorField, field] <;> fun_prop

/-- An end-to-end analytic counterexample in dimension eight. -/
theorem weak_markus_yamabe_false_in_eight :
    ∃ F : (Fin 8 → ℝ) → (Fin 8 → ℝ),
      ContDiff ℝ (⊤ : ℕ∞) F ∧ IsHurwitz F ∧ ¬ Function.Injective F :=
  ⟨vectorField, vectorField_smooth, vectorField_hurwitz, not_injective⟩

end
end ProofExplorer.Jacobian.MarkusEight

Download MarkusResult.lean ↓

D · CalculusLibrary.leanThe coordinate-derivative bridge

import ProofExplorer.Jacobian.Library

namespace ProofExplorer.Jacobian.CalculusLibrary
open MvPolynomial

set_option backward.isDefEq.respectTransparency false in
/-- Formal partial derivatives agree with analytic coordinate derivatives. -/
theorem eval_hasDerivAt {n : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (u : Fin n → ℝ) (j : Fin n) :
    HasDerivAt (fun t => eval (Function.update u j t) p)
      (eval u (pderiv j p)) (u j) := by
  induction p using MvPolynomial.induction_on with
  | C c => simpa using hasDerivAt_const (u j) c
  | add p q hp hq =>
    convert! hp.add hq using 1 <;> simp [Pi.add_apply] <;> rfl
  | mul_X p i hp =>
    by_cases hij : j = i
    · subst i
      convert! hp.mul (hasDerivAt_id (u j)) using 1 <;>
        simp [Derivation.leibniz, smul_eq_mul, Pi.mul_apply, mul_comm, add_comm] <;> rfl
    · convert! hp.mul (hasDerivAt_const (u j) (u i)) using 1 <;>
        simp [Derivation.leibniz, smul_eq_mul, hij, Function.update_of_ne (Ne.symm hij), Pi.mul_apply, mul_comm] <;> rfl

end ProofExplorer.Jacobian.CalculusLibrary

Download CalculusLibrary.lean ↓

E · VectorLibrary.leanEight-coordinate vector lemmas

import ProofExplorer.Jacobian.Library

namespace ProofExplorer.Jacobian.VectorLibrary

@[simp] theorem eight_0 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 0 = a := rfl

@[simp] theorem eight_1 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 1 = b := rfl

@[simp] theorem eight_2 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 2 = c := rfl

@[simp] theorem eight_3 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 3 = d := rfl

@[simp] theorem eight_4 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 4 = e := rfl

@[simp] theorem eight_5 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 5 = f := rfl

@[simp] theorem eight_6 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 6 = g := rfl

@[simp] theorem eight_7 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 7 = h := rfl

end ProofExplorer.Jacobian.VectorLibrary

Download VectorLibrary.lean ↓

F · Library.leanShared project library

import Mathlib

namespace ProofExplorer.Jacobian.Library
open Polynomial
variable {R : Type*} [CommRing R]

theorem coeff_mul_0 (p q : R[X]) : (p*q).coeff 0 = p.coeff 0 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_1 (p q : R[X]) : (p*q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_2 (p q : R[X]) : (p*q).coeff 2 = p.coeff 0 * q.coeff 2 + p.coeff 1 * q.coeff 1 + p.coeff 2 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_3 (p q : R[X]) : (p*q).coeff 3 = p.coeff 0 * q.coeff 3 + p.coeff 1 * q.coeff 2 + p.coeff 2 * q.coeff 1 + p.coeff 3 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_pow_2_0 (p : R[X]) : (p^2).coeff 0 = 1*(p.coeff 0)^2 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_1 (p : R[X]) : (p^2).coeff 1 = 2*(p.coeff 0)^1*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_2 (p : R[X]) : (p^2).coeff 2 = 1*(p.coeff 1)^2 + 2*(p.coeff 0)^1*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_3 (p : R[X]) : (p^2).coeff 3 = 2*(p.coeff 1)^1*(p.coeff 2)^1 + 2*(p.coeff 0)^1*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_0 (p : R[X]) : (p^3).coeff 0 = 1*(p.coeff 0)^3 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_1 (p : R[X]) : (p^3).coeff 1 = 3*(p.coeff 0)^2*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_2 (p : R[X]) : (p^3).coeff 2 = 3*(p.coeff 0)^1*(p.coeff 1)^2 + 3*(p.coeff 0)^2*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_3 (p : R[X]) : (p^3).coeff 3 = 1*(p.coeff 1)^3 + 6*(p.coeff 0)^1*(p.coeff 1)^1*(p.coeff 2)^1 + 3*(p.coeff 0)^2*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_0 (p : R[X]) : (p^4).coeff 0 = 1*(p.coeff 0)^4 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_1 (p : R[X]) : (p^4).coeff 1 = 4*(p.coeff 0)^3*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_2 (p : R[X]) : (p^4).coeff 2 = 6*(p.coeff 0)^2*(p.coeff 1)^2 + 4*(p.coeff 0)^3*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_3 (p : R[X]) : (p^4).coeff 3 = 4*(p.coeff 0)^1*(p.coeff 1)^3 + 12*(p.coeff 0)^2*(p.coeff 1)^1*(p.coeff 2)^1 + 4*(p.coeff 0)^3*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_0 (p : R[X]) : (p^5).coeff 0 = 1*(p.coeff 0)^5 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_1 (p : R[X]) : (p^5).coeff 1 = 5*(p.coeff 0)^4*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_2 (p : R[X]) : (p^5).coeff 2 = 10*(p.coeff 0)^3*(p.coeff 1)^2 + 5*(p.coeff 0)^4*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_3 (p : R[X]) : (p^5).coeff 3 = 10*(p.coeff 0)^2*(p.coeff 1)^3 + 20*(p.coeff 0)^3*(p.coeff 1)^1*(p.coeff 2)^1 + 5*(p.coeff 0)^4*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_0 (p : R[X]) : (p^6).coeff 0 = 1*(p.coeff 0)^6 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_1 (p : R[X]) : (p^6).coeff 1 = 6*(p.coeff 0)^5*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_2 (p : R[X]) : (p^6).coeff 2 = 15*(p.coeff 0)^4*(p.coeff 1)^2 + 6*(p.coeff 0)^5*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_3 (p : R[X]) : (p^6).coeff 3 = 20*(p.coeff 0)^3*(p.coeff 1)^3 + 30*(p.coeff 0)^4*(p.coeff 1)^1*(p.coeff 2)^1 + 6*(p.coeff 0)^5*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_0 (p : R[X]) : (p^7).coeff 0 = 1*(p.coeff 0)^7 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_1 (p : R[X]) : (p^7).coeff 1 = 7*(p.coeff 0)^6*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_2 (p : R[X]) : (p^7).coeff 2 = 21*(p.coeff 0)^5*(p.coeff 1)^2 + 7*(p.coeff 0)^6*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_3 (p : R[X]) : (p^7).coeff 3 = 35*(p.coeff 0)^4*(p.coeff 1)^3 + 42*(p.coeff 0)^5*(p.coeff 1)^1*(p.coeff 2)^1 + 7*(p.coeff 0)^6*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

/-- Numeral rule for partial derivatives, in any finite number of variables. -/
theorem mv_pderiv_numeral {K : Type*} [CommRing K] {n : ℕ}
    (i : Fin n) (m : ℕ) [m.AtLeastTwo] :
    MvPolynomial.pderiv i (no_index (OfNat.ofNat m) : MvPolynomial (Fin n) K) = 0 := by
  exact (MvPolynomial.pderiv i).map_natCast m

/-- Coefficient extraction after multiplication by a variable. -/
theorem mv_coeff_X_mul {K : Type*} [CommSemiring K] {n : ℕ}
    (m : Fin n →₀ ℕ) (i : Fin n) (p : MvPolynomial (Fin n) K) :
    MvPolynomial.coeff m (MvPolynomial.X i * p) =
      if i ∈ m.support then MvPolynomial.coeff (m-Finsupp.single i 1) p else 0 :=
  MvPolynomial.coeff_X_mul' m i p

end ProofExplorer.Jacobian.Library

Download Library.lean ↓

G · Independent exact arithmetic checkPython · Requires SymPy

This Python program is supplementary evidence; the Lean proof does not depend on its output.

"""Exact symbolic certificate and reproducible Lean certificate generation."""
import sympy as s
from pathlib import Path
import json
zv=s.symbols('a b c d e x y z')
a,b,c,d,e,x,y,z=zv
t=s.Symbol('t')
F=s.Matrix([-a-2*x**3*y**2+x**3*z/2,-b+d+15*x**2*y**3-6*x**2*y*z,-c+e+9*x**2*y**4-3*x**2*y**2*z,-d+12*x**3*y**4-3*x**3*y**2*z,-e+4*x**3*y**5-x**3*y**3*z,a+s.Rational(3,2)*x**2*y-x,b-3*x*z-y,c+5*x*y**3-3*x*y*z-z-s.Rational(1,4)])
J=F.jacobian(zv)
points=[[0,0,0,0,0,0,0,-s.Rational(1,4)],[s.Rational(13,4),45,-s.Rational(297,8),-s.Rational(351,8),s.Rational(351,16),1,-s.Rational(3,2),s.Rational(31,2)],[-s.Rational(13,4),-45,-s.Rational(297,8),s.Rational(351,8),s.Rational(351,16),-1,s.Rational(3,2),s.Rational(31,2)]]
assert (J+s.eye(8)).charpoly(t).as_expr()==t**8
assert all(F.subs(dict(zip(zv,p)))==s.zeros(8,1) for p in points)
Path(__file__).with_suffix('.json').write_text(json.dumps({'order':list(map(str,zv)),'field':list(map(str,F)),'shifted_charpoly':str(t**8),'zeros':[[str(v) for v in p] for p in points]},indent=2)+'\n')
print('Verified the characteristic polynomial and three rational zeros.')

Recorded output

Verified the characteristic polynomial and three rational zeros.

Download check_symbolic.py ↓