Alphabeta Math
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.

✓ 21 results · all verified · 13 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Iterative Sparsification and the Five-Vertex Path

1 · Prerequisites

2 · Summary

This draft page follows the source split that the design called out: the first half proves that P5 is nice by iteratively building pure or sparse blockades, and the second half turns a nice blockade into either a complete or anticomplete blockade or a deeper sparse subgraph until the published restricted-set theorem can close the argument.

The final two items separate the two endpoints. First the page proves the polynomial Rödl property for P5, then it converts that stronger conclusion to the Erdős-Hajnal property using the already-published Rödl-to-EH implication.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A nice graph

Definition

Let H be a finite graph. We say that H is nice if there exists a real d≥1 such that for every ϵ∈(0,12) and every H‾-free graph G with

∣V(G)∣≥ϵ−10d2,

there is a (⌈ϵ−1⌉,ϵ10d2∣V(G)∣)-blockade B=(B1,…,Bℓ) in G such that for all distinct i,j∈[ℓ] the pair (Bi,Bj) is either complete or weakly ϵd-sparse.

The complement appears because the source proves niceness for P5 through P5‾-free graphs. The blockade clause is exactly the local configuration that the second half of the source proof refines into complete or anticomplete blockades.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Small anticonnected components yield a complete blockade

Statement

Let G be a graph on n vertices, and let k≥2 be an integer. Suppose every anticonnected component of G has size less than n/k. Then G contains a complete blockade of length at least k/2 and width at least n/(2k).

Facts & Assumptions

Given: A graph G on n vertices and an integer k≥2 such that every anticonnected component of G has size less than n/k.

[L1]

Proof

technique · direct packing
1.1givenchoosealgebra

Partition the anticonnected components into a minimum number of unions S0,…,Sr, each of size less than n/k, and order them so that ∣S0∣≤⋯≤∣Sr∣. Since their union has size n, one has r+1>k.

2.1step 1.1L1algebra∎

For every i≥1, minimality gives ∣Si−1∣+∣Si∣≥n/k; otherwise these two parts could be merged. The ordering then yields ∣Si∣≥n/(2k). Thus S1,…,Sr contain at least k nonempty blocks of width at least n/(2k), and [L1] makes every cross-pair complete. Selecting any ⌈k/2⌉ of them proves the statement.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A dense bipartite side has a small hitting set

Statement

Let A,B be disjoint nonempty vertex sets in a graph, and let x∈(0,1]. Assume every vertex of B has at least x∣A∣ neighbours in A. Then there is a set S⊆A with ∣S∣≤⌈1/x⌉ that meets the neighbourhood in A of at least half of the vertices of B.

Facts & Assumptions

Given: Disjoint nonempty vertex sets A,B in a graph and a real x∈(0,1] such that every b∈B has at least x∣A∣ neighbours in A.

[L1]

If S=A, then every neighbourhood in A is hit; otherwise a uniform m-subset of A misses a fixed b-neighbourhood with probability at most (1−x)m.

Proof

technique · probabilistic existence
1.1L1givenchoosealgebra

If ⌈1/x⌉≥∣A∣, take S:=A and every neighbourhood in A is hit. Otherwise let m:=⌈1/x⌉<∣A∣ and choose a subset S⊆A uniformly among all subsets of size m. For a fixed vertex b∈B, the probability that S∩N(b)=∅ is at most (1−x)m≤e−xm≤e−1<1/2.

2.1step 1.1algebra∎

In the first case every vertex of B is hit. In the second case the expected number of vertices of B whose neighbourhood misses S is less than ∣B∣/2, so some choice of S misses fewer than half of B. Thus in either case there is a set S⊆A with ∣S∣≤⌈1/x⌉ that meets the neighbourhood of at least half of the vertices of B.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A sparse P5-free graph has an anticomplete two-blockade

Statement

There exists η>0 such that every η-sparse P5-free graph G with ∣V(G)∣≥η−1 contains an anticomplete blockade of length 2 and width at least η∣V(G)∣.

Facts & Assumptions

Given: An η-sparse P5-free graph G with ∣V(G)∣≥η−1.

[L1]

Lemma 4.4 of the cited source proves exactly the displayed conclusion for η=2−5, using repeated large-component consequences of the failure of the desired anticomplete blockade.

