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.

A transversal of wide structural blocks yields the pure blockade outcome

Statement

Assume a structural comb partition for an $(ℓ, w)$ -comb with $ℓ, w \geq 4$ . If for every $i \in [ℓ]$ one can choose a block $A_{j_{i}}^{i}$ with $∣ A_{j_{i}}^{i} ∣ \geq w / (2 ℓ)$ , then $(A_{j_{1}}^{1}, \dots, A_{j_{ℓ}}^{ℓ})$ is a pure $(ℓ, w / ℓ^{2})$ -blockade.

Facts & Assumptions

Given: One selected partition block $A_{j_{i}}^{i}$ of size at least $w / (2 ℓ)$ for every $i \in [ℓ]$ .

[F1]

Every partition block $A_{j}^{i}$ is pure to every vertex in every other comb block $B_{k}$ with $k \neq i$ (The structural comb-partition hypothesis).

[F2]

A blockade is a sequence of pairwise disjoint nonempty sets with the stated length and width bounds; a pure blockade has every pair of blocks pure (Blockades, their length, their width, and their support, Complete, anticomplete, pure, weakly sparse, and $x$ -sparse blockades).

Proof

technique · direct

1.1

The selected sets lie in distinct, hence disjoint, comb blocks. Fix $i \neq k$ . By [F1], every vertex of $A_{j_{k}}^{k} \subseteq B_{k}$ is individually complete or anticomplete to $A_{j_{i}}^{i}$ . If two such vertices had opposite relations, then any vertex of the nonempty set $A_{j_{i}}^{i}$ would be mixed on $A_{j_{k}}^{k}$ , contradicting [F1] applied with $i$ and $k$ reversed. Hence the relation is uniform and the pair of selected blocks is pure.

2.1

Thus the selected sequence is a pure blockade of length $ℓ$ and width at least $w / (2 ℓ)$ by [F2].

step 1.1F2

3.1

Since $ℓ \geq 4$ , $2 ℓ \leq ℓ^{2}$ , so $w / (2 ℓ) \geq w / ℓ^{2}$ . Step 2.1 and [F2] give the asserted pure $(ℓ, w / ℓ^{2})$ -blockade.

step 2.1F2algebra∎

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

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