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.

Order parameter control of total H mass — Lemma 2.3

PDF p. 13: Lemma 2.3 and proof; PDF p. 14: Lemma 2.3 and proof

Statement

Assume countable choice. Let $G = (V, E)$ be a finite undirected graph with $n = ∣ V ∣ > 0$ , symmetric binary adjacency matrix $A$ and possible self-loops. Let $d^{*}, α \in R$ , and suppose $G$ is an $(n, d^{*}, α)$ -expander: with $J$ the all-ones matrix and $Δ_{A} = A - (d^{*} / n) J$ , this means $∥ Δ_{A} ∥ \leq α d^{*}$ in the Euclidean operator norm. Assume either $d^{*} \neq 0$ or that $G$ is connected, meaning that every two vertices can be joined by a finite path of edges. Let $θ$ be a stable state, meaning a local minimum of $E_{G} (θ) = \frac{1}{2} \sum_{x, y} A_{x y} (1 - \cos (θ_{x} - θ_{y}))$ on the phase torus. Choose representatives $θ_{x} \in (- π, π]$ and suppose the first Daido parameter $ρ_{1} (θ) = n^{- 1} \sum_{x} e^{i θ_{x}}$ is real and nonnegative. Define $H (t) = \sin^{2} (∣ t ∣)$ for $∣ t ∣ \leq π / 2$ and $H (t) = 1$ for $π / 2 \leq ∣ t ∣ \leq π$ . Then $n α^{2} \geq ρ_{1} (θ)^{2} \sum_{x \in V} H (θ_{x})$ .

In particular, the original article's connected-graph statement holds, including $d^{*} = 0$ . For the usual positive reference degree, connectedness is unnecessary.

Facts & Assumptions

[F1]

For $d^{*} > 0$ , stability and the stated normalization imply that $S_{y} = \sum_{x} (Δ_{A})_{x y} e^{i (θ_{x} - θ_{y})}$ satisfies $∣ S_{y} ∣^{2} \geq (d^{*} ρ_{1})^{2} H (θ_{y})$ for every $y$ (Centered-adjacency pointwise phase bounds). This supplier assumes countable choice (The Axiom of Countable Choice (AC_ω)).

[F2]

The centered matrix is real symmetric. The Euclidean operator norm satisfies $∥ Δ_{A} f ∥ \leq ∥ Δ_{A} ∥ ∥ f ∥$ , and the expander hypothesis is $∥ Δ_{A} ∥ \leq α d^{*}$ (Centered graph matrices and reference degree, Loewner order, Hermitian inner product, and operator norm, Adjacency spectral expander — Definition 1.3).

[F3]

For real $t$ , $e^{i t} = \cos t + i \sin t$ , $∣ e^{i t} ∣ = 1$ , $\cos^{2} t + \sin^{2} t = 1$ , and $e^{i (u - v)} = e^{i u} e^{- i v}$ (Phasors, trigonometric identities and periodic derivatives). The first order parameter is the mean phasor and satisfies $∣ ρ_{1} ∣ \leq 1$ (Daido order parameters, Bounds, saturation, and rotation of order parameters). The two branches defining $H$ therefore give $0 \leq H (t) \leq 1$ and $H (0) = 0$ (Truncated sine-square function).

[F4]

The graph adjacency entries are nonnegative and record exactly the edges; its vertex set is finite and nonempty (Adjacency, degrees, graph Laplacian, and spectral notation). A stable state is the local energy minimum specified in the statement (Equilibria, stable states, synchronized states, and spurious minima).

[F5]

Cauchy–Schwarz gives $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ in a complex inner-product space (Cauchy–Schwarz: |⟨ u,v⟩|≤‖ u‖‖ v‖, with equality exactly for linearly dependent vectors). With the matrix convention $⟨ u, v ⟩ = \sum_{x} \overline{u_{x}} v_{x}$ , this follows also by conjugating the linear-first convention (Loewner order, Hermitian inner product, and operator norm).

Proof

Given: The graph, expander bound, stable normalized state and reference parameter in the statement, with either $d^{*} \neq 0$ or connected $G$ , under countable choice.

Goal: Prove $n α^{2} \geq ρ_{1}^{2} \sum_{x} H (θ_{x})$ , including the original connected zero-reference case.

1.1F1F2F3algebra

First let $d^{*} > 0$ and set $f_{x} = e^{i θ_{x}}$ . By [F3], $∥ f ∥^{2} = n$ . Symmetry and the phasor product identity give $S_{y} = e^{- i θ_{y}} (Δ_{A} f)_{y}$ , so $∣ S_{y} ∣^{2} = ∣ (Δ_{A} f)_{y} ∣^{2}$ . Summing the pointwise bound yields $(d^{*} ρ_{1})^{2} \sum_{y} H (θ_{y}) \leq ∥ Δ_{A} f ∥^{2}$ .

1.2F2F3F4F5algebra

For completeness, let $d^{*} < 0$ and let $u$ be the all-ones vector. Since $∥ u ∥^{2} = n$ and $\sum_{x, y} A_{x y} \geq 0$ , we have $⟨ u, Δ_{A} u ⟩ = \sum_{x, y} A_{x y} - d^{*} n \geq - d^{*} n > 0$ . By Cauchy–Schwarz and the norm bound this quantity is at most $∥ u ∥ ∥ Δ_{A} u ∥ \leq ∥ Δ_{A} ∥ n \leq α d^{*} n$ . Dividing by $d^{*} n < 0$ gives $α \leq - 1$ , hence $α^{2} \geq 1$ . Since $0 \leq ρ_{1}^{2} \leq 1$ and $0 \leq H \leq 1$ , it follows that $ρ_{1}^{2} \sum_{x} H (θ_{x}) \leq n \leq n α^{2}$ .

2.1F2step 1.1algebra

By the norm bound, $∥ Δ_{A} f ∥^{2} \leq ∥ Δ_{A} ∥^{2} n \leq (α d^{*})^{2} n$ . Both quantities being squared are nonnegative by the norm inequality. Combine this with step 1.1 and divide by $(d^{*})^{2} > 0$ to obtain the conclusion when $d^{*} > 0$ , including $ρ_{1} = 0$ .

3.1F2F3F4step 2.1step 1.2algebra∎

Finally let $d^{*} = 0$ . The norm hypothesis gives $∥ A ∥ \leq 0$ , so $A = 0$ : for every coordinate vector $e_{y}$ , the norm inequality gives $A e_{y} = 0$ . Thus there are no edges. The statement requires $G$ connected in this case, so its nonempty vertex set has one vertex; two distinct vertices could not be joined by an edge path. For this single vertex the normalized mean phasor $e^{i θ_{1}}$ is real, nonnegative and of unit modulus, so equals $1$ . Its representative in $(- π, π]$ is $θ_{1} = 0$ , whence $H (θ_{1}) = 0$ . Therefore the required inequality is $α^{2} \geq 0$ . Together with the preceding cases this proves the result.

Source notes

The article's Section 2.1, PDF p. 11, explicitly says: “We assume now that G is a connected graph”. That standing assumption applies to Lemma 2.3. The two-vertex edgeless example in the retained author escalation violates it and does not refute the original article. The positive-reference proof follows the article's pointwise-to-norm argument using a fixed vector $f_{x} = e^{i θ_{x}}$ ; zero reference degree is handled directly above. The negative-reference case is a harmless extension of the local real-parameter expander definition, although the article selects $d^{*}$ as an expected average degree.

Depends on

Used by · 2

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. 6, Section 1.2 and Definition 1.3; p. 11, last paragraph of Section 2.1; pp. 13–14, Lemma 2.3 and proof