"""Exact degree-13 witness for the FMS seven-family exhaustiveness claim.

See classification-source-check.md for the irreducibility/primitivity argument.
No assertion about thinness of this example or of the stated families is made.
"""
from pathlib import Path
from hashlib import sha256
import importlib.util
import json
import sympy as s

base = Path(__file__).resolve().parent
spec = importlib.util.spec_from_file_location('fms_exact_checks', base / 'exact_checks.py')
checks = importlib.util.module_from_spec(spec)
spec.loader.exec_module(checks)
x = checks.x
n = 13
p = s.Poly((x + 1) * s.cyclotomic_poly(36, x), x)
q = s.Poly((x - 1)**3 * s.cyclotomic_poly(3, x)
           * s.cyclotomic_poly(6, x) * s.cyclotomic_poly(18, x), x)
assert p.degree() == q.degree() == n and s.gcd(p, q).degree() == 0
assert s.isprime(n)
assert q.eval(1) == q.diff().eval(1) == q.diff().diff().eval(1) == 0
assert q.diff().diff().diff().eval(1) != 0
a, b = checks.companion(p), checks.companion(q)
identity = s.eye(n)
c = a.inv() * b
assert c**2 == identity and (c - identity).rank() == 1
u = (c - identity)[:, -1]
assert u[-1] == -2
assert all(c[:, j] == identity[:, j] for j in range(n - 1))
orbit = s.Matrix.hstack(*[b**j * u for j in range(n)])
observability = s.Matrix.vstack(*[identity[-1, :] * b**j for j in range(n)])
assert orbit.det() != 0 and observability.det() != 0
gram = s.Matrix(n, n, lambda i, j: (b**(j - i) * u)[-1])
oi = orbit.inv()
form = oi.T * gram * oi
assert form == form.T and gram == gram.T
assert a.T * form * a == b.T * form * b == form
assert checks.inertia(form) == [12, 1, 0]
denominator = s.ilcm(*[v.q for v in form])
assert all(v.q == 1 for v in denominator * form)
# An n-dimensional companion matrix is cyclic; its minimal polynomial is Q.
# Triple root 1 therefore proves B nonsemisimple. This also follows explicitly:
assert len((b - identity).nullspace()) == 1

# All P-shapes of the intended seven families at n=13. Dependence on j is
# confined to Q. M1's obvious middle-coordinate typo is corrected generously.
shapes = [('M1', s.cancel((x - 1) * (x**n + 1) / (x + 1))),
          ('M2', (x + 1) * (x**(n - 1) + 1)),
          ('M3', (x + 1)**2 * (x**(n - 2) + 1))]
for family, m, factor in [('N1', n, (x - 1) / (x + 1)),
                          ('N2', n - 1, x - 1),
                          ('N3', n - 1, x + 1),
                          ('N4', n - 2, (x + 1)**2)]:
    for k in s.divisors(m):
        ell = m // k
        shapes.append((f'{family}:k={k},ell={ell}',
                       s.cancel(factor * (x**(ell * (k + 1)) - 1) / (x**ell - 1))))
targets = [p, q, s.Poly(-p.as_expr().subs(x, -x), x),
           s.Poly(-q.as_expr().subs(x, -x), x)]
assert all(s.Poly(expr, x).degree() == n for _, expr in shapes)
assert all(s.Poly(expr, x) not in targets for _, expr in shapes)
assert a.trace() == -1 and b.trace() == 3
output = {'scope': 'Counterexample to exhaustiveness of the intended seven parameter '
                  'families in Theorem 2.6; no thinness verdict.',
          'arithmetic': 'exact rational and integer',
          'p': str(p.as_expr()), 'q': str(q.as_expr()),
          'p_factors': 'Phi_2 * Phi_36', 'q_factors': 'Phi_1^3 * Phi_3 * Phi_6 * Phi_18',
          'degree': n, 'spectrum_gcd': str(s.gcd(p, q).as_expr()),
          'orbit_determinant': str(orbit.det()),
          'observability_determinant': str(observability.det()),
          'form_integer_scale': str(denominator),
          'inertia_positive_negative_zero': checks.inertia(form),
          'gram_first_row': [str(v) for v in gram[0, :]],
          'irreducibility_witness': 'C-I has image span(u) and kernel ker(e_n^T); '
                                   'B-orbit of u and dual B-orbit of e_n^T both span.',
          'primitivity_witness': 'Prime degree 13 forces any nontrivial block system '
                                'to have 1-dimensional blocks. Then B would be monomial '
                                'and hence semisimple, contrary to its cyclic minimal '
                                'polynomial having (x-1)^3.',
          'unmatched_p_shapes': [{'family': label, 'p': str(expr)} for label, expr in shapes],
          'allowed_comparisons': 'P/Q exchange and simultaneous multiplication of roots '
                                 'by -1; any scalar shift into another integral pair is '
                                 'real by the nonzero integer trace, hence is +/-1.',
          'script_sha256': sha256(Path(__file__).read_bytes()).hexdigest()}
(base / 'classification-witness.json').write_text(json.dumps(output, indent=2) + '\n')
print(json.dumps({'exact_checks': 'passed', 'degree': n, 'signature': [12, 1],
                  'excluded_family_p_shapes': len(shapes)}))