LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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.

Small anticonnected components yield a complete blockade

Statement

Let $G$ be a graph on $n$ vertices, and let $k \geq 2$ be an integer. Suppose every anticonnected component of $G$ has size less than $n / k$ . Then $G$ contains a complete blockade of length at least $k / 2$ and width at least $n / (2 k)$ .

Facts & Assumptions

Given: A graph $G$ on $n$ vertices and an integer $k \geq 2$ such that every anticonnected component of $G$ has size less than $n / k$ .

[L1]

Distinct anticonnected components are complete to one another (Distinct connected components are anticomplete, and distinct anticonnected components are complete).

Proof

technique · direct packing

1.1

Partition the anticonnected components into a minimum number of unions $S_{0}, \dots, S_{r}$ , each of size less than $n / k$ , and order them so that $∣ S_{0} ∣ \leq \dots \leq ∣ S_{r} ∣$ . Since their union has size $n$ , one has $r + 1 > k$ .

givenchoosealgebra

2.1

For every $i \geq 1$ , minimality gives $∣ S_{i - 1} ∣ + ∣ S_{i} ∣ \geq n / k$ ; otherwise these two parts could be merged. The ordering then yields $∣ S_{i} ∣ \geq n / (2 k)$ . Thus $S_{1}, \dots, S_{r}$ contain at least $k$ nonempty blocks of width at least $n / (2 k)$ , and [L1] makes every cross-pair complete. Selecting any $⌈ k / 2 ⌉$ of them proves the statement.

step 1.1L1algebra∎

Depends on

Used by

Dependency tree · two levels

10 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

Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. VII. The five-vertex path, Lemma 4.1 (standard reference, not scraped)