LemmaStatement: 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.

Good copy extension count

Statement

Let $J$ have $j \geq 1$ vertices and let $(A_{v} : v \in V (J))$ be a $(t, 1 / j)$ -blowup in a finite graph $G$ , with integer $t \geq 1$ . Every good embedding of $J [I]$ , $I \subseteq V (J)$ , has at least $(t / j)^{j - ∣ I ∣}$ good extensions to $J$ .

Facts & Assumptions

Given: A $(t, 1 / j)$ -blowup of a nonempty $j$ -vertex pattern, integer $t \geq 1$ , $I \subseteq V (J)$ , and a good partial embedding $ϕ$ .

[F1]

In a $(t, 1 / j)$ -blowup, every vertex of either block has at most $t / j$ wrong adjacencies in the other block; good embeddings respect the assigned labels. (Labelled blowup and good induced copy).

Proof

1.1

Induct on $r = j - ∣ I ∣$ . When $r = 0$ , the given map is its unique extension and the bound is $(t / j)^{0} = 1$ .

base

1.2

Let $r > 0$ and assume the assertion for $r - 1$ . Choose a missing label $v$ . For every $i \in I$ , [F1] bounds by $t / j$ the vertices in $A_{v}$ with the wrong adjacency to $ϕ (i)$ . The union of these forbidden sets has size at most $∣ I ∣ t / j$ : assign each forbidden vertex to its first offending label, obtaining disjoint subsets of the forbidden sets. Thus at least $t - ∣ I ∣ t / j \geq t / j > 0$ vertices are available.

F1ih

2.1

Each available $w \in A_{v}$ gives an induced extension by $v \mapsto w$ : the old map already preserves all old pairs, the new pairs have the prescribed adjacency, and disjoint blocks prevent collisions. By induction each such map has at least $(t / j)^{r - 1}$ full extensions. The families for distinct $w$ are disjoint since they differ at $v$ ; adding their cardinalities gives at least $(t / j) (t / j)^{r - 1} = (t / j)^{r}$ . This proves the induction, including the empty initial map.

step 1.1step 1.2discharge-induction∎

Source notes

Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 4.2, internal claim (1).

Depends on

Used by

Dependency tree · two levels

29 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)