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.

First and second order parameter inequality — Lemma 2.1

PDF p. 12: Lemma 2.1, equations (2.8), (2.9), and proof; PDF p. 13: Lemma 2.1, equations (2.8), (2.9), and proof

Statement

Assume countable choice. Let $G = (V, E)$ be a finite connected undirected $(n, d^{*}, α)$ -expander with $n = ∣ V ∣ > 0$ , $d^{*} \geq 0$ , $α \geq 0$ , and symmetric binary adjacency matrix $A$ , allowing self-loops. Connectedness means that the loop-free support graph on $V$ , with an edge ${x, y}$ exactly when $x \neq y$ and $A_{x y} = 1$ , is connected: every two vertices are joined by a path in this finite simple graph. A path of length zero joins a vertex to itself. Here $d (x) = \sum_{y} A_{x y}$ counts a loop once, and the expander condition is $∥ A - (d^{*} / n) J ∥ \leq α d^{*}$ , where $J$ is the all-ones matrix. Let $θ$ be a stable state, meaning a local minimum of the homogeneous Kuramoto energy. Set $ρ_{k} = n^{- 1} \sum_{x} e^{i k θ_{x}}$ , and adopt the article's common-rotation convention $ρ_{1} \in [0, 1]$ with phase representatives in $(- π, π]$ . Then

$ρ_{1}^{2} \geq \frac{1 + ∣ ρ_{2} ∣^{2}}{2} - 2 α .$

If $G$ is $d^{*}$ -regular, then

$ρ_{1}^{2} \geq \frac{1 + ∣ ρ_{2} ∣^{2}}{2} - \frac{3}{2} α .$

The second bound also holds whenever $\sum_{x, y} A_{x y} = d^{*} n$ . In particular it holds when the graph has no self-loops and $∣ E ∣ = d^{*} n / 2$ . These are the proved assertions exported by this item; the additional source assertion discussed in Source notes is not an available premise.

Statement references

Adjacency, degrees, graph Laplacian, and spectral notation

Adjacency spectral expander — Definition 1.3

Equilibria, stable states, synchronized states, and spurious minima

Daido order parameters

Bounds, saturation, and rotation of order parameters

The Axiom of Countable Choice (AC_ω)

Finite symmetric networks and loop removal

Connected graphs and connected components defined by the existence of vertex paths

Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges

Facts & Assumptions

[F1]

The graph has symmetric binary adjacency, a loop contributes one to a row sum, and $d^{*}$ -regularity means that every row sum equals $d^{*}$ . If $ℓ$ is the number of loops, then $\sum_{x, y} A_{x y} = 2 ∣ E ∣ - ℓ$ , because a non-loop edge contributes two ordered entries and a loop contributes one (Adjacency, degrees, graph Laplacian, and spectral notation).

[F2]

The spectral-expander hypothesis is $∥ A - (d^{*} / n) J ∥ \leq α d^{*}$ . With the stated Daido parameters, the spectral-phase-sums lemma gives

$\sum_{x, y} A_{x y} \cos (θ_{x} - θ_{y}) \leq d^{*} n ∣ ρ_{1} ∣^{2} + α d^{*} n,$

and

$\sum_{x, y} A_{x y} \cos^{2} (θ_{x} - θ_{y}) \geq \frac{d^{*} n}{2} (1 + ∣ ρ_{2} ∣^{2}) - α d^{*} n .$

If $\sum_{x, y} A_{x y} = d^{*} n$ , the last error improves from $α d^{*} n$ to $α d^{*} n / 2$ (Adjacency spectral expander — Definition 1.3, Spectral estimates for phase Fourier sums, Daido order parameters).

[F3]

Under countable choice, stability as a local energy minimum implies

$\sum_{x, y} A_{x y} \cos (θ_{x} - θ_{y}) \geq \sum_{x, y} A_{x y} \cos^{2} (θ_{x} - θ_{y}) .$

This includes the self-loop convention: each diagonal term has $\cos 0 = \cos^{2} 0 = 1$ and cancels from the difference (Equilibria, stable states, synchronized states, and spurious minima, Second-order necessary conditions for stable states, The Axiom of Countable Choice (AC_ω)).

[F4]

The order parameters have modulus at most one, and common rotation can make $ρ_{1}$ real and nonnegative without changing any phase difference; representatives may then be chosen in $(- π, π]$ (Bounds, saturation, and rotation of order parameters).

[F5]

Deleting the diagonal entries of the symmetric binary matrix $A$ gives the finite simple support graph with edges ${x, y}$ exactly when $x \neq y$ and $A_{x y} = 1$ (Finite symmetric networks and loop removal). Connectedness means that every pair of vertices in this nonempty graph is joined by a path (Connected graphs and connected components defined by the existence of vertex paths). A path is a finite vertex list whose consecutive vertices are adjacent and whose vertices are distinct; its length is the number of edges traversed. In particular, the single-vertex list is a path of length zero (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges).

Proof

