ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 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 log-log choice of $x$ still 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 Loglog quantitative induced density bound, and let $G$ be an $H$ -free graph on $n \geq 3$ vertices. Write $L : = \log_{2} n$ , and set $β : = 1 / (4 \sqrt{C_{H}})$ and $x : = 2^{- β \sqrt{L \log_{2} L}}$ .

Facts & Assumptions

Given: The data in the Example.

[L1]

For nonempty $H, G$ and $0 < x < 1 / 2$ , the proved quantitative induced-density theorem gives every $H$ -free $n$ -vertex graph a nonempty set $S$ of order at least $2^{- C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x)} n$ whose induced graph or complement has at most $x (\binom{∣ S ∣}{2})$ edges (Loglog quantitative induced density bound).

Verification

technique · direct

1.1givenalgebra

For the chosen $x$ , one has $\log_{2} (1 / x) = β \sqrt{L \log_{2} L}$ .

2.1step 1.1algebra

For all sufficiently large $L$ , the inequality $β \sqrt{L \log_{2} L} \geq \sqrt{L} > 1$ holds. Hence $0 < x < 1 / 2$ and $\log_{2} \log_{2} (1 / x) \geq \frac{1}{2} \log_{2} L$ .

3.1step 2.1L1algebra

Hence, for all sufficiently large $n$ , $C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x) \leq 2 C_{H} β^{2} L = L / 8$ , and therefore $2^{- C_{H} (\log_{2} (1 / x))^{2} / \log_{2} \log_{2} (1 / x)} n \geq 2^{- L / 8} n = 2^{7 L / 8} \geq \sqrt{n}$ .

4.1step 3.1L1∎

So for all sufficiently large $n$ , this choice of $x$ still leaves 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.8 (standard reference, not scraped)

For large nn, the log-log choice of xx still leaves a dense-or-sparse set of order at least nn​