ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

A nearly covered sparse pair at small parameters

Example

For $y = 2^{- 8}$ and $x = 2^{- 9}$ , suppose a graph $G$ of order $2^{40}$ satisfies the sparse-graph, non- $2 y^{4}$ -sparsity, and no-large-sparse-pair hypotheses of the nearly covered sparse-pair lemma. Its conclusion asks for a set $B$ of size at least $2^{8}$ and a set $A$ of size at least $(1 - 3 \cdot 2^{- 8}) 2^{40}$ such that $A$ is $2^{- 16}$ -sparse to $B$ and every vertex of $B$ has at least $2^{- 18} ∣ A ∣$ neighbours in $A$ .

Facts & Assumptions

Given: The parameters $y = 2^{- 8}$ , $x = 2^{- 9}$ , a graph $G$ with $∣ V (G) ∣ = 2^{40}$ , and all hypotheses of the cited lemma.

[L1]

Under those hypotheses, the lemma produces disjoint sets $A, B$ with $∣ B ∣ \geq y^{4} ∣ V (G) ∣$ , $∣ A ∣ \geq (1 - 3 y) ∣ V (G) ∣$ , $A$ $y^{2}$ -sparse to $B$ , and every vertex of $B$ having at least $x^{2} ∣ A ∣$ neighbours in $A$ (A sparse graph without a large sparse pair has a large nearly covered sparse pair).

Verification

technique · arithmetic unpacking

1.1

Substituting $y = 2^{- 8}$ and $∣ V (G) ∣ = 2^{40}$ into [L1] gives $y^{4} ∣ V (G) ∣ = 2^{- 32} \cdot 2^{40} = 2^{8}$ and $(1 - 3 y) ∣ V (G) ∣ = (1 - 3 \cdot 2^{- 8}) 2^{40}$ .

L1algebra

2.1

The same substitution gives $y^{2} = 2^{- 16}$ and $x^{2} = 2^{- 18}$ , so the sparsity and neighbourhood conclusions in [L1] become exactly the numerical conditions stated above.

step 1.1L1algebra∎

Depends on

A sparse graph without a large sparse pair has a large nearly covered sparse pair

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. VII. The five-vertex path, Claim 5.2.1 (standard reference, not scraped)