Given: The graph, nonnegative reference degree and expansion parameter and stable state in the Statement, under countable choice.

Goal: Prove the general estimate, the regular-graph refinement and the stated ordered-sum and loop-free sufficient conditions.

Proof technique: direct.

1.1F1F2F3F4F5givenalgebra

If $d^{*} = 0$ , the norm bound in [F2] forces $A = 0$ . Its loop-free support graph from [F5] is therefore edgeless. A path between distinct vertices would have positive length and traverse an edge, so [F5] and connectedness force $n = 1$ . The order-parameter formula gives $∣ ρ_{1} ∣ = ∣ ρ_{2} ∣ = 1$ , and the normalization in [F4] gives $ρ_{1} = 1$ , so both asserted inequalities hold because $α \geq 0$ . Hence it remains to treat $d^{*} > 0$ . By [F4], the normalization gives $∣ ρ_{1} ∣^{2} = ρ_{1}^{2}$ . Combining the upper bound in [F2], the stability inequality in [F3], and the general lower bound in [F2] yields $d^{*} n ρ_{1}^{2} + α d^{*} n \geq d^{*} n (1 + ∣ ρ_{2} ∣^{2}) / 2 - α d^{*} n$ . Divide by the positive number $d^{*} n$ and subtract $α$ to obtain the first asserted bound.

2.1F1F2F3F4givenstep 1.1algebra∎

In the remaining case $d^{*} > 0$ , if $\sum_{x, y} A_{x y} = d^{*} n$ , use instead the improved lower bound in [F2]. The same comparison gives $d^{*} n ρ_{1}^{2} + α d^{*} n \geq d^{*} n (1 + ∣ ρ_{2} ∣^{2}) / 2 - α d^{*} n / 2$ , and division by $d^{*} n > 0$ gives the second asserted bound. For a $d^{*}$ -regular graph, summing the row sums from [F1] gives $\sum_{x, y} A_{x y} = d^{*} n$ , including when loops are present. For a loop-free graph with $∣ E ∣ = d^{*} n / 2$ , the counting identity in [F1] gives the same equality. Thus every stated refinement follows.

Source notes

The two displayed inequalities in the Statement reproduce the conclusions of the printed Lemma 2.1, equations (2.8) and (2.9), in Expander graphs are globally synchronizing, PDF page 12. The proof above follows its Hessian-and-spectral argument on pages 12–13 using the authored suppliers. The connectedness and phase conventions are stated immediately before the lemma on page 11; the row-sum degree convention counting self-loops once is explicit on page 18. No underlying proof from reference [26] was independently read or imported here.

The final paragraph of the article's proof, PDF page 13, additionally says: “If the number of edges $∣ E ∣$ is equal to $d^{*} n / 2$ (for example, if the graph is $d^{*}$ -regular), then we use $⟨ h, A h ⟩ = d^{*} n$ instead of $∣ ⟨ h, A h ⟩ - d^{*} n ∣ \leq α d^{*} n$ , which leads to the improved inequality (2.9).” This additional assertion is preserved as an attributed unresolved source claim, not as a theorem or a proof input. It extends beyond the regular-graph conclusion of the printed lemma. Consumers may use only the proved Statement, not this unresolved assertion.

The equality inference in that paragraph fails with loops. In a connected graph on two vertices having their connecting edge and both loops, $A = J_{2}$ , $n = 2$ , $∣ E ∣ = 3$ , $d^{*} = 3$ and $α = 1 / 3$ . The centered matrix is $- J_{2} / 2$ with eigenvalues $- 1, 0$ , so the expander bound holds. The synchronized state $θ = (0, 0)$ globally minimizes the nonnegative energy and is stable; its normalized parameters are $ρ_{1} = ρ_{2} = 1$ . Nevertheless $∣ E ∣ = d^{*} n / 2$ while $⟨ 1, A 1 ⟩ = 4 \neq 6 = d^{*} n$ . This refutes that equality inference under the original connectedness and loop conventions. It does not refute the improved inequality itself, which holds in this example. No counterexample to that additional inequality or complete proof of it is claimed.

The correct identity is $⟨ 1, A 1 ⟩ = 2 ∣ E ∣ - ℓ$ , with $ℓ$ the number of loops. Substitution into the article's spectral-and-Hessian argument, for $d^{*} > 0$ under $∣ E ∣ = d^{*} n / 2$ , gives the supported estimate $ρ_{1}^{2} \geq (1 + ∣ ρ_{2} ∣^{2}) / 2 - 3 α / 2 - ℓ / (2 d^{*} n)$ . Removing the final loop term needs a further argument. The full printed lemma, including its regular case with loops allowed, is proved above without that additional assertion.

Depends on

Used by · 6

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 — Abdalla, Bandeira, Kassabov, Souza, Strogatz, Townsend (2026) · PDF p. 11, Section 2.1 conventions; pp. 12–13, Lemma 2.1, equations (2.8)–(2.9) and proof; p. 18, opening of Section 3