Proof

technique · translate the cited source lemma
1.1L1given

The cited source lemma assumes the negation of the desired blockade, first obtains a connected component of size at least ∣V(G)∣/2, and then obtains two further large connected pieces outside successive neighbourhoods.

2.1step 1.1L1∎

The source shows that the absence of the blockade then forces five selected vertices to induce P5, contradicting the hypothesis. Therefore the stated anticomplete two-blockade exists.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A sparse P5‾-free graph has a large nearly covered sparse pair

Statement

Let x,y>0 with x≤y≤2−8, and let G be a y3-sparse P5‾-free graph with ∣V(G)∣≥y−4. Suppose that G is not 2y4-sparse, and that there do not exist disjoint sets X,Y⊆V(G) such that

∣X∣≥y4∣V(G)∣,∣Y∣≥(1−4y)∣V(G)∣,

and Y is x-sparse to X. Then there exist disjoint sets A,B⊆V(G) such that:

  1. ∣A∣≥(1−3y)∣V(G)∣ and ∣B∣≥y4∣V(G)∣;
  2. A is y2-sparse to B; and
  3. every vertex of B has at least x2∣A∣ neighbours in A.

Facts & Assumptions

Given: Parameters x,y and a graph G satisfying the displayed hypotheses.

[L1]

Claim 5.2.1 of the cited source proves exactly the displayed conclusion under these hypotheses after translating notation.

Proof

technique · translate the cited source claim
1.1L1given

The cited source claim proves exactly this large nearly covered sparse-pair conclusion after translating notation.

2.1step 1.1∎

Therefore the present statement follows.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31Open item page →

Anticonnected block contraction turns an upside-down comb into a pure blockade

Statement

Let G be a P5‾-free graph, let k≥4 be an integer, and let B⊆V(G). Suppose

((ai,Bi):i∈[k])

is a (k,∣B∣/k8)-comb in G with Bi⊆B and ai∉B for every i∈[k]. Suppose also that there is a vertex

v∈V(G)∖(B∪{a1,…,ak})

that is complete to B and anticomplete to {a1,…,ak}. Then G[B] contains a pure (k,∣B∣/k10)-blockade.

Facts & Assumptions

Given: The graph G, the integer k, the set B, the displayed comb, and the vertex v satisfying the hypotheses above.

[F1]

In the displayed comb, ai is complete to Bi and anticomplete to Bj for i≠j, while the blocks are pairwise disjoint and satisfy ∣Bi∣≥∣B∣/k8 (Combs in a graph).

[F2]

A set D is an anticonnected component of G[X] precisely when it is the vertex set of a connected component of G[X]‾ (Anticonnected graphs and anticonnected components).

[L1]

Distinct anticonnected components of a graph are complete to one another (Distinct connected components are anticomplete, and distinct anticonnected components are complete).

[F3]

A blockade is pure when every pair of distinct blocks is either complete or anticomplete (Complete, anticomplete, pure, weakly sparse, and x-sparse blockades).

[F5]

Complementation exchanges edges and nonedges (Graph isomorphisms, automorphisms and graph complements).

Proof

technique · contract each comb block to a large anticomponent
1.1F1L1F3givenchoosealgebra

Fix i∈[k] and put ni:=∣Bi∣. Suppose first that every anticonnected component of G[Bi] has size less than ni/k. Partition the anticonnected components into a minimum number of unions S0,…,Sr, each of size less than ni/k, and order them by nondecreasing size. Since the parts cover Bi, one has r+1>k. Minimality gives ∣Sj−1∣+∣Sj∣≥ni/k for j≥1, and hence ∣Sj∣≥ni/(2k)≥ni/k2 because k≥4. By [L1], the sets S1,…,Sk are pairwise complete. They therefore form a complete, hence pure, (k,ni/k2)-blockade in G[B]. By [F1], ni/k2≥∣B∣/k10, which proves the result in this case.

2.1F1F2step 1.1choosealgebra

We may consequently assume that, for every i∈[k], the graph G[Bi] has an anticonnected component Di with ∣Di∣≥∣Bi∣/k. Choose one such Di. Then ∣Di∣≥∣Bi∣/k≥∣B∣/k9≥∣B∣/k10, giving the required width bound for every chosen component.

