LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

At most $k$ cyclic intervals of length $k$ in a cyclic order are pairwise intersecting when the ground-set size is at least $2 k$

Statement

Let $1 \leq k$ and $n \geq 2 k$ , and place an $n$ -element set in a cyclic order. Among its $n$ cyclic intervals of length $k$ , every pairwise intersecting family has at most $k$ members.

Facts & Assumptions

Given: Natural numbers $1 \leq k$ and $n \geq 2 k$ , a cyclic order $(a_{0}, \dots, a_{n - 1})$ , and a pairwise intersecting family $I$ of its length- $k$ cyclic intervals, with indices read modulo $n$ .

[F1]

A family is intersecting when every two of its members have nonempty intersection (Intersecting uniform families of finite sets).

Proof

technique · direct

1.1

If $I$ is empty there is nothing to prove. Otherwise rotate the notation so that $I_{0} : = {a_{0}, \dots, a_{k - 1}}$ belongs to $I$ .

given

1.2

For each $j \in {1, \dots, k - 1}$ , the interval starting at $a_{j}$ and the interval starting at $a_{j - k}$ are disjoint: the latter ends at $a_{j - 1}$ and the former begins at $a_{j}$ , and together they use two adjacent blocks of $k$ positions without wrapping into each other because $n \geq 2 k$ .

given

2.1

Every other length- $k$ interval in $I$ must intersect $I_{0}$ . Since $n \geq 2 k$ , its starting position is therefore one of $1, \dots, k - 1$ or one of $n - k + 1, \dots, n - 1$ .

step 1.1F1

3.1

Thus $I$ contains at most one interval from each of the $k - 1$ disjoint pairs in step 1.2, in addition to $I_{0}$ . Hence $∣ I ∣ \leq 1 + (k - 1) = k$ .

step 2.1step 1.2F1∎

Depends on

Intersecting uniform families of finite sets

Used by

Erdős-Ko-Rado theorem: for 1≤ k and n≥ 2k, an intersecting family of k-subsets of an n-set has size at most C(n-1, k-1), and a star attains the bound Theorem

Dependency tree · two levels

2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Erdős-Ko-Rado theorem (Wikipedia) (standard reference, not scraped)

At most kk cyclic intervals of length kk in a cyclic order are pairwise intersecting when the ground-set size is at least 2k2k