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 large Y-part in a structural comb partition yields the clique-or-stable-set outcome

Statement

Assume $(F_{1}, F_{2}; H)$ satisfies the structural comb-partition hypothesis. Let $c \in (0, 1]$ be an Erdős–Hajnal constant for both $F_{1}$ -free and $F_{2}$ -free graphs. If an $(ℓ, w)$ -comb with $ℓ, w \geq 4$ has a structural partition and $∣ Y_{i} ∣ \geq w / 2$ for some $i$ , then $G$ has a clique or stable set of size at least $w^{c / 2}$ .

Facts & Assumptions

Given: The structural partition, $c \in (0, 1]$ , $w \geq 4$ , and an index $i$ with $∣ Y_{i} ∣ \geq w / 2$ .

[F1]

The structural hypothesis makes $Y_{i}$ $F_{1}$ -free (The structural comb-partition hypothesis).

[F2]

An Erdős–Hajnal constant $c$ gives a clique or stable set of size at least $∣ V (Q) ∣^{c}$ in every nonempty $F_{1}$ -free graph $Q$ (The Erdős–Hajnal property and an Erdős–Hajnal constant for a hereditary graph class).

[F3]

For positive bases, real powers obey the product and iterated-power laws (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

Proof

technique · direct

1.1

Since $∣ Y_{i} ∣ \geq w / 2 > 0$ , [F1] and [F2] give a clique or stable set in $G [Y_{i}]$ , hence in $G$ , with at least $(w / 2)^{c}$ vertices.

F1F2

1.2

As $w \geq 4$ , we have $w / 2 \geq \sqrt{w} > 0$ ; raising this inequality to the positive exponent $c$ and using [F3] gives $(w / 2)^{c} \geq (\sqrt{w})^{c} = w^{c / 2}$ .

F3algebra

2.1

The set from step 1.1 therefore has at least $w^{c / 2}$ vertices, which is the claimed clique-or-stable-set outcome.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

30 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 of Lemma 5.1 (standard reference, not scraped)