3.1F2step 2.1given

Let i≠j, and suppose that some u∈Dj is mixed on Di. The sets of neighbours and nonneighbours of u in Di are both nonempty. Since G[Di]‾ is connected, some edge of that complement crosses these two sets. Thus there are w,z∈Di such that uw∈E(G), uz∉E(G), and wz∉E(G).

4.1F1F4F5step 3.1given

Among the five vertices v,ai,u,z,w, the nonedges are exactly vai,aiu,uz,zw. Indeed, the hypotheses on v determine its four incidences; [F1] determines the incidences from ai to Di⊆Bi and to u∈Dj⊆Bj; and step 3.1 determines the three remaining incidences. Hence those four nonedges form the path v−ai−u−z−w, so these vertices induce P5‾ by [F4] and [F5], contrary to the hypothesis on G. Therefore no vertex of Dj is mixed on Di.

5.1step 4.1cases

Applying step 4.1 with both orders of i,j shows that no vertex of either set is mixed on the other. If the pair (Di,Dj) had both an edge and a nonedge, then the vertices of Dj would include one complete to Di and one anticomplete to Di; every endpoint in Di of the cross-edge would then be mixed on Dj, a contradiction. Thus (Di,Dj) is pure.

6.1F1F3step 2.1step 5.1∎

The sets D1,…,Dk are pairwise disjoint subsets of B, have size at least ∣B∣/k10 by step 2.1, and every cross-pair is pure by step 5.1. Hence they form the required pure (k,∣B∣/k10)-blockade in G[B].

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A sparse P5‾-free graph either sparsifies further or yields a pure blockade or a large sparse pair

Statement

Let x,y>0 with x≤y≤2−8, and let G be a y3-sparse P5‾-free graph with ∣V(G)∣≥y−4. Then at least one of the following holds:

  1. G is 2y4-sparse;
  2. there exists an integer k∈[y−1/4,1/x] and a pure (k,∣V(G)∣/k26)-blockade in G; or
  3. there are disjoint sets X,Y⊆V(G) such that ∣X∣≥y4∣V(G)∣, ∣Y∣≥(1−4y)∣V(G)∣, and Y is x-sparse to X.

Facts & Assumptions

Given: Parameters x,y and a graph G satisfying the displayed hypotheses.

[L1]

Lemma 5.2 of the cited source proves exactly the displayed trichotomy under these hypotheses.

Proof

technique · translate the cited source lemma
1.1L1given

The cited source lemma proves exactly the three displayed alternatives under these hypotheses.

2.1step 1.1∎

Therefore the present trichotomy holds.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

An x-sparse blockade iteration yields further sparsification or a pure blockade

Statement

Let x∈(0,12). There exist constants c>0 and d≥1 such that the following holds. If G is a sparse P5‾-free graph and B=(B0,…,Bn) is a maximal x-sparse blockade whose last block still has linear size, then either:

  1. some induced subgraph of Bn is substantially sparser than G; or
  2. G has a pure blockade of polynomial width.

Facts & Assumptions

Given: A sparse P5‾-free graph G and a maximal x-sparse blockade B=(B0,…,Bn) with large last block Bn.

[L1]

Lemma 5.3 of the cited source proves the stated maximal-blockade alternative with explicit constants, sizes, and exponents.

Proof

technique · translate the cited source lemma
1.1L1given

The cited source lemma applies the preceding sparse-pair trichotomy to the final block and uses the correctly oriented sparse relations to extend the blockade whenever the sparse-pair outcome occurs.

2.1step 1.1L1∎

Maximality excludes that extension, leaving exactly a substantially sparser induced subgraph or a polynomial-width pure blockade.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31Open item page →

An iterative sparsification step for sparse P5‾-free graphs

Statement

Put c:=2−8. Let x∈(0,c5), and let G be a c16-sparse P5‾-free graph with ∣V(G)∣≥x−7. Then at least one of the following holds:

  1. for some k∈[c−1,x−1], there is a pure (k,∣V(G)∣/k34)-blockade in G; or
  2. for some y∈[x,c5], there is an x-sparse (y−1,y7∣V(G)∣)-blockade in G.

Facts & Assumptions

