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