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

Iterated sparse restriction reaches the target sparsity threshold

Statement

Let c(0,1), b1>1, b2,b3>0, and assume b1b2b2+b3. Suppose that x(0,c) and that a graph G satisfies:

  1. G has a c-sparse induced subgraph with at least cb2V(G) vertices; and
  2. for every λ[x,c] and every λ-sparse induced subgraph F of G with V(F)λb2V(G), there is a λb1-sparse induced subgraph of F with at least λb3V(F) vertices.

Then G contains an x-sparse induced subgraph with at least xb1b2V(G) vertices.

Facts & Assumptions

Given: The parameters and hypotheses in the statement.

[L1]

A λ-sparse vertex set is nonempty, and every vertex has degree at most λ times the size of that set inside the induced subgraph (c-sparse, c-dense and c-restricted vertex sets).

Proof

technique · direct
1.1

Hypothesis 1 supplies a nonempty c-sparse vertex set, because c-sparse sets are nonempty by [L1]. Hence V(G)>0.

givenL1
1.2

For each nonempty induced subgraph E of G, let μ(E) be its maximum degree divided by V(E); by [L1], the graph E is λ-sparse exactly when μ(E)λ. Define λ(E):=max(xb1,μ(E)). Hypothesis 1 gives a c-sparse induced subgraph E0 with at least cb2V(G) vertices, so λ(E0)c and V(E0)λ(E0)b2V(G). Because G has only finitely many induced subgraphs, the set of values λ(E) with λ(E)c and V(E)λ(E)b2V(G) has a minimum. Choose an induced subgraph F for which that minimum is attained, and write λ:=λ(F).

givenchooseL1algebra
2.1

Suppose that λx. Then hypothesis 2 applies to F and produces a λb1-sparse induced subgraph FF with at least λb3V(F)λb2+b3V(G)λb1b2V(G) vertices, where the last inequality uses b1b2b2+b3. Since F is λb1-sparse, we have μ(F)λb1 and therefore λ(F)=max(xb1,μ(F))λb1<λ. Also V(F)λ(F)b2V(G). This contradicts the minimal choice of λ. Therefore λ<x.

step 1.2givenalgebraassume-contradischarge-contradiction
3.1

Since λ=λ(F), step 1.2 gives xb1λ, and step 2.1 gives λ<x. Because F is λ-sparse, it is also x-sparse. Moreover V(F)λb2V(G)(xb1)b2V(G)=xb1b2V(G).

step 1.2step 2.1algebra
4.1

The induced subgraph F from step 3.1 is the required x-sparse induced subgraph.

step 3.1

Depends on

Used by

Dependency tree · two levels

6 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