Given: The constant c=2−8, a parameter x∈(0,c5), and a c16-sparse P5‾-free graph G with ∣V(G)∣≥x−7.

[F1]

Lemma 5.4 of Nguyen, Scott, and Seymour's cited paper gives the displayed two outcomes with these constants and exponents. Its statement prints ∣G∣≥y−7 before y is bound; the proof shows that the intended hypothesis is ∣G∣≥x−7 by using it to deduce cx∣G∣≥x2∣G∣≥x−5.

[F2]

The source proof chooses a minimal threshold y∈[cx,c5], applies its preceding three-outcome sparse-blockade lemma, and rules out the deeper-sparsification branch by minimality. The remaining branches give the pure blockade in outcome 1 or the x-sparse blockade in outcome 2.

Proof

technique · translate the cited source lemma
1.1F1F2givencases

Apply the corrected, well-formed reading of the cited source lemma recorded in [F1]. Its two alternatives are exactly outcomes 1 and 2, and [F2] records the minimal-threshold argument establishing them.

2.1step 1.1∎

Therefore the present statement follows.

TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31Open item page →

P5‾-free graphs admit a pure or x-sparse polynomial blockade

Statement

There exists d≥40 such that for every x∈(0,2−d) and every P5‾-free graph G with ∣V(G)∣≥x−d, there exists an integer k∈[2,x−1] and either

  1. a pure (k,∣V(G)∣/kd)-blockade in G; or
  2. an x-sparse (k,∣V(G)∣/kd)-blockade in G.

Facts & Assumptions

Given: After the exponent d is chosen below, a parameter x∈(0,2−d) and a P5‾-free graph G with ∣V(G)∣≥x−d.

[L1]

Lemma 5.5 of the cited source supplies an exponent D≥40 such that, under its convention allowing a real blockade-length threshold, there is some r∈[2,x−1] and a pure or x-sparse (r,∣V(G)∣/rD)-blockade whenever x∈(0,2−D) and ∣V(G)∣≥x−D.

[F2]

In this library, the first parameter ℓ of an (ℓ,w)-blockade may be any real number at least 1; its integral actual length must be at least ℓ (equivalently, at least ⌈ℓ⌉) (Blockades, their length, their width, and their support).

Proof

technique · translate the cited source theorem
1.1L1givenalgebra

Let D≥40 be supplied by [L1], and set d:=2D. Fix x and G as in the Statement. Since d≥D, one has x<2−D and ∣V(G)∣≥x−D. Thus [L1] gives a real r∈[2,x−1] and a pure or x-sparse blockade whose actual length is at least r and whose width is at least ∣V(G)∣/rD.

2.1step 1.1F2algebra

Put k:=⌊r⌋. Then k is an integer and 2≤k≤r≤x−1. The blockade's integral actual length, being at least r, is in particular at least k, so [F2] makes it a (k,∣V(G)∣/rD)-blockade.

3.1step 1.1step 2.1algebra

Since k≥2 and k≤r<k+1, one has rD<(k+1)D≤(3k/2)D≤k2D=kd. Consequently ∣V(G)∣/rD≥∣V(G)∣/kd. The blockade from step 1.1 is therefore a pure or x-sparse (k,∣V(G)∣/kd)-blockade in the library's sense.

4.1step 1.1step 3.1∎

The chosen d=2D satisfies d≥40, and steps 1.1--3.1 prove the stated conclusion for every admissible x and G.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A maximal layout has at most ϵ−1 blocks

Statement

Let ϵ∈(0,12) and d≥1. In the counterexample layout construction used for Theorem 6.1 of the cited source, the chosen maximal layout has fewer than ϵ−1 blocks; otherwise its blocks already contain the blockade required by that theorem.

Facts & Assumptions

Given: The maximal layout and counterexample hypotheses in the proof of Theorem 6.1 of the cited source.

[L1]

Claim 6.1.1 of the cited source proves that a chosen layout with at least ϵ−1 blocks already satisfies the target blockade conclusion.

Proof

technique · direct from the cited source claim
1.1L1given

If the chosen layout had at least ϵ−1 blocks, [L1] would make its blocks a blockade satisfying the conclusion of the surrounding theorem.

2.1step 1.1∎

