"""Exact AB top-capacity boundary certificate, rational arithmetic only."""
from fractions import Fraction as F
from pathlib import Path
import json
N=6
E=[[F(int(i==j))for j in range(N)]for i in range(N)]
x,y,z,w,b,r=E
ell=[x[i]+y[i]+z[i]+w[i]for i in range(N)]
def V(*args):return [sum(c*a[i]for c,a in args)for i in range(N)]
def out(a,b):return [[u*v for v in b]for u in a]
def A(*args):return [[sum(c*a[i][j]for c,a in args)for j in range(N)]for i in range(N)]
def sy(a,b):return A((F(1,2),out(a,b)),(F(1,2),out(b,a)))
q=V((F(1,2),x),(-1,b));h=V((2,b));d=V((1,q),(1,h))
base=A((F(1,4),out(x,x)),(1,out(y,y)),(F(1,2),out(z,z)),(1,out(w,w)),(1,out(b,b)))
K=A((F(1,2),out(q,q)),(F(-1,2),out(r,r)))
fR=A((1,sy(r,V((1,x),(1,z),(-3,y)))),(-3,out(r,r)))
NN=sy(V((1,q),(-1,r)),V((2,r),(-1,q)))
forms=[('q-r',V((1,q),(-1,r))),('r-.8q',V((1,r),(F(-4,5),q))),('h-.3q',V((1,h),(F(-3,10),q))),('1.25q-h',V((F(5,4),q),(-1,h))),('3z/8-y',V((F(3,8),z),(-1,y))),('13q/20-y',V((F(13,20),q),(-1,y))),('3q-z',V((3,q),(-1,z))),('w-y',V((1,w),(-1,y))),('6w-r-z',V((6,w),(-1,r),(-1,z))),('w-.1ell',V((1,w),(F(-1,10),ell))),('r-.1ell',V((1,r),(F(-1,10),ell))),('z-.2ell',V((1,z),(F(-1,5),ell))),('q-2w',V((1,q),(-2,w)))]+[(name,v)for name,v in zip(['x','y','z','w','b','r'],E)]

def build(kind):
 t=r if kind=='r_le_2w'else V((2,w))
 g=A((1,sy(t,V((F(3,2),q),(-1,r),(-1,z),(2,y)))),(F(-7,8),out(t,t)),(F(1,2),out(q,q)))
 fs=forms+[(kind,V((2,w),(-1,r)) if kind=='r_le_2w'else V((1,r),(-2,w)))]
 terms=[A((-1,K),(-1,fR)),A((-3,K),(-1,g)),A((-1,NN))]+[A((-1,sy(ell,v)))for _,v in fs]+[A((-1,out(ell,ell)))]
 return A((1,base),(1,K)),terms,[n for n,_ in fs]

def ldl(H):
 L=[[F(int(i==j))for j in range(N)]for i in range(N)];D=[]
 for i in range(N):
  v=H[i][i]-sum(L[i][k]**2*D[k]for k in range(i));assert v>0,(i,v);D.append(v)
  for j in range(i+1,N):L[j][i]=(H[j][i]-sum(L[j][k]*L[i][k]*D[k]for k in range(i)))/v
 return D

def check(row):
 base,terms,names=build(row['kind']);pars=list(map(F,row['parameters']));br,bt=pars[:2];p=1-br-bt
 assert len(pars)==len(terms) and all(v>=0 for v in pars)
 assert F(5,8)*br>=3*bt and p>=5*bt and p>=2*bt and p+bt>=F(3,2)*br
 assert pars[-1]==1-2*F(row['gamma'])
 H=A((1,base),*[(v,t)for v,t in zip(pars,terms)]);piv=ldl(H)
 print('PASS',row['kind'],'gamma <=',row['gamma'],'weights',p,br,bt,'minimum LDL',float(min(piv)))
 return F(row['gamma'])
if __name__=='__main__':
 data=json.loads(Path(__file__).with_name('ab-boundary-certificate.json').read_text())
 assert len(data['cases'])==2 and {row['kind']for row in data['cases']}=={'r_le_2w','r_ge_2w'}
 ans=[check(row)for row in data['cases']];print('PASS AB q>=2w boundary gamma <=',max(ans),float(max(ans)))