LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

Homogeneous sets in pure-blockade patterns lift to complete or anticomplete blockades

Statement

Let $(A_{1}, \dots, A_{t})$ be a pure blockade of width at least $s > 0$ , and let $\emptyset \neq S \subseteq [t]$ . If $S$ is a clique in its pattern graph, the blocks indexed by $S$ form a complete $(∣ S ∣, s)$ -blockade; if $S$ is a stable set, they form an anticomplete $(∣ S ∣, s)$ -blockade.

Facts & Assumptions

Given: A pure blockade $(A_{1}, \dots, A_{t})$ of width at least $s$ and a nonempty clique or stable set $S$ in its pattern graph.

[F1]

Pattern vertices $i, j$ are adjacent exactly when $A_{i}$ is complete to $A_{j}$ ; the blockade's purity makes the pattern well defined (The pattern graph of a pure blockade).

[F2]

Complete and anticomplete blockades require every distinct pair of blocks to be respectively complete and anticomplete (Complete, anticomplete, pure, weakly sparse, and $x$ -sparse blockades).

[F3]

The original blocks are pairwise disjoint and nonempty, and width at least $s$ means every selected block has at least $s$ vertices (Blockades, their length, their width, and their support).

Proof

technique · cases

1.1

The selected sequence has $∣ S ∣$ pairwise disjoint nonempty blocks of size at least $s$ by [F3].

2.1

If $S$ is a clique, each pair of its pattern vertices is adjacent, so [F1] makes every selected pair complete. Thus [F2] makes the sequence a complete $(∣ S ∣, s)$ -blockade.

assume-case cliqueF1F2step 1.1

2.2

If $S$ is a stable set, no selected pattern pair is adjacent. Since the original blockade is pure, [F1] makes every selected pair anticomplete; [F2] therefore gives an anticomplete $(∣ S ∣, s)$ -blockade.

assume-case stableF1F2step 1.1

3.1

The clique and stable-set cases exhaust the stated alternatives.

step 2.1step 2.2cases-exhaustive∎

Depends on

Used by

A wide integral geometric layer forces the complete-or-anticomplete property-(*) blockade Lemma

Dependency tree · two levels

5 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

Huang, Ju, and Zhou, Erdős–Hajnal beyond the five-vertex path, Claim 5.1.2 (standard reference, not scraped)