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.

Strong regularity with linearly large representative subsets and no irregular representative pair

Statement

Let $ϵ_{0} > 0$ , let $ϵ_{1} \geq ϵ_{2} \geq \dots > 0$ , and let $k_{0} \geq 1$ . There are $K$ and $δ > 0$ such that every finite graph $G$ of order at least $k_{0}$ has an equitable partition $V (G) = V_{1} ⊔ \dots ⊔ V_{k}, k_{0} \leq k \leq K,$ and nonempty subsets $W_{i} \subseteq V_{i}$ with $∣ W_{i} ∣ \geq δ ∣ V (G) ∣$ such that

every pair $(W_{i}, W_{j})$ , including $i = j$ , is $ϵ_{k}$ -regular; and
for all but at most $ϵ_{0} k^{2}$ ordered pairs $(i, j)$ , $∣ d (W_{i}, W_{j}) - d (V_{i}, V_{j}) ∣ \leq ϵ_{0} .$

Facts & Assumptions

Given: $ϵ_{0}$ , a nonincreasing positive sequence, an integer $k_{0} \geq 1$ , and a finite graph $G$ of order $n \geq k_{0}$ .

[L1]

For any prescribed minimum coarse part count $m_{0}$ , strong regularity produces equitable partitions $P, Q$ of any graph of order at least $m_{0}$ with $Q$ refining $P$ , $P$ being $ϵ_{0}$ -regular with $m_{0} \leq ∣ P ∣$ , $Q$ being $ϵ_{∣ P ∣}$ -regular, $q (Q) \leq q (P) + ϵ_{0}$ , and $∣ Q ∣$ bounded (Equitable strong regularity lemma: a very regular refinement that changes energy only slightly).

[L2]

A small energy increment makes almost all fine-pair densities close to their coarse densities (A small energy increment makes fine-pair densities close to their coarse densities almost everywhere).

[L3]

Every finite graph with at least one vertex contains a nonempty linearly large self-regular subset at any prescribed parameter (Every finite graph has a linearly large $ϵ$ -self-regular vertex subset).

[L4]

Large restrictions of regular pairs stay regular and have nearby density (Slicing lemma: large subpairs remain regular and their density shifts by at most $ϵ$ ).

[L5]

If a nonnegative integer-valued random variable has expectation below $1$ , some outcome makes it zero (The first-moment method for avoiding or forcing a finite count of bad events).

Proof

technique · constructive

1.1

Apply [L1] with minimum coarse part count $m_{0} = k_{0}$ , coarse parameter much smaller than $ϵ_{0}^{3}$ , and fine parameter, at a coarse part count $k$ , much smaller than $ϵ_{k}$ after slicing. This is legitimate because $n \geq k_{0}$ . Obtain equitable $P = {V_{1}, \dots, V_{k}}$ with $k_{0} \leq k \leq K$ and a fine equitable refinement $Q$ .

givenL1chooseconstruct

2.1

By [L2], the total ordered vertex-pair weight of fine pairs whose density differs from their coarse pair by more than $ϵ_{0} / 2$ is at most a chosen constant below $ϵ_{0}^{2}$ . The fine partition has bounded order.

step 1.1L2algebra

3.1

Independently for each $i$ , choose a fine atom $U_{i} \subseteq V_{i}$ with probability proportional to its size. Choose the parameters so that the expected number $I$ of nonregular selected ordered pairs is below $1 / 4$ , while the expected number $D$ of pairs with $∣ d (U_{i}, U_{j}) - d (V_{i}, V_{j}) ∣ > ϵ_{0} / 2$ is below $ϵ_{0} k^{2} / 4$ .

step 1.1step 2.1algebra

4.1

Inside every selected atom $U_{i}$ , apply [L3] at a much smaller parameter and obtain $W_{i} \subseteq U_{i}$ of size at least a fixed fraction of $∣ U_{i} ∣$ . Because both partition orders are bounded and equitable, there is a uniform $δ > 0$ with $∣ W_{i} ∣ \geq δ n$ .

step 3.1L3choose

4.2

Let $X = I + 1_{{D > ϵ_{0} k^{2}}}$ . Since $1_{{D > ϵ_{0} k^{2}}} \leq D / (ϵ_{0} k^{2})$ , step 3.1 gives $E X < 1 / 2$ . By [L5] there is a selection with $X = 0$ : it has no irregular selected pair and at most $ϵ_{0} k^{2}$ density failures.

step 3.1L5algebrachoose

5.1

On every fine-regular selected cross-pair, [L4] makes $(W_{i}, W_{j})$ $ϵ_{k}$ -regular and changes its density by at most $ϵ_{0} / 2$ . Each diagonal pair is $ϵ_{k}$ -regular by the self-regular choice in step 4.1.

step 3.1step 4.1L4algebra

6.1

For that selection, step 5.1 gives regularity for every representative pair, while step 4.2 gives the density-approximation exception bound. Step 4.1 gives the common linear lower bound and makes each $W_{i}$ nonempty, and step 1.1 gives $k_{0} \leq k \leq K$ , completing the construction.

step 4.1step 5.1step 4.2discharge-construct∎

Depends on

Used by

Induced graph removal lemma for a fixed graph Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 24 results over 8 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.8.9 (standard reference, not scraped)
D. Conlon and J. Fox, Graph removal lemmas, sec. 2.3 (standard reference, not scraped)