# -*- coding: utf-8 -*-
"""
PHASE 5 — FULL SYMBOLIC determinant of the 22x22 Jacobian.

The chain-factorization already proves det J == 1; this attempts the direct
symbolic computation as a third, fully independent proof path.
Strategy: fraction-free Gaussian elimination over the polynomial ring (Bareiss)
via sympy's polys-based det on a sparse matrix.
"""
import sympy as sp
import json, time

t0 = time.time()
art = json.load(open('post-jc-program/degree3_counterexample.json', encoding='utf-8'))
V = [sp.Symbol(s) for s in art["variables"]]
F = [sp.sympify(s) for s in art["components"]]
J = sp.Matrix(F).jacobian(V)

d = sp.expand(J.det(method='berkowitz')) if False else None
# Bareiss is usually far better for sparse polynomial matrices:
d = sp.expand(J.det(method='bareiss'))
dt = round(time.time() - t0, 2)
print(f"symbolic det (bareiss, {dt}s): {d}")
ok = (d == 1)
print(f"[{'PASS' if ok else 'FAIL'}] FULL SYMBOLIC det J == 1 identically over Q[{len(V)} vars]")
json.dump({"symbolic_det": str(d), "method": "bareiss fraction-free", "pass": bool(ok),
           "elapsed_sec": dt},
          open('post-jc-program/symbolic_det_report.json', 'w', encoding='utf-8'), indent=2)