The enclosing counterexample excludes that conclusion, so the layout has fewer than ϵ−1 blocks.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Refining the largest layout block forces local blockade length at least ϵ−1

Statement

In the setting of the previous lemma, let A be the largest block of the maximal layout. If A is refined by a pure or x-sparse polynomial blockade, then that local blockade has length at least ϵ−1.

Facts & Assumptions

Given: A maximal layout, its largest block A, and a pure or x-sparse polynomial blockade inside A.

[L1]

The cited source claim proves that substituting a local blockade of length below ϵ−1 into the largest layout block preserves the three defining layout bounds while strictly increasing the number of blocks.

Proof

technique · contradiction by substitution
1.1L1assume-contra

Suppose the local blockade inside A had length k<ϵ−1. By [L1], substituting its pattern for the layout vertex corresponding to A produces another admissible layout with strictly more blocks.

2.1step 1.1discharge-contradiction∎

This contradicts the maximal choice of the original layout. Hence the local blockade has length at least ϵ−1.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Local pure or x-sparse blockades yield a nice blockade

Statement

Let ϵ∈(0,12) and d≥1, and put x:=ϵ5d. Let G be a graph with ∣V(G)∣≥ϵ−10d2. Assume that every induced subgraph F of G with ∣V(F)∣≥ϵd∣V(G)∣ has a pure or x-sparse (k,∣V(F)∣/kd)-blockade for some integer k∈[2,x−1]. Then G has a (⌈ϵ−1⌉,x2d∣V(G)∣)-blockade whose distinct block pairs are either complete or weakly ϵd-sparse.

Facts & Assumptions

Given: The hypotheses in the statement.

[L1]

Theorem 6.1 of the cited source proves exactly the displayed local-to-global blockade conclusion, with its layout carrying both the block-size power-sum condition and the wrong-pair bound.

Proof

technique · translate the cited source theorem
1.1L1given

The cited source theorem applies to the hypotheses above and produces a blockade of length at least ϵ−1, width at least x2d∣V(G)∣, and complete-or-weakly-ϵd-sparse cross-pairs.

2.1step 1.1algebra∎

Since blockade length is integral, length at least ϵ−1 is equivalent to length at least ⌈ϵ−1⌉. This is exactly the stated conclusion.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

The five-vertex path is nice

Statement

The graph P5 is nice.

Facts & Assumptions

Given: The five-vertex path P5.

[L1]

Every sufficiently large P5‾-free graph admits a pure or x-sparse polynomial blockade when x is below the source threshold (P5‾-free graphs admit a pure or x-sparse polynomial blockade).

[L2]

Such local pure or sparse blockades force a nice blockade (Local pure or x-sparse blockades yield a nice blockade).

[L3]

A graph is nice exactly when some exponent d makes the conclusion of step 2.1 hold for every sufficiently large H‾-free graph (A nice graph).

Proof

technique · direct
1.1L1choosegivenalgebra

Let d be a common exponent large enough to dominate the polynomial width bound in [L1] and the layout theorem [L2]. Fix ϵ∈(0,12) and a P5‾-free graph G with ∣V(G)∣≥ϵ−10d2, and set x:=ϵ5d. Then x<2−d. If F is an induced subgraph of G with ∣V(F)∣≥ϵd∣V(G)∣, then ∣V(F)∣≥ϵdϵ−10d2=ϵ−10d2+d≥ϵ−5d2=x−d. Therefore [L1] applies to F and gives a pure or x-sparse (k,∣V(F)∣/kd)-blockade for some k∈[2,ϵ−5d2].

2.1step 1.1L2L3

Applying [L2] to G yields an (ϵ−1,ϵ10d2∣V(G)∣)-blockade whose distinct block pairs are either complete or weakly ϵd-sparse. By [L3], this is exactly the niceness condition for H=P5.

3.1step 2.1∎

Therefore P5 is nice.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A semisparse blockade can be sampled to anticonnected blocks with nearly pure relations

Statement

There exist constants c>0 and d≥1 such that every sufficiently large sparse P5‾-free graph has at least one of the following:

  1. a complete blockade of linear width; or
  2. a blockade (B1,…,Bt) with t≥c−1, every block of size at least c∣V(G)∣, each Bi anticonnected, and every pair (Bi,Bj) with i≠j either complete or weakly c-sparse.

