"""Exact Farkas certificates for the counting bound (see bound.py), one per
case, written to out/certificates.json for check.py to verify on its own.

In AG(d,3), to rule out n points holding t or more lines: each parallel class
of hyperplanes splits the points as (a, b, c), with P = sum C(k,2) and
T = sum C(k,3) over the parts. Summed over the N = (3^d-1)/2 classes,
P adds up to A = c1*C(n,2) and T to at least B = c2*C(n,3) + (c1-c2)*t.
Only splits with gsub(a)+gsub(b)+gsub(c)+min(ab,bc,ca) >= t can occur.
A certificate is one of:
  none   no split is allowed;
  pairs  A/N lies outside [min P, max P] over the allowed splits;
  line   rationals u, v with T <= u + v*P for every allowed split and
         N*u + v*A < B (so summing over the classes can't reach B).

  python3 certify.py > out/certificates.json
"""
import json
from fractions import Fraction as F
from math import comb
from bound import G3, built

def allowed(d, gsub, n, t):
    return [(a, b, n - a - b) for a in range(n + 1) for b in range(n - a + 1)
            if a >= b >= n - a - b and a < len(gsub)
            and gsub[a] + gsub[b] + gsub[n - a - b] + min(a * b, b * (n - a - b), a * (n - a - b)) >= t]

def certificate(d, gsub, n, t):
    N, c1, c2 = (3 ** d - 1) // 2, (3 ** (d - 1) - 1) // 2, (3 ** (d - 2) - 1) // 2
    ok = allowed(d, gsub, n, t)
    if not ok:
        return {'kind': 'none'}
    pts = sorted({(sum(comb(k, 2) for k in p), sum(comb(k, 3) for k in p)) for p in ok})
    A, B = c1 * comb(n, 2), c2 * comb(n, 3) + (c1 - c2) * t
    x0 = F(A, N)
    if not pts[0][0] <= x0 <= pts[-1][0]:
        return {'kind': 'pairs'}
    # the lowest line above every point, at x0: an edge of the upper hull
    best = None
    for P1, T1 in pts:
        for P2, T2 in pts:
            if P1 <= x0 <= P2 and P1 < P2:
                v = F(T2 - T1, P2 - P1)
                u = T1 - v * P1
                if all(T <= u + v * P for P, T in pts) and (best is None or N * u + v * A < best[0]):
                    best = (N * u + v * A, u, v)
    if best is None or not best[0] < B:
        return {'kind': 'fails'}
    return {'kind': 'line', 'u': str(best[1]), 'v': str(best[2]), 'reach': str(best[0]), 'need': B}

def main():
    out = []
    for n in range(3, 48):  # four features: the bound is f(n) for n <= 47
        f = built(n)
        out.append({'d': 4, 'n': n, 't': f + 1, **certificate(4, G3, n, f + 1)})
    for d in range(5, 13):  # more features, n <= 27, parts bounded by G3 (induction)
        for n in range(3, 28):
            out.append({'d': d, 'n': n, 't': G3[n] + 1, **certificate(d, G3, n, G3[n] + 1)})
    print(json.dumps(out, indent=0))

if __name__ == '__main__':
    main()