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.

An iterative sparsification step for sparse P5-free graphs

Statement

Put c:=28. Let x(0,c5), and let G be a c16-sparse P5-free graph with V(G)x7. Then at least one of the following holds:

  1. for some k[c1,x1], there is a pure (k,V(G)/k34)-blockade in G; or
  2. for some y[x,c5], there is an x-sparse (y1,y7V(G))-blockade in G.

Facts & Assumptions

Given: The constant c=28, a parameter x(0,c5), and a c16-sparse P5-free graph G with V(G)x7.

[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 Gy7 before y is bound; the proof shows that the intended hypothesis is Gx7 by using it to deduce cxGx2Gx5.

[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.1

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.

F1F2givencases
2.1

Therefore the present statement follows.

step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

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