LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $2k$

Statement

Let $1\le k$ and $n\ge2k$ , 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\le k$ and $n\ge2k$ , a cyclic order $(a_0,\ldots,a_{n-1})$ , and a pairwise intersecting family $\mathcal 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 $\mathcal I$ is empty there is nothing to prove. Otherwise rotate the notation so that $I_0:=\{a_0,\ldots,a_{k-1}\}$ belongs to $\mathcal I$ .

given

1.2

For each $j\in\{1,\ldots,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\ge2k$ .

given

2.1

Every other length- $k$ interval in $\mathcal I$ must intersect $I_0$ . Since $n\ge2k$ , its starting position is therefore one of $1,\ldots,k-1$ or one of $n-k+1,\ldots,n-1$ .

step 1.1F1

3.1

Thus $\mathcal I$ contains at most one interval from each of the $k-1$ disjoint pairs in step 1.2, in addition to $I_0$ . Hence $|\mathcal I|\le1+(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 binomn-1k-1, and a star attains the bound Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 11 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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

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