# Analyse the m=3 tables computed by m3_table.py:
#  (i) Lemma 3: N(lambda*(b), b') != 0  =>  b' >=_dom b;  (ii) Lemma 2: N(lambda*(b), b) >= 1;
#  (iii) the |b| = 4 table equals the polynomial table proved by hand in S1-3 (= C-6's table);
#  (iv) every |b| <= 5 entry equals the closed form listed below (proved for |b| <= 4 and
#       for the three corrected entries; for |b| = 5 a fit, checked at every computed q).
import json, glob, sys, os
D = '/private/tmp/claude-501/-Users-miltonlin-Projects-Trees/f0f18b89-aa0d-4ce6-93d2-78c269eb7d7d/scratchpad/salvage/S1/'
data = {}
for f in glob.glob(D + 'm3_table_q*_d*.json'):
    q = int(os.path.basename(f).split('_')[2][1:])
    for col, rows in json.load(open(f)).items():
        bp = tuple(eval(col))
        for lam, v in rows.items():
            data.setdefault(q, {})[(tuple(eval(lam)), bp)] = v
def dom(x, y):  # x >=_dom y
    sx = sy = 0
    for a, b in zip(x, y):
        sx += a; sy += b
        if sx < sy: return False
    return True
P = {  # (row lambda, column b') -> closed form in q
 ((1,0,0,0,0,0),(1,0,0)): lambda q: q+1,
 ((2,0,0,0,0,0),(2,0,0)): lambda q: q*(q+1), ((1,1,0,0,0,0),(2,0,0)): lambda q: 1,
 ((1,1,0,0,0,0),(1,1,0)): lambda q: (q+1)*(q*q+1),
 ((3,0,0,0,0,0),(3,0,0)): lambda q: q**2*(q+1), ((2,1,0,0,0,0),(3,0,0)): lambda q: q+1,
 ((2,1,0,0,0,0),(2,1,0)): lambda q: q**2*(q+1)**2, ((1,1,1,0,0,0),(2,1,0)): lambda q: q+1,
 ((1,1,1,0,0,0),(1,1,1)): lambda q: (q+1)*(q*q+1)*(q**3+1),
 # |b| = 4 (proved by hand in S1-3; equals C-6)
 ((4,0,0,0,0,0),(4,0,0)): lambda q: q**3*(q+1), ((3,1,0,0,0,0),(4,0,0)): lambda q: q*(q+1), ((2,2,0,0,0,0),(4,0,0)): lambda q: 1,
 ((3,1,0,0,0,0),(3,1,0)): lambda q: q**3*(q+1)**2, ((2,2,0,0,0,0),(3,1,0)): lambda q: q*(q*q-1), ((2,1,1,0,0,0),(3,1,0)): lambda q: (q+1)**2,
 ((2,2,0,0,0,0),(2,2,0)): lambda q: q**3*(q+1)*(q*q+1), ((2,1,1,0,0,0),(2,2,0)): lambda q: q*(q+1)*(q*q+1), ((1,1,1,1,0,0),(2,2,0)): lambda q: 1,
 ((2,1,1,0,0,0),(2,1,1)): lambda q: q**3*(q+1)**2*(q*q+1), ((1,1,1,1,0,0),(2,1,1)): lambda q: (q+1)*(q*q+1),
 # |b| = 5 (fits)
 ((5,0,0,0,0,0),(5,0,0)): lambda q: q**4*(q+1), ((4,1,0,0,0,0),(5,0,0)): lambda q: q**2*(q+1), ((3,2,0,0,0,0),(5,0,0)): lambda q: q+1,
 ((4,1,0,0,0,0),(4,1,0)): lambda q: q**4*(q+1)**2, ((3,2,0,0,0,0),(4,1,0)): lambda q: q*(q-1)*(q+1)**2,
 ((3,1,1,0,0,0),(4,1,0)): lambda q: q*(q+1)**2, ((2,2,1,0,0,0),(4,1,0)): lambda q: q+1,
 ((3,2,0,0,0,0),(3,2,0)): lambda q: q**5*(q+1)**2, ((3,1,1,0,0,0),(3,2,0)): lambda q: q**4*(q+1),
 ((2,2,1,0,0,0),(3,2,0)): lambda q: q**2*(q+1)**2, ((2,1,1,1,0,0),(3,2,0)): lambda q: q+1,
 ((3,1,1,0,0,0),(3,1,1)): lambda q: q**4*(q+1)**2*(q*q+1), ((2,2,1,0,0,0),(3,1,1)): lambda q: q*(q-1)*(q+1)**2*(q*q+1),
 ((2,1,1,1,0,0),(3,1,1)): lambda q: (q+1)**2*(q*q+1),
 ((2,2,1,0,0,0),(2,2,1)): lambda q: q**5*(q+1)**2*(q*q+1), ((2,1,1,1,0,0),(2,2,1)): lambda q: q**2*(q+1)**2*(q*q+1),
 ((1,1,1,1,1,0),(2,2,1)): lambda q: q+1,
}
allok = True
for q in sorted(data):
    T = data[q]
    cols = sorted(set(bp for (_, bp) in T))
    l3 = l2 = fit = True
    for d in range(1, 6):
        bs = [b for b in cols if sum(b) == d]
        for b in bs:
            lam = b + (0, 0, 0)
            if T.get((lam, b), 0) < 1: l2 = False
            for bp in bs:
                if T.get((lam, bp), 0) and not dom(bp, b): l3 = False
    keys = set(T) | set(k for k in P if k[1] in cols)
    for k in keys:
        if T.get(k, 0) != (P[k](q) if k in P else 0):
            fit = False; print('  q=%d mismatch at' % q, k, T.get(k, 0), P[k](q) if k in P else 0)
    print('q=%d: columns %s ... Lemma 2 diagonal >= 1: %s; Lemma 3 zero pattern: %s; all entries = closed forms: %s' % (q, len(cols), l2, l3, fit))
    allok &= l2 and l3 and fit
print('ALL OK:', allok)