Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31
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 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.

Depends on

Used by

Dependency tree · two levels

16 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