#!/usr/bin/env python3
"""
Exact verifier for a counterexample to Conjecture 6.6
("Cyclotomic Catalan") in arXiv:2605.14682v1.

The counterexample is mu=2, n=k=3.
Only integer arithmetic is used.
"""

from itertools import permutations
from math import comb


def avoids_312(p):
    """Return True iff permutation p avoids the pattern 312."""
    n = len(p)
    for i in range(n):
        for j in range(i + 1, n):
            for k in range(j + 1, n):
                # Values have relative order 3,1,2.
                if p[i] > p[k] > p[j]:
                    return False
    return True


def inversions(p):
    return sum(
        1
        for i in range(len(p))
        for j in range(i + 1, len(p))
        if p[i] > p[j]
    )


def polynomial_add(a, b):
    """Polynomials represented as coefficient lists in ascending degree."""
    size = max(len(a), len(b))
    out = [0] * size
    for i, value in enumerate(a):
        out[i] += value
    for i, value in enumerate(b):
        out[i] += value
    while len(out) > 1 and out[-1] == 0:
        out.pop()
    return out


def polynomial_shift(a, exponent):
    return [0] * exponent + a


def q_catalan_triangle(max_n):
    """
    Compute C_{n,k}(q) from Definition 2.2:
      C_{n,0}(q)=q^(n choose 2),
      C_{n,k}=C_{n,k-1}+q^(n-k-1) C_{n-1,k},
    with C_{n-1,k}=0 when k>n-1.
    """
    C = {(0, 0): [1]}
    for n in range(1, max_n + 1):
        C[(n, 0)] = [0] * comb(n, 2) + [1]
        for k in range(1, n + 1):
            value = C[(n, k - 1)]
            if k <= n - 1:
                value = polynomial_add(
                    value,
                    polynomial_shift(C[(n - 1, k)], n - k - 1),
                )
            C[(n, k)] = value
    return C


def evaluate_at_minus_one(coefficients):
    return sum(coef * ((-1) ** degree)
               for degree, coef in enumerate(coefficients))


def main():
    mu = 2
    n = k = 3

    C = q_catalan_triangle(n)
    coefficients = C[(n, k)]
    recurrence_value = evaluate_at_minus_one(coefficients)

    avoiding = [p for p in permutations(range(1, n + 1)) if avoids_312(p)]
    permutation_terms = [(p, inversions(p), (-1) ** inversions(p))
                         for p in avoiding]
    permutation_value = sum(term for _, _, term in permutation_terms)

    conjectured_value = comb(n + 1, (n + 1) // mu) // mu

    print(f"C_{{3,3}}(q) coefficients, low to high degree: {coefficients}")
    print(f"C_{{3,3}}(-1) from recurrence: {recurrence_value}")
    print("312-avoiding permutations and their (-1)^inv weights:")
    for p, inv, weight in permutation_terms:
        print(f"  {p}: inv={inv}, weight={weight}")
    print(f"Sum from permutation definition: {permutation_value}")
    print(f"Conjecture 6.6 predicts: {conjectured_value}")

    assert recurrence_value == -1
    assert permutation_value == recurrence_value
    assert conjectured_value == 3
    assert recurrence_value != conjectured_value

    print("COUNTEREXAMPLE VERIFIED: -1 != 3")


if __name__ == "__main__":
    main()