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.

Qid bipartite density trimming

Statement

Let $A, B$ be disjoint finite vertex sets and $c \geq 0$ . If $e_{G} (A, B) \leq c ∣ A ∣ ∣ B ∣$ , then some $A^{'} \subseteq A$ with $∣ A^{'} ∣ \geq ∣ A ∣ / 2$ has $∣ N_{G} (v) \cap B ∣ \leq 2 c ∣ B ∣$ for every $v \in A^{'}$ . Empty sets are permitted. This is a bound from $A^{'}$ into $B$ .

Facts & Assumptions

Given: Disjoint finite $A, B$ , $c \geq 0$ , and $e_{G} (A, B) \leq c ∣ A ∣ ∣ B ∣$ .

[F1]

For a finite incidence relation, summing row sizes counts all incidences; empty index sets are permitted. (Double counting: $\sum_{x \in X} ∣ R_{x} ∣ = ∣ R ∣ = \sum_{y \in Y} ∣ R^{y} ∣$ for a relation between finite sets).

Proof

1.1F1given

Let $d (v) = ∣ N_{G} (v) \cap B ∣$ . Counting the finite relation of adjacent pairs by its $A$ fibres gives $\sum_{v \in A} d (v) = e_{G} (A, B)$ , including empty sets by [F1]. If $A$ or $B$ is empty, take $A^{'} = A$ . If $c = 0$ , the sum of nonnegative integer degrees is zero, so every degree is zero and again take $A^{'} = A$ .

2.1step 1.1algebra∎

Otherwise $c ∣ B ∣ > 0$ . Let $D = {v \in A : d (v) > 2 c ∣ B ∣}$ . If $D$ is nonempty, $2 c ∣ B ∣ ∣ D ∣ < \sum_{v \in D} d (v) \leq c ∣ A ∣ ∣ B ∣$ , hence $∣ D ∣ < ∣ A ∣ / 2$ . If $D$ is empty the same required conclusion $∣ D ∣ \leq ∣ A ∣ / 2$ holds. Thus $A^{'} = A ∖ D$ has at least half the vertices and every degree in it is at most $2 c ∣ B ∣$ .

Source notes

Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 4.1.

Depends on

Used by

Dependency tree · two levels

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