LemmaStatement: AI-adaptedProof: AI-generated

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.

Large-set amplification — Lemma 4.3

PDF p. 23: Lemma 4.3; PDF p. 26: Proof of Lemma 4.3

Statement

Assume countable choice. Let $G = (V, E)$ be an $(n, d^{*}, α, c^{-}, c^{+})$ -expander with real $d^{*}, α, c^{-}, c^{+}$ and $c^{+} \neq c^{-}$ . Assume either $d^{*} \neq 0$ or that $G$ is connected, meaning that every two vertices can be joined by a finite path of edges. Thus $n = ∣ V ∣ > 0$ , $∥ A - (d^{*} / n) J ∥ \leq α d^{*}$ , and $c^{-} d^{*} I ⪯ L - d^{*} I + (d^{*} / n) J ⪯ c^{+} d^{*} I$ . Let $θ$ be a stable state, meaning a local minimum of the graph Kuramoto energy. Choose its phase origin so that $n^{- 1} \sum_{x \in V} e^{i θ_{x}}$ is real and nonnegative. For $0 \leq ψ \leq π$ , write $C_{ψ} = {x \in V : ∣ θ_{x} ∣ \geq ψ}$ using principal representatives in $(- π, π]$ .

Let $0 < ε < 1 + c^{-}$ and $0 < γ < β \leq π / 2$ , and suppose $∣ C_{β} ∣ > 0$ . If

$\sin (β - γ) \geq \frac{2 (1 + c^{+} + α) ∣ C_{π / 2} ∣}{(1 + c^{-} - ε) ∣ C_{β} ∣},$

then

$∣ C_{γ} ∣ \geq \min {(1 + \frac{ε}{c^{+} - c^{-}}) ∣ C_{β} ∣, \frac{n}{2}} .$

Statement references

Two-sided spectral expander — Definition 1.9

Equilibria, stable states, synchronized states, and spurious minima

Phase tail sets for amplification

The Axiom of Countable Choice (AC_ω)

Facts & Assumptions

[F1]

The expander inequalities in the Statement use nonnegative quadratic-form order. The adjacency matrix is symmetric and nonnegative, $L 1 = 0$ , and $J 1 = n 1$ (Two-sided spectral expander — Definition 1.9).

[F2]

For $0 < γ < β \leq π / 2$ , the phase tails obey $C_{π / 2} \subseteq C_{β} \subseteq C_{γ}$ . For subsets $P, Q \subseteq V$ , their ordered adjacency count is $e (P, Q) = \sum_{x \in P, y \in Q} A_{x y}$ , and $Q^{c} = V ∖ Q$ (Phase tail sets for amplification, Oriented edge count between sets).

[F3]

Under the stated stability, alignment, expander and countable-choice hypotheses, $\sin (β - γ) e (C_{β}, C_{γ}^{c}) \leq (1 + c^{+} + α) d^{*} ∣ C_{π / 2} ∣$ (Almost antisymmetry and summed kernel bounds, The Axiom of Countable Choice (AC_ω)).

[F4]

If $X \subseteq Y$ , $∣ Y ∣ \leq n / 2$ , and $∣ Y ∣ < (1 + ε / (c^{+} - c^{-})) ∣ X ∣$ , then $e (X, Y^{c}) > (1 + c^{-} - ε) (d^{*} / n) ∣ X ∣ ∣ Y^{c} ∣$ , under the positive-degree and nonzero-gap hypotheses of the Statement (Strict forms of the nested mixing estimates — Remark 3.9).

[F5]

Sine is nonnegative on $[0, π]$ (Angular order and elementary inverse-trigonometric bounds). If $0 < γ < β \leq π / 2$ , then $0 < β - γ < π$ , so $\sin (β - γ) > 0$ (Pi is the first positive zero of sine).

[F6]

The finite graph is nonempty and its binary adjacency matrix records its edges (Adjacency, degrees, graph Laplacian, and spectral notation). The normalized first Daido parameter is the mean of the unit phasors, and each phase has a unique representative in $(- π, π]$ (Bounds, saturation, and rotation of order parameters).

Proof

Given: The graph, state, parameters and sine inequality in the Statement.

Goal: Prove the stated lower bound for $∣ C_{γ} ∣$ .

1.1F1F2algebra

If $d^{*} < 0$ , the difference of the two quadratic-form bounds in [F1] gives $(c^{+} - c^{-}) d^{*} \geq 0$ . Thus the nonzero gap obeys $c^{+} - c^{-} < 0$ . Since $ε > 0$ , the factor $q = 1 + ε / (c^{+} - c^{-})$ is less than $1$ . Tail nesting gives $∣ C_{γ} ∣ \geq ∣ C_{β} ∣ \geq q ∣ C_{β} ∣$ , hence the required minimum bound.

1.2F1F2F6algebra

If $d^{*} = 0$ , the expander norm condition gives $A = 0$ , since $∥ A e_{y} ∥ \leq ∥ A ∥ ∥ e_{y} ∥ = 0$ for every coordinate vector $e_{y}$ . The statement then requires connectedness, so [F6] implies $n = 1$ : an edgeless graph cannot have a path between two distinct vertices. The sole phasor is real and nonnegative by normalization, and has unit modulus, so equals $1$ . Its principal representative is $0$ . Therefore $C_{β}$ is empty for $β > 0$ , contradicting the nonempty-denominator hypothesis. This case has no admissible inputs.

1.3F1algebra

We may now assume $d^{*} > 0$ . Testing the difference of the two quadratic-form bounds in [F1] on a nonzero vector shows $(c^{+} - c^{-}) d^{*} \geq 0$ . Since $d^{*} > 0$ and the gap is nonzero, $c^{+} - c^{-} > 0$ . The norm bound gives $α \geq 0$ . Testing the upper Laplacian bound on $1$ gives $c^{+} \geq 0$ , because the centered Laplacian annihilates $1$ . Thus $B : = 1 + c^{+} + α > 0$ , and $k : = 1 + c^{-} - ε > 0$ by hypothesis.

2.1F2F4step 1.3algebra

Suppose the conclusion fails. Put $X = C_{β}$ , $Y = C_{γ}$ , $a = ∣ X ∣$ , $r = ∣ C_{π / 2} ∣$ , and $t = ∣ Y^{c} ∣$ . By [F2], $X \subseteq Y$ ; failure of the conclusion gives $∣ Y ∣ < n / 2$ and $∣ Y ∣ < (1 + ε / (c^{+} - c^{-})) a$ . Hence $t > n / 2$ . Applying [F4] gives $e (X, Y^{c}) > k (d^{*} / n) a t$ .

3.1F3F5step 1.3step 2.1algebra∎

Put $s = \sin (β - γ)$ . By [F5], $s > 0$ , so step 2.1 gives $s e (X, Y^{c}) > s k (d^{*} / n) a t$ . The hypothesis, $a > 0$ , and $k > 0$ give $s k a \geq 2 B r$ . Consequently $s e (X, Y^{c}) > 2 B r (d^{*} / n) t \geq B r d^{*}$ ; the last inequality also holds when $r = 0$ . This contradicts [F3]. Therefore the conclusion holds.

Source notes

The article’s Lemma 4.3 states the same displayed amplification implication for a stable state on an $(n, d^{*}, α, c^{-}, c^{+})$ -expander with $0 < ε < 1 + c^{-}$ and $0 < γ < β \leq π / 2$ . Its displayed fractions require $∣ C_{β} ∣$ and $c^{+} - c^{-}$ to be nonzero. The article’s earlier phase convention makes the first order parameter real and nonnegative. Section 2.1, PDF p. 11, also explicitly assumes that $G$ is connected. At $d^{*} = 0$ , connectedness and phase normalization force a single vertex at phase zero, contradicting the nonempty denominator $∣ C_{β} ∣ > 0$ . Thus the original connected-graph claim is preserved. For $d^{*} > 0$ , connectedness is unnecessary; negative real reference parameters give the conclusion directly by nesting. This source note attributes the original formulation and does not use the article as a proof premise.

Depends on

Used by · 3

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Expander graphs are globally synchronizing · PDF pp. 23–24, Lemma 4.3; p. 26, proof; p. 11, phase convention