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

Generalized niceness yields four reduction outcomes

Statement

Let F be a generalized nice, leaf-reducible, wonderful finite family of graphs. Then there exist constants a1,a2,a5>0 and a3≥a4≥4 such that for every y∈(0,12) and every y-restricted F‾-free graph G, at least one of the following holds:

  1. G has a clique or stable set of size at least (ya1∣G∣)a2;
  2. G has a ya4-restricted induced subgraph with at least ya3∣G∣ vertices;
  3. G has a complete or anticomplete (k,∣G∣/ka3)-blockade with k≥y−1; or
  4. there exist disjoint sets X,Y⊆V(G) with ∣X∣≥ya3∣G∣,∣Y∣≥(1−a5y)∣G∣, and Y complete or anticomplete to X.

Facts & Assumptions

Given: A generalized nice, leaf-reducible, wonderful finite family F, a parameter y∈(0,12), and a y-restricted F‾-free graph G.

[L1]

Generalized niceness supplies constants c1≥3, c2≥8, c3,c4,c5,c8>0, c6≥1, and c7≥4 with the four alternatives in Generalized nice finite graph families.

[L2]

Leaf-reducibility supplies constants d>0 and h≥1 such that every y-sparse F-free graph yields either a large anticomplete pair or a deeper restricted induced subgraph (Leaf-reducible families yield a large anticomplete pair or a deeper restricted induced subgraph).

[L4]

Wonderfulness supplies an exponent a≥6 as in Wonderful finite graph families.

[L5]

A complete-or-weakly-sparse blockade can be thinned to equal-sized subblocks with directional sparsity (A complete-or-weakly-sparse blockade can be thinned to equal subblocks with directional sparsity).

[L6]

Such an equal-sized blockade either contains a complete subblockade or can be thinned further to anticonnected subblocks (A complete-or-weakly-sparse blockade yields a complete subblockade or an anticonnected thinning).

[L7]

A wonderful anticonnected blockade with small support yields either a y4-restricted induced subgraph or a large anticomplete pair (A wonderful anticonnected complete-or-sparse blockade yields a restricted subgraph or a large anticomplete pair).

Proof

technique · separate the complement-sparse branch from the sparse branch, then resolve the blockade branch by thinning and wonderfulness
1.1L1L2L4choose

Fix constants from [L1], [L2], and [L4], and set a1:=ac3, a2:=c4, a4:=4, a5:=h+4, and a3:=max⁡{a(c1+5), ac8, c5, 4d+1}. These choices depend only on F.

2.1step 1.1givenalgebra

If ∣G∣≤y−a3, then any one-vertex induced subgraph of G is y4-restricted and has size at least ya3∣G∣. So outcome 2 holds.

2.2L2L3step 1.1givenalgebra

Suppose G‾ is y-sparse. Apply [L2] to the family F inside G‾ with the parameter b=4. Either G‾ has a y4-restricted induced subgraph of size at least y4d+1∣G∣, or there are disjoint sets X,Y⊆V(G) with ∣X∣≥y4d+1∣G∣, ∣Y∣≥(1−hy)∣G∣, and Y anticomplete to X in G‾. By [L3], the restricted induced subgraph is also y4-restricted in G, and the anticomplete pair in G‾ is a complete pair in G. Since a3≥4d+1 and a5≥h, this gives outcome 2 or outcome 4 in G.

2.3L1step 1.1givenalgebra

We may therefore assume that G itself is y-sparse. Put ϵ:=ya, where a is the witness from [L4]. Because G is F‾-free, [L1] applies to G and ϵ. If [L1] produces a clique or stable set of size (ϵc3∣G∣)c4, then this is exactly outcome 1 by the choice a1=ac3 and a2=c4. If [L1] produces a complete or anticomplete (k,∣G∣/kc5)-blockade with k≥ϵ−c6, then k≥y−1 because c6≥1, and ∣G∣/kc5≥∣G∣/ka3 because a3≥c5, so outcome 3 holds. If [L1] produces an ϵc7-restricted induced subgraph of size at least ϵc8∣G∣, then ϵc7≤y4 and ϵc8=yac8≥ya3, so outcome 2 holds. We are left only with the blockade alternative from [L1].

3.1L5L6step 2.3step 1.1choosealgebra

Thus G has a blockade A=(A1,…,Aℓ) with ℓ=⌈ϵ−1⌉, each ∣Ai∣≥m:=ϵc1∣G∣, and every distinct pair complete or weakly ϵc2-sparse. Apply [L5] to obtain equal-sized subblocks D=(D1,…,Dℓ) with ∣Di∣=q:=⌈ϵ⌈m⌉⌉ and every noncomplete pair mutually ϵc2−5-sparse. Then apply [L6] to D. If [L6] yields a complete (ℓ,q/ℓ2)-blockade, then q/ℓ2≥ϵm⋅ϵ4=ϵ5m=ya(c1+5)∣G∣≥ya3∣G∣, because ℓ=⌈ϵ−1⌉≤ϵ−2 for ϵ∈(0,12) and step 1.1 has a3≥a(c1+5). Since also ℓ≥ϵ−1=y−a≥y−1, outcome 3 follows.

4.1step 2.1step 3.1L6L7step 1.1algebra

We may therefore assume [L6] yields anticonnected subsets Bi⊆Di of common size w:=⌈q/ℓ⌉ such that every distinct pair is either complete or mutually (ϵc2−5ℓ)-sparse. Because ℓ≤ϵ−2, every noncomplete pair is in fact mutually ϵc2−7-sparse. Also w≥q/ℓ≥ϵ3m=ϵc1+3∣G∣=ya(c1+3)∣G∣≥ya3∣G∣, since q≥ϵm and ℓ≤ϵ−2. Since step 2.1 fails, ∣G∣>y−a3, and because a3≥a(c1+5) with ϵ=ya, this gives m=ϵc1∣G∣>y−5a=ϵ−5 and hence q=⌈ϵ⌈m⌉⌉>ϵm>ϵ−4≥ϵ−2≥ℓ. Therefore ∣V(B)∣=∑i=1ℓ∣Bi∣≤ℓ(q/ℓ+1)=q+ℓ≤2q≤2⌈m⌉≤4m≤ϵc1−2∣G∣≤ϵ∣G∣≤y∣G∣, where B:=(B1,…,Bℓ). Since c2≥8, one has ϵc2−7=ya(c2−7)≤ya. Therefore the hypotheses of [L7] hold for B.

5.1L7step 4.1step 1.1algebra

Applying [L7] to B yields either a y4-restricted induced subgraph of size at least w, giving outcome 2, or disjoint sets X,Y⊆V(G) with ∣X∣=w≥ya3∣G∣, ∣Y∣≥(1−4y)∣G∣≥(1−a5y)∣G∣, and Y anticomplete to X, giving outcome 4.

6.1step 2.1step 2.2step 2.3step 5.1∎

The cases in steps 2.1, 2.2, 2.3, and 5.1 exhaust all possibilities, so one of the four stated outcomes always holds.

Depends on

Used by

Dependency tree · two levels

28 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