PropositionStatement: 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.

Nonnegativity and synchronized global minima

PDF p. 3: Section 1, paragraph before Definition 1.1

Statement

Assume countable choice. Let $G = (V, E)$ be a finite undirected graph with nonempty vertex set, allowing self-loops, and let $A$ be its symmetric binary adjacency matrix. For a phase state $θ \in T_{V} = (S^{1})^{V} = R^{V} / (2 π Z)^{V}$ , its homogeneous Kuramoto energy is $E_{G} (θ) = \frac{1}{2} \sum_{x, y \in V} A_{x, y} (1 - \cos (θ_{x} - θ_{y}))$ , evaluated using any real lift. Then $E_{G} (θ) \geq 0$ for every phase state. Every fully synchronized state, meaning one with $θ_{x} = θ_{y}$ in $S^{1}$ for all $x, y \in V$ , has energy zero and is a global minimizer: its energy is no greater than that of any phase state.

Statement references

Adjacency, degrees, graph Laplacian, and spectral notation

Finite phase tori, local lifts and the flat metric

Homogeneous Kuramoto energy

Equilibria, stable states, synchronized states, and spurious minima

The Axiom of Countable Choice (AC_ω)

Facts & Assumptions

[A1]

Countable choice is assumed, as in the synchronized-state definition (The Axiom of Countable Choice (AC_ω), Equilibria, stable states, synchronized states, and spurious minima).

[F1]

The graph has finitely many vertices and each adjacency entry $A_{x, y}$ is either zero or one (Adjacency, degrees, graph Laplacian, and spectral notation).

[F2]

Phase states are equivalence classes of real vectors modulo coordinatewise integer multiples of $2 π$ ; the energy formula is independent of the chosen lift (Finite phase tori, local lifts and the flat metric, Homogeneous Kuramoto energy).

[F3]

For real $u, v$ , the phasor $z (u) = e^{i u}$ has modulus one, $z (u - v) = z (u) \overline{z (v)}$ , and $\cos (u - v) = Re z (u - v)$ ; these values are unchanged by adding integer multiples of $2 π$ to either angle (Phasors, trigonometric identities and periodic derivatives).

[F4]

A fully synchronized state has equal phase coordinates in $S^{1}$ (Equilibria, stable states, synchronized states, and spurious minima).

Proof

Given: A graph and phase state as in the statement, and a real lift of that state.

Goal: Prove nonnegativity of its energy and zero energy, hence global minimality, for each fully synchronized state.

1.1F1F2F3algebra

For any real $t$ , write $z (t) = a + i b$ with real $a, b$ . By [F3], $a^{2} + b^{2} = ∣ z (t) ∣^{2} = 1$ , so $a \leq 1$ and hence $1 - \cos t \geq 0$ . Each adjacency coefficient is nonnegative by [F1]. Therefore every term in the finite ordered-pair energy sum is nonnegative, and $E_{G} (θ) \geq 0$ . The value is independent of the lift by [F2].

2.1F2F3F4step 1.1algebra∎

If the state is fully synchronized, [F4] and [F2] imply that any two lifted coordinates differ by an integer multiple of $2 π$ . By the periodicity in [F3], their phasors are equal; hence $z (θ_{x} - θ_{y}) = z (θ_{x}) \overline{z (θ_{y})} = ∣ z (θ_{x}) ∣^{2} = 1$ . Thus every cosine in the energy sum equals one and the energy is zero. Step 1.1 shows that no phase state has smaller energy, so every fully synchronized state is a global minimizer.

Source notes

The claim is attributed to Expander graphs are globally synchronizing, PDF page 3, Section 1, paragraph before Definition 1.1. The proof above is a local argument from the listed mathematical suppliers.

Depends on

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 p. 3, Section 1, paragraph before Definition 1.1