LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Cheeger sweep and layer cake

Statement

For a finite $d$ -regular graph on $n \geq 2$ vertices and a nonnegative $f$ supported on at most $n / 2$ vertices, use the unnormalized inner product $⟨ f, g ⟩_{0} = \sum_{v} f (v) g (v)$ and energy $E (f) = ⟨ f, (I - M) f ⟩_{0}$ . Then $h ∥ f ∥_{0}^{2} \leq \frac{1}{d} \sum_{u < v} A_{u v} ∣ f (u)^{2} - f (v)^{2} ∣ \leq \sqrt{2 E (f) ∥ f ∥_{0}^{2}} .$ Also $γ \leq 2 h$ , and there exists a nonzero nonnegative function $g$ , supported on at most $n / 2$ vertices, with $E (g) \leq γ ∥ g ∥_{0}^{2}$ : namely, the positive part of a suitable sign of a nonzero mean-zero $μ_{2}$ eigenvector. These are the indicator and positive-part conclusions of the preceding lemma in the unnormalized inner product.

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

Let $n \geq 2$ and use normalized edge expansion $h$ and algebraic gap $γ = 1 - μ_{2}$ . Then $γ \leq 2 h$ . Moreover some sign of a nonzero mean-zero $μ_{2}$ eigenvector has positive part $f \neq 0$ supported on at most $n / 2$ vertices and satisfying $⟨ f, (I - M) f ⟩ \leq γ ∥ f ∥^{2}$ . (Cheeger indicator and positive part energy).

[F2]

For vectors $u, v$ in a real or complex inner product space, $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥ .$ Equality holds if and only if $u$ and $v$ are linearly dependent, including the case in which either vector is zero. (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

1.1

Order coordinates $f_{1} \geq \dots \geq f_{n} \geq 0$ and let $a = ∣ supp f ∣ \leq n / 2$ . Put $f_{a + 1} = 0$ . Each difference of squared values telescopes across initial segments, so the middle numerator equals $\sum_{i = 1}^{a} (f_{i}^{2} - f_{i + 1}^{2}) cut ({1, \dots, i})$ . Each cut is at least $d h i$ , and $\sum_{i = 1}^{a} i (f_{i}^{2} - f_{i + 1}^{2}) = \sum_{i} f_{i}^{2}$ . For $a = 0$ all sums are zero.

givenalgebra

2.1

Factor $∣ f (u)^{2} - f (v)^{2} ∣ = ∣ f (u) - f (v) ∣ ∣ f (u) + f (v) ∣$ and apply Cauchy–Schwarz with weights $A_{u v}$ for $u < v$ . The first squared sum is $d E (f)$ ; the second is at most $2 \sum_{u < v} A_{u v} (f (u)^{2} + f (v)^{2}) \leq 2 d ∥ f ∥_{0}^{2}$ . Dividing by $d$ proves the upper estimate. Loop terms vanish in the difference sum and only reduce the nonloop degree sum.

F2step 1.1

3.1

Multiplying all normalized inner products by $n$ leaves the preceding lemma's inequalities unchanged; thus its positive-part and indicator estimates have exactly the stated unnormalized form. No division by $E (f)$ or $∥ f ∥_{0}$ was used above, so zero functions and zero energy are included.

F1step 2.1∎

Depends on

Used by

Cheeger inequalities for finite regular graphs Theorem

Dependency tree · two levels

9 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

Hoory–Linial–Wigderson, Expander Graphs and Their Applications, May 2006 draft; §4.5.2 Lemmas4.12–4.13, pp41–42. (standard reference, not scraped)