"""Shared exact rational matrix helpers for the upper-bound certificates.

Imported by verify_ab_good_domains.py. This module defines six-variable
quadratic forms and an LDL^T checker; it has no standalone certificate.
Run verify_global.py or verify_all.py for the complete verification.
"""
from fractions import Fraction as F
from pathlib import Path
import json
N=6

def add(*terms):return [[sum(c*A[i][j] for c,A in terms) for j in range(N)] for i in range(N)]
def outer(a,b):return [[v*w for w in b] for v in a]
def sy(a,b):return add((F(1,2),outer(a,b)),(F(1,2),outer(b,a)))
def vs(*terms):return [sum(c*a[i] for c,a in terms) for i in range(N)]
def pd(A):
 L=[[F(i==j) for j in range(N)] for i in range(N)];D=[]
 for j in range(N):
  p=A[j][j]-sum(L[j][k]**2*D[k] for k in range(j));assert p>0,(j,p);D.append(p)
  for i in range(j+1,N):L[i][j]=(A[i][j]-sum(L[i][k]*L[j][k]*D[k] for k in range(j)))/p
 assert all(A[i][j]==sum(L[i][k]*D[k]*L[j][k] for k in range(N)) for i in range(N) for j in range(N))
E=[[F(i==j) for j in range(N)] for i in range(N)]
x,y,z,w,bal,r=E;ell=vs((1,x),(1,y),(1,z),(1,w));q=vs((F(1,2),x),(-1,bal));d=vs((F(1,2),x),(1,bal))
base=[[F([F(1,4),1,F(1,2),1,1,0][i]) if i==j else F(0) for j in range(N)] for i in range(N)]
K=add((F(1,2),outer(q,q)),(F(-1,2),outer(r,r)))
fR=add((1,sy(r,vs((1,x),(1,z),(-3,y)))),(-3,outer(r,r)))
fT=add((1,sy(r,vs((F(7,2),q),(-1,z),(2,y)))),(F(-23,8),outer(r,r)),(F(-1,2),outer(q,q)))