"""Checks out/certificates.json on its own: no imports from the other scripts.
For every case and EVERY line count L >= t (up to C(n,2)/3), it recomputes
which splits are allowed and verifies the certificate in exact fractions.

  python3 check.py
"""
import json, sys
from fractions import Fraction as F
from math import comb

# most lines among k points of AG(3,3), k = 0..27: OEIS A380167 (and third.c)
g = [0, 0, 0, 1, 1, 2, 3, 5, 8, 12, 12, 13, 14, 16, 19, 23, 26, 30, 36, 41,
     47, 54, 62, 71, 81, 92, 104, 117]

def splits(n, L):
    for a in range(min(n, 27) + 1):
        for b in range(min(n - a, a) + 1):
            c = n - a - b
            if b >= c and g[a] + g[b] + g[c] + min(a * b, b * c, c * a) >= L:
                yield sum(comb(k, 2) for k in (a, b, c)), sum(comb(k, 3) for k in (a, b, c))

def holds(cert, L):
    d, n = cert['d'], cert['n']
    N, c1, c2 = (3 ** d - 1) // 2, (3 ** (d - 1) - 1) // 2, (3 ** (d - 2) - 1) // 2
    A, B = c1 * comb(n, 2), c2 * comb(n, 3) + (c1 - c2) * L
    pts = list(splits(n, L))
    if cert['kind'] == 'none':
        return not pts
    if not pts:
        return True
    if cert['kind'] == 'pairs':
        return not min(P for P, T in pts) * N <= A <= max(P for P, T in pts) * N
    if cert['kind'] == 'line':
        u, v = F(cert['u']), F(cert['v'])
        return all(T <= u + v * P for P, T in pts) and N * u + v * A < B
    return False

bad = 0
for cert in json.load(open(sys.argv[1] if len(sys.argv) > 1 else 'out/certificates.json')):
    ok = all(holds(cert, L) for L in range(cert['t'], comb(cert['n'], 2) // 3 + 1))
    bad += not ok
    if cert['d'] == 4 or not ok:
        print(f"d={cert['d']} n={cert['n']:2d}: at most {cert['t'] - 1:3d} lines  "
              f"{cert['kind']:5s} {'PASS' if ok else 'FAIL'}")
print('all certificates pass' if not bad else f'{bad} FAILED')