TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Triangle counting lemma for three pairwise regular vertex sets

Statement

Let $X, Y, Z$ be pairwise disjoint nonempty vertex sets such that all three cross-pairs are $ϵ$ -regular. Write $d (X, Y) = a, d (X, Z) = b, d (Y, Z) = c,$ and suppose $a, b \geq 2 ϵ$ . Then the number of ordered triples $(x, y, z) \in X \times Y \times Z$ spanning a triangle is at least $(1 - 2 ϵ) (a - ϵ) (b - ϵ) (c - ϵ) ∣ X ∣ ∣ Y ∣ ∣ Z ∣ .$ When $c < ϵ$ , the right side is nonpositive and the inequality is interpreted literally.

Facts & Assumptions

Given: Three vertex sets satisfying the hypotheses in the Statement.

[L1]

In an $ϵ$ -regular pair $(X, Y)$ of density $d$ , and for $Y^{'} \subseteq Y$ with $∣ Y^{'} ∣ \geq ϵ ∣ Y ∣$ , fewer than $ϵ ∣ X ∣$ vertices $x \in X$ have $∣ N (x) \cap Y^{'} ∣ < (d - ϵ) ∣ Y^{'} ∣$ , and separately fewer than $ϵ ∣ X ∣$ have $∣ N (x) \cap Y^{'} ∣ > (d + ϵ) ∣ Y^{'} ∣$ (In a regular pair, fewer than $ϵ ∣ X ∣$ vertices have too small a degree into a large subset, and fewer than $ϵ ∣ X ∣$ have too large a degree).

[L2]

If $(Y, Z)$ is $ϵ$ -regular, then any subsets of sizes at least $ϵ ∣ Y ∣$ and $ϵ ∣ Z ∣$ have density at least $d (Y, Z) - ϵ$ ( $ϵ$ -regular pairs and self-regular vertex sets).

Proof

technique · direct

1.1

By [L1], fewer than $ϵ ∣ X ∣$ vertices have fewer than $(a - ϵ) ∣ Y ∣$ neighbours in $Y$ , and fewer than $ϵ ∣ X ∣$ have fewer than $(b - ϵ) ∣ Z ∣$ neighbours in $Z$ . Thus at least $(1 - 2 ϵ) ∣ X ∣$ vertices $x \in X$ satisfy both lower bounds.

givenL1algebra

2.1

For each such $x$ , put $Y_{x} = N (x) \cap Y$ and $Z_{x} = N (x) \cap Z$ . Since $a, b \geq 2 ϵ$ , step 1.1 gives $∣ Y_{x} ∣ \geq ϵ ∣ Y ∣$ and $∣ Z_{x} ∣ \geq ϵ ∣ Z ∣$ .

step 1.1algebra

3.1

By [L2], there are at least $(c - ϵ) ∣ Y_{x} ∣ ∣ Z_{x} ∣$ edges between $Y_{x}$ and $Z_{x}$ , and each produces a unique triangle $(x, y, z)$ .

step 2.1L2

4.1

Since $a \leq 1$ and $a \geq 2 ϵ$ , we have $ϵ \leq 1 / 2$ , so $1 - 2 ϵ \geq 0$ . If $c < ϵ$ then $c - ϵ < 0$ makes the claimed lower bound nonpositive, while the triangle count is nonnegative, so the inequality holds. If $c \geq ϵ$ then $c - ϵ \geq 0$ , so substituting the bounds $∣ Y_{x} ∣ \geq (a - ϵ) ∣ Y ∣$ and $∣ Z_{x} ∣ \geq (b - ϵ) ∣ Z ∣$ of step 1.1 into $(c - ϵ) ∣ Y_{x} ∣ ∣ Z_{x} ∣$ preserves the inequality of step 3.1; summing over the at least $(1 - 2 ϵ) ∣ X ∣$ good choices of $x$ gives exactly the claimed product bound.

step 1.1step 3.1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 5 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Y. Zhao, Graph Theory and Additive Combinatorics, Theorem 2.2.1 (standard reference, not scraped)