CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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.

Fox sudakov quantitative induced density bound

Statement

For every nonempty finite graph $H$ there is $C_{H} > 0$ such that for $0 < x < 1 / 2$ , $δ = 2^{- C_{H} (\log_{2} (1 / x))^{2}}$ , and any nonempty finite graph $G$ with ${ind}_{H} (G) \leq (δ ∣ G ∣)^{∣ H ∣}$ , there is a nonempty $S \subseteq V (G)$ with $∣ S ∣ \geq δ ∣ G ∣$ and at most $x (\binom{∣ S ∣}{2})$ edges in $G [S]$ or $\overline{G} [S]$ . In particular this holds for $H$ -free $G$ . The version with a strict copy inequality covers the null pattern vacuously.

The constant is allowed to depend on $H$ ; this assertion does not specify an absolute constant times $∣ H ∣$ .

Facts & Assumptions

Given: Nonempty $H, G$ , $0 < x < 1 / 2$ , and the copy hypothesis with the displayed fraction after $C_{H}$ is chosen.

[F1]

From Qid logarithmic and constant divisibility: Every nonempty finite graph $H$ is $ℓ$ -divisive for each of $ℓ (x) = \log_{2} (1 / x)$ and $ℓ (x) = 2$ . Both functions are subreciprocal on $(0, 1 / 2)$ .

[F2]

For nonempty $ℓ$ -divisive $H$ and subreciprocal $ℓ$ , some $C_{H, ℓ} > 0$ gives the fraction $δ = 2^{- C_{H, ℓ} \log_{2} (1 / ϵ)^{2} / \log_{2} ℓ (ϵ)}$ on $0 < ϵ < 1 / 2$ ; a nonempty host with at most $(δ ∣ G ∣)^{∣ H ∣}$ embeddings has the asserted nonempty sparse-or-dense set of size at least $δ ∣ G ∣$ . (Quantitative density theorem for ell divisive graphs).

Proof

1.1F1F2

Choose $ℓ (x) = 2$ . By [F1] this is subreciprocal and the given nonempty $H$ is $ℓ$ -divisive, so [F2] applies. Its denominator is $\log_{2} ℓ (x) = \log_{2} 2 = 1$ . With $C_{H} = C_{H, ℓ}$ , its fraction is exactly $2^{- C_{H} (\log_{2} (1 / x))^{2}}$ and its conclusion is the claimed set and edge bound.

2.1step 1.1algebra∎

If $G$ is $H$ -free, its labelled induced-embedding count is zero, which satisfies the non-strict premise. For the null pattern the unique empty embedding gives count 1, while $(δ ∣ G ∣)^{0} = 1$ ; the strict premise would read $1 < 1$ and is impossible. These observations establish both additional clauses.

Source notes

Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 5.2 at ell=2; 1.7 (comparison of constant dependence).

Depends on

Used by

Dependency tree · two levels

13 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

Bucic, Nguyen, Scott and Seymour, Induced subgraph density I (standard reference, not scraped)