Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

Large induced subgraphs without a polynomial clique or stable set force complete or anticomplete blockades

Statement

Let F be a generalized nice, leaf-reducible, wonderful finite family. Let c1≥1 and c2>0 be the constants from Rödl initialization upgrades generalized niceness to a restricted set, a complete or anticomplete blockade, or a polynomial clique or stable set. Fix an F‾-free graph G, define

q:=42c12,c:=min⁡{q−1,c2/2},x:=∣G∣−1/(3c1),ϵ:=x1/(7c1).

and assume that G has no clique or stable set of size at least ∣G∣c. Then every induced subgraph F of G with ∣F∣≥ϵ2c1∣G∣ has a complete or anticomplete (k,∣F∣/kc1)-blockade for some integer k∈[2,ϵ−1].

Facts & Assumptions

Given: The data and hypotheses in the Statement.

[L1]

The previous lemma gives every F‾-free graph either an x-restricted induced subgraph of size at least xc1 times the ambient order, or a complete or anticomplete (k,∣G∣/kc1)-blockade with k≥2, or a clique or stable set of size at least (xc1∣G∣)c2 (Rödl initialization upgrades generalized niceness to a restricted set, a complete or anticomplete blockade, or a polynomial clique or stable set).

[L2]

A nonempty x-sparse graph H satisfies χ(H)≤x∣H∣+1,∣H∣≤χ(H)α(H), by The greedy colouring bound χ(G)≤Δ(G)+1 for every nonnull finite graph and The bounds ω(G)≤χ(G) and ∣V(G)∣≤χ(G)α(G).

Proof

technique · apply the previous lemma to $F$ and show that the restricted and clique/stable branches contradict the assumed failure of the polynomial bound
1.1givenassume-contra

Let F be an induced subgraph of G with ∣F∣≥ϵ2c1∣G∣, and suppose for contradiction that F has no complete or anticomplete (k,∣F∣/kc1)-blockade for any integer k∈[2,ϵ−1].

2.1

Apply [L1] to the graph F with the parameter x. Because the blockade branch is excluded by step 1.1, either:

  1. F has an x-restricted induced subgraph S with ∣S∣≥xc1∣F∣, or
  2. F has a complete or anticomplete (k,∣F∣/kc1)-blockade for some integer k≥2, or
  3. F has a clique or stable set of size at least (xc1∣F∣)c2.

[step 1.1, L1]

3.1step 2.1L3algebra

Suppose the restricted branch of step 2.1 holds. Then ∣S∣≥xc1∣F∣≥xc1ϵ2c1∣G∣=xc1+2/7∣G∣=x−2c1+2/7. Since c1≥1 and 0<x<1, the exponent −2c1+2/7 is at most −1, so ∣S∣≥x−1. After replacing S by the same set in the complementary graph if necessary, [L3] lets us assume that S is x-sparse.

3.2step 1.1step 2.1algebrachoose

Suppose instead that the blockade branch of step 2.1 holds. Then step 1.1 forces k>ϵ−1. Choosing one vertex from each block gives a clique or stable set of size k>ϵ−1=∣G∣1/(21c12)≥∣G∣c, because c≤(42c12)−1. This contradicts the hypothesis on G.

3.3step 2.1algebra

Suppose instead that the clique-or-stable-set branch of step 2.1 holds. Then (xc1∣F∣)c2≥(xc1ϵ2c1∣G∣)c2=(xc1+2/7∣G∣)c2. Since x=∣G∣−1/(3c1), the inner factor equals ∣G∣1−(c1+2/7)/(3c1), whose exponent is at least 1/2 because c1≥1. Therefore F contains a clique or stable set of size at least ∣G∣c2/2≥∣G∣c, because c≤c2/2. This again contradicts the hypothesis on G.

4.1step 3.1L2algebra

By [L2], α(G[S])≥∣S∣x∣S∣+1=1x+∣S∣−1≥1x+x≥x−1/2. Because x=∣G∣−1/(3c1), this gives a clique or stable set of size at least ∣G∣1/(6c1)≥∣G∣c, contradicting the hypothesis on G because c≤q−1=1/(42c12)≤1/(6c1).

5.1step 4.1step 3.2step 3.3discharge-contradiction∎

All three branches from step 2.1 contradict the hypothesis on G, so the assumption in step 1.1 was false. Therefore F has a complete or anticomplete (k,∣F∣/kc1)-blockade for some integer k∈[2,ϵ−1].

Depends on

Used by

Dependency tree · two levels

22 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