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.

Failure of the first and third property-(*) outcomes forces one small-block structural partition

Statement

Under the hypotheses of the preceding two lemmas, suppose that $G$ has no clique or stable set of size $w^{c / 2}$ and no pure $(ℓ, w / ℓ^{2})$ -blockade. Then for some $i \in [ℓ]$ , $∣ X_{i} ∣ \geq w / 2, t_{i} \geq ℓ, ∣ A_{j}^{i} ∣ \leq w / (2 ℓ) (j \in [t_{i}]) .$

Facts & Assumptions

Given: A structural partition, $c \in (0, 1]$ , and failure of the first and third displayed outcomes.

[F1]

A $Y_{i}$ of size at least $w / 2$ yields a clique or stable set of size at least $w^{c / 2}$ (A large Y-part in a structural comb partition yields the clique-or-stable-set outcome).

[F2]

A selected block of size at least $w / (2 ℓ)$ in every partition yields a pure $(ℓ, w / ℓ^{2})$ -blockade (A transversal of wide structural blocks yields the pure blockade outcome).

[F3]

Each $B_{i}$ is the disjoint union of $X_{i}$ and $Y_{i}$ , and $(A_{1}^{i}, \dots, A_{t_{i}}^{i})$ partitions $X_{i}$ (The structural comb-partition hypothesis).

Proof

technique · contradiction

1.1F1F3

By the contrapositive of [F1], every $Y_{i}$ has size less than $w / 2$ . Since $∣ B_{i} ∣ \geq w$ and $B_{i} = X_{i} \dot{\cup} Y_{i}$ by [F3], every $X_{i}$ has size at least $w / 2$ .

1.2F2assume-contradischarge-contradiction

Suppose every partition had a block of size at least $w / (2 ℓ)$ . Then [F2] would give the excluded pure blockade. Hence some index $i$ has every $A_{j}^{i}$ of size less than $w / (2 ℓ)$ , and thus at most that bound.

2.1step 1.1step 1.2F3algebradischarge-contradiction∎

For this $i$ , [F3] and step 1.1 give $w / 2 \leq ∣ X_{i} ∣ = \sum_{j = 1}^{t_{i}} ∣ A_{j}^{i} ∣ \leq t_{i} w / (2 ℓ)$ , hence $t_{i} \geq ℓ$ .

Depends on

Used by

The structural comb-partition criterion implies property (*) Theorem

Dependency tree · two levels

15 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, proof after Claim 5.1.1 (standard reference, not scraped)