Facts & Assumptions

Given: A sufficiently large sparse P5‾-free graph G.

[L1]

Claim 7.1.1 of the cited source yields exactly the displayed two-outcome alternative after translating exponents into constants.

Proof

technique · translate the cited source claim
1.1L1given

The cited source claim yields exactly this semisparse-blockade or complete-blockade alternative after translating exponents into constants.

2.1step 1.1∎

Therefore one of the two displayed outcomes holds.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

No vertex is mixed on many blocks of a semisparse blockade

Statement

There exist constants c>0 and d≥1 such that the following holds. Let G be a sufficiently large c-sparse P5‾-free graph, and let (B1,…,Bt) be a blockade from outcome 2 of A semisparse blockade can be sampled to anticonnected blocks with nearly pure relations. Then at least one of the following holds:

  1. G has a cd-sparse induced subgraph of linear size; or
  2. every vertex outside the blockade is mixed on fewer than ct blocks, where a vertex v is mixed on Bi when the pair ({v},Bi) is mixed in the sense of Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs.

Facts & Assumptions

Given: A graph G and a blockade (B1,…,Bt) as in the statement.

[L1]

Claim 7.1.2 of the cited source proves exactly the displayed dichotomy for such semisparse blockades after translating exponents into constants.

Proof

technique · translate the cited source claim
1.1L1given

The cited source claim proves exactly this mixed-block dichotomy after translating exponents into constants.

2.1step 1.1∎

Therefore one of the two displayed outcomes holds.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31Open item page →

A sparse P5‾-free graph yields deeper sparsification or a complete blockade or a large anticomplete set

Statement

There exists a constant d≥40 such that, for every y∈(0,12) and every y-sparse P5‾-free graph G, at least one of the following holds:

  1. there is a set S⊆V(G) with ∣S∣≥y30d3∣V(G)∣ such that G[S] is y2d-sparse;
  2. there is a complete (y−1,y33d3∣V(G)∣)-blockade in G; or
  3. there are disjoint sets X,Y⊆V(G) such that ∣X∣≥y33d3∣V(G)∣,∣Y∣≥(1−3y)∣V(G)∣, and X is anticomplete to Y.

Facts & Assumptions

Given: A parameter y∈(0,12) and a y-sparse P5‾-free graph G.

[F1]

Lemma 7.1 of Nguyen, Scott, and Seymour's cited paper states the displayed trichotomy, with the same constant d≥40 and the same exponents and blockade parameters.

[F2]

In the proof of that lemma, Claim 7.1.1 constructs either the complete blockade in outcome 2 or a long semisparse blockade with anticonnected blocks. Claim 7.1.2 shows that a vertex mixed on many of those blocks yields outcome 1; otherwise averaging over the blocks gives a block anticomplete to a set of size at least (1−3y)∣V(G)∣, which is outcome 3.

Proof

technique · translate the cited source lemma
1.1F1F2givencases

Apply [F1] to the graph in the Given. Its three alternatives are exactly outcomes 1, 2, and 3 in the statement; [F2] records how the semisparse and mixed-block cases in the source proof produce those alternatives.

2.1step 1.1∎

Therefore the present trichotomy holds.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A sparse P5‾-free graph yields a complete or anticomplete blockade or a sparser subgraph

Statement

There exist constants c>0 and d≥1 such that every sufficiently large c-sparse P5‾-free graph has at least one of the following:

  1. a complete blockade of polynomial width;
  2. an anticomplete blockade of polynomial width; or
  3. a cd-sparse induced subgraph of linear size.

Facts & Assumptions

Given: A sufficiently large c-sparse P5‾-free graph G.

[L1]

Lemma 7.2 of the cited source proves the displayed complete-or-anticomplete blockade versus deeper-sparsification alternative with explicit parameters.

Proof

technique · translate the cited source lemma
1.1L1given

The cited source lemma builds a maximal anticomplete blockade and verifies the size normalization needed before applying the preceding sparse trichotomy inside its last block.

2.1step 1.1L1∎

Its three resulting cases are precisely a complete blockade, an anticomplete blockade, or a linearly large induced subgraph with strictly deeper sparsity.

LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The minimal sparsity parameter drops below the target

Statement

Let x∈(0,12). In the minimal-threshold setup of the source, the least sparsity parameter y for which a linear-sized y-sparse induced subgraph exists satisfies y<x.

Facts & Assumptions

Given: A parameter x∈(0,12) and a counterexample graph G in which y is minimal with the stated property.

[L1]

Claim 7.3.1 of the cited source proves exactly that the minimal parameter in its fully quantified threshold setup satisfies y<x.

Proof

technique · direct translation
1.1L1given

The cited source claim applies the exact sparsity, size, and exponent bounds to the minimal witness and excludes its blockade outcome by the enclosing counterexample hypothesis.

2.1step 1.1L1∎

The remaining outcome contradicts minimality unless y<x, which proves the statement.

TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

P5‾-free graphs yield a polynomial restricted set or a complete or anticomplete blockade

Statement

There exists a≥1 such that for every x∈(0,12) and every P5‾-free graph G, at least one of the following holds:

  1. G has an x-restricted induced subgraph with at least xa∣V(G)∣ vertices; or
  2. G has a complete or anticomplete (k,∣V(G)∣/ka)-blockade for some integer k∈[2,x−1].

Facts & Assumptions

Given: A parameter x∈(0,12) and a P5‾-free graph G.

[L1]

Lemma 7.3 of the cited source proves exactly the displayed restricted-set or complete/anticomplete-blockade alternative, with explicit constants.

Proof

technique · direct from the minimal-threshold alternative
1.1L1given

The cited source lemma runs the minimal-threshold argument with all size and exponent bounds and proves the first alternative whenever the blockade alternative is absent.

2.1step 1.1L1∎

Consequently either the stated polynomial restricted set exists or the source's complete/anticomplete polynomial blockade exists, exactly as claimed.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

The five-vertex path has the polynomial Rödl property

Statement

The graph P5 has the polynomial Rödl property.

Facts & Assumptions

Given: The graph P5.

[L1]

There exists a≥1 such that every P5‾-free graph either has an x-restricted induced subgraph of size at least xa∣V(G)∣ or has a complete or anticomplete (k,∣V(G)∣/ka)-blockade for some k∈[2,x−1] (P5‾-free graphs yield a polynomial restricted set or a complete or anticomplete blockade).

[L2]

The blockade alternative alone already forces an x-restricted induced subgraph of size at least x3a∣V(G)∣ (Complete or anticomplete blockade hypotheses force an ϵ-restricted induced subgraph).

Proof

technique · direct
1.1L1givencasesalgebra

Let a be as in [L1]. Fix x∈(0,12) and a P5-free graph G. Then G‾ is P5‾-free. Apply [L1] to every induced subgraph F of G‾ with ∣V(F)∣≥x2a∣V(G)∣. If any such F has an x-restricted set of size at least xa∣V(F)∣, that set has size at least x3a∣V(G)∣ and is also x-restricted in G.

2.1step 1.1L2cases

Otherwise every such F has the complete-or-anticomplete blockade supplied by [L1], so the hypothesis of [L2] holds for G‾. Applying [L2] yields an x-restricted induced subgraph on at least x3a∣V(G)∣ vertices; the same vertex set is x-restricted in G.

3.1step 2.1∎

Therefore P5 has the polynomial Rödl property.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

The five-vertex path and its complement have the Erdős-Hajnal property

Statement

Both P5 and P5‾ have the Erdős-Hajnal property.

Facts & Assumptions

Given: The graph P5.

[L1]

The graph P5 has the polynomial Rödl property (The five-vertex path has the polynomial Rödl property).

[L2]

Every finite family with the polynomial Rödl property has the Erdős-Hajnal property (The polynomial Rödl property implies the Erdős–Hajnal property).

[F1]

The polynomial Rödl property and the Erdős-Hajnal property are both invariant under complementation of the forbidden graph.

Proof

technique · direct
1.1L1L2

Applying [L2] to the singleton family {P5} and using [L1], we conclude that P5 has the Erdős-Hajnal property.

2.1step 1.1

By [F1], the same holds for P5‾.

3.1step 1.1step 2.1∎

Therefore both P5 and P5‾ have the Erdős-Hajnal property.

5 · Examples, counterexamples and false statements

None yet.

Sources