ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-09-26 (gpt-6-sol)

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.

For large $n$ , the Fox–Sudakov choice of $x$ leaves a dense-or-sparse set of order at least $\sqrt{n}$

Example

Fix a nonempty finite graph $H$ , let $C_{H} > 0$ be the constant from Fox sudakov quantitative induced density bound, and let $G$ be an $H$ -free graph on $n$ vertices. Write $L : = \log_{2} n$ , assume $L > 2 C_{H}$ , and choose $x : = 2^{- \sqrt{L / (2 C_{H})}}$ .

Facts & Assumptions

Given: The data in the Example, in particular $L > 2 C_{H}$ .

[L1]

For nonempty $H$ and $G$ and $0 < x < 1 / 2$ , the proved quantitative-density corollary gives every $H$ -free $n$ -vertex graph a nonempty set $S$ of order at least $2^{- C_{H} (\log_{2} (1 / x))^{2}} n$ such that $G [S]$ or its complement has at most $x (\binom{∣ S ∣}{2})$ edges (Fox sudakov quantitative induced density bound). The hypothesis $L > 2 C_{H} > 0$ ensures $n > 1$ , so $G$ is nonempty.

Verification

technique · direct

1.1givenalgebra

For the chosen $x$ , one has $\log_{2} (1 / x) = \sqrt{L / (2 C_{H})} > 1$ , so $0 < x < 1 / 2$ .

2.1step 1.1L1algebra

Therefore $2^{- C_{H} (\log_{2} (1 / x))^{2}} n = 2^{- C_{H} \cdot L / (2 C_{H})} n = 2^{- L / 2} n = \sqrt{n}$ .

3.1step 2.1L1∎

So the proved quantitative-density corollary guarantees a dense-or-sparse set of order at least $\sqrt{n}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

Matija Bucić, Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. I. A loglog step towards Erdős-Hajnal, Theorem 1.5 (standard reference, not scraped)

For large nn, the Fox–Sudakov choice of xx leaves a dense-or-sparse set of order at least nn​