Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

Constant-scale restricted property (*) yields a restricted subgraph, a polynomial clique or stable set, or two blockade alternatives

Statement

Suppose that F has property (∗) and is leaf-reducible. Then there exist constants c1,c2,c3>0, c4,c5≥4, and c:=2−4c5 such that for every x∈(0,c10] and every c10-restricted F‾-free graph G, at least one of the following holds:

  1. G has an x-restricted induced subgraph with at least x22c4∣G∣ vertices;
  2. G has a clique or stable set of size at least (x30c4∣G∣)c1;
  3. G has a complete or anticomplete (k,∣G∣/kc2+27c4/c3)-blockade for some real k≥2;
  4. G has a pure or x-sparse (ℓ,∣G∣/ℓ29c4)-blockade for some real ℓ∈[c−1,x−2].

Facts & Assumptions

Given: A finite family F with property (∗) and leaf-reducible, an x∈(0,c10], and a c10-restricted F‾-free graph G.

[L1]

The previous claim says that, under the failure of outcomes 2-4, every y10/3-restricted induced subgraph of sufficiently large relative size has a deeper y11/3-restricted induced subgraph (Under failure of the global outcomes, a large y^(10/3)-restricted induced subgraph forces a y^(11/3)-restricted induced subgraph).

[L2]

If a graph has a c10-restricted induced subgraph of size at least (c10)3(c4+2)∣G∣ and every λ-restricted induced subgraph of size at least λ3(c4+2)∣G∣ contains a λ11/10-restricted induced subgraph of size at least λ3(c4+2)/10 times as many vertices, then the graph has an x10/3-restricted induced subgraph with at least x11(c4+2)∣G∣ vertices (Iterated restricted sparsification reaches the target scale).

[L3]

If a set is x10/3-restricted, then it is x-restricted (c-sparse, c-dense and c-restricted vertex sets).

Proof

technique · if outcomes 2-4 fail, verify the hypotheses of the iterative restricted-sparsification lemma with $b_1=\tfrac{11}{10}$, $b_2=3(c_4+2)$, and $b_3=\tfrac{3(c_4+2)}{10}$
1.1L1choose

Let c1,c2,c3>0, c4,c5≥4, and c:=2−4c5 be the constants from Under failure of the global outcomes, a large y^(10/3)-restricted induced subgraph forces a y^(11/3)-restricted induced subgraph, and set b1:=11/10,b2:=3(c4+2),b3:=3(c4+2)/10.

1.2givenassume-contra

Suppose outcomes 2, 3, and 4 all fail. We will show that outcome 1 then holds.

2.1step 1.1L2givenalgebra

Hypothesis 1 of [L2] is immediate: the graph G itself is c10-restricted and has size ∣G∣≥(c10)b2∣G∣ because b2>0 and c10<1.

2.2step 1.1step 1.2L1L2algebra

Let λ∈[x10/3,c10] and let F be a λ-restricted induced subgraph of G with ∣F∣≥λb2∣G∣. Write λ=y10/3, so y=λ3/10∈[x,c3]. Then ∣F∣≥y10(c4+2)∣G∣. Since outcomes 2-4 fail globally, [L1] applied with this y gives a y11/3=λ11/10-restricted induced subgraph of F with at least yc4+2∣F∣=λb3∣F∣ vertices.

2.3step 1.1L2algebra

The exponent condition for [L2] holds because b1b2=1110⋅3(c4+2)=33(c4+2)10≥30(c4+2)10=b2+b3.

3.1step 2.1step 2.2step 2.3L2L3algebra

Therefore [L2] yields an x10/3-restricted induced subgraph S⊆G with at least (x10/3)b1b2∣G∣=x11(c4+2)∣G∣ vertices. Since c4≥4, the exponent satisfies 11(c4+2)≤22c4, so ∣S∣≥x22c4∣G∣. By [L3], the subgraph S is x-restricted. Hence outcome 1 holds.

4.1step 1.2step 3.1discharge-contradiction∎

Outcome 1 follows whenever outcomes 2-4 fail. Hence at least one of the four stated outcomes always holds.

Depends on

Used by

Dependency tree · two levels

9 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