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