Lean 4 / Mathlib verifier: polynomial map C^3->C^3 with constant Jacobian -2 sending 3 distinct points to (-1/4,0,0)

JacobianCounterexample.lean

/-
  Jacobian "counterexample" verifier.

  The map  F : ℂ³ → ℂ³  (here checked over ℚ ⊂ ℂ; all data is rational)

    F₀ = (1+xy)³ z + y² (1+xy) (4+3xy)
    F₁ = y + 3x (1+xy)² z + 3x y² (4+3xy)
    F₂ = 2x − 3x² y − x³ z

  Claimed facts, machine-verified below:

    (1) det (Jacobian F) = −2   (a constant, hence nonzero everywhere)
    (2) F sends the three DISTINCT points
            (0,  0,   −1/4)
            (1, −3/2,  13/2)
            (−1, 3/2,  13/2)
        all to the single point (−1/4, 0, 0).

  (1)+(2) ⇒ F has nonzero constant Jacobian yet is not injective.

  Requires Mathlib. Variables: X 0 = x, X 1 = y, X 2 = z.
-/
import Mathlib

open MvPolynomial

noncomputable section
namespace JacobianCounterexample

/-- Work in the polynomial ring ℚ[x, y, z]. -/
abbrev R := MvPolynomial (Fin 3) ℚ

def x : R := X 0
def y : R := X 1
def z : R := X 2

/-- `u = 1 + x y`. Constants are `C _` so `pderiv` kills them cleanly. -/
def u : R := C 1 + x * y
/-- `w = 4 + 3 x y`. -/
def w : R := C 4 + C 3 * x * y

/-- The three components of the map. -/
def F0 : R := u ^ 3 * z + y ^ 2 * u * w
def F1 : R := y + C 3 * x * u ^ 2 * z + C 3 * x * y ^ 2 * w
def F2 : R := C 2 * x - C 3 * x ^ 2 * y - x ^ 3 * z

/-! ### Part 1 — the Jacobian determinant is the constant −2 -/

/-- Jacobian matrix `J i j = ∂Fᵢ/∂xⱼ`, entries computed by Mathlib's `pderiv`. -/
def J : Matrix (Fin 3) (Fin 3) R :=
  !![pderiv 0 F0, pderiv 1 F0, pderiv 2 F0;
     pderiv 0 F1, pderiv 1 F1, pderiv 2 F1;
     pderiv 0 F2, pderiv 1 F2, pderiv 2 F2]

/-- **The Jacobian determinant equals −2**, as a polynomial identity in ℚ[x,y,z].
    Since −2 ≠ 0, the map has a nonvanishing constant Jacobian. -/
theorem jacobian_det : J.det = -2 := by
  rw [J, Matrix.det_fin_three_of]
  -- unfold the map and turn every `^` into repeated `*`
  simp only [F0, F1, F2, u, w, x, y, z, pow_succ, pow_zero, one_mul]
  -- differentiate: pderiv is additive/Leibniz; it kills the `C _` constants
  simp only [pderiv_add, pderiv_sub, pderiv_mul, pderiv_C, pderiv_X,
             Pi.single_apply, map_add, map_sub, map_mul]
  -- normalize the surviving constants  C 1 = 1, C 2 = 2, C 3 = 3, C 4 = 4
  simp only [map_one, map_ofNat]
  ring

/-! ### Part 2 — three distinct points share the image (−1/4, 0, 0) -/

/-- Point P₀ = (0, 0, −1/4) ↦ (−1/4, 0, 0). -/
theorem image_P0 :
    eval ![0, 0, (-1/4 : ℚ)] F0 = -1/4 ∧
    eval ![0, 0, (-1/4 : ℚ)] F1 = 0 ∧
    eval ![0, 0, (-1/4 : ℚ)] F2 = 0 := by
  refine ⟨?_, ?_, ?_⟩ <;>
  · simp only [F0, F1, F2, u, w, x, y, z, map_add, map_sub, map_mul, map_pow,
               eval_C, eval_X, Matrix.cons_val_zero, Matrix.cons_val_one,
               Matrix.head_cons, Matrix.cons_val, Matrix.tail_cons]
    norm_num

/-- Point P₁ = (1, −3/2, 13/2) ↦ (−1/4, 0, 0). -/
theorem image_P1 :
    eval ![1, -3/2, (13/2 : ℚ)] F0 = -1/4 ∧
    eval ![1, -3/2, (13/2 : ℚ)] F1 = 0 ∧
    eval ![1, -3/2, (13/2 : ℚ)] F2 = 0 := by
  refine ⟨?_, ?_, ?_⟩ <;>
  · simp only [F0, F1, F2, u, w, x, y, z, map_add, map_sub, map_mul, map_pow,
               eval_C, eval_X, Matrix.cons_val_zero, Matrix.cons_val_one,
               Matrix.head_cons, Matrix.cons_val, Matrix.tail_cons]
    norm_num

/-- Point P₂ = (−1, 3/2, 13/2) ↦ (−1/4, 0, 0). -/
theorem image_P2 :
    eval ![-1, 3/2, (13/2 : ℚ)] F0 = -1/4 ∧
    eval ![-1, 3/2, (13/2 : ℚ)] F1 = 0 ∧
    eval ![-1, 3/2, (13/2 : ℚ)] F2 = 0 := by
  refine ⟨?_, ?_, ?_⟩ <;>
  · simp only [F0, F1, F2, u, w, x, y, z, map_add, map_sub, map_mul, map_pow,
               eval_C, eval_X, Matrix.cons_val_zero, Matrix.cons_val_one,
               Matrix.head_cons, Matrix.cons_val, Matrix.tail_cons]
    norm_num

/-- The three source points are pairwise distinct (so the fibre over
    (−1/4,0,0) has ≥ 3 points ⇒ `F` is not injective). -/
theorem points_distinct :
    (![0, 0, (-1/4 : ℚ)] : Fin 3 → ℚ) ≠ ![1, -3/2, 13/2] ∧
    (![0, 0, (-1/4 : ℚ)] : Fin 3 → ℚ) ≠ ![-1, 3/2, 13/2] ∧
    (![1, -3/2, (13/2 : ℚ)] : Fin 3 → ℚ) ≠ ![-1, 3/2, 13/2] := by
  refine ⟨?_, ?_, ?_⟩ <;>
    · intro h
      have := congrFun h 0
      norm_num [Matrix.cons_val_zero] at this

end JacobianCounterexample