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.

Bounds, saturation, and rotation of order parameters

PDF p. 11: Section 2.1 prose following (2.7)

Statement

Let $V$ be a nonempty finite vertex set, $n = ∣ V ∣$ , and let $θ$ assign to each vertex a phase, meaning a real angle modulo $2 π$ . For every integer $k \geq 1$ , the Daido order parameter $ρ_{k} (θ) = n^{- 1} \sum_{x \in V} e^{i k θ_{x}}$ satisfies $∣ ρ_{k} ∣ \leq 1$ . If $∣ ρ_{1} ∣ = 1$ , all phases coincide modulo $2 π$ . If $∣ ρ_{k} ∣ = 1$ , the phasors $e^{i θ_{x}}$ lie in one common rotation of the $k$ th roots of unity, the complex numbers $w$ with $w^{k} = 1$ .

For nonzero $ρ_{1}$ , an argument of $ρ_{1}$ is the phase $a$ satisfying $e^{i a} = ρ_{1} / ∣ ρ_{1} ∣$ ; it is the direction of the mean phasor and is called the average phase. A global rotation, meaning addition of one common phase to every $θ_{x}$ , can make $ρ_{1}$ real and nonnegative. If $ρ_{1} = 0$ , it is already zero and has no argument. After rotation, each phase has a unique representative in $(- π, π]$ .

Statement references

Daido order parameters

Global rotation equivalence of phase configurations

Diagonal phase rotations and relative-phase coordinates

Rigidity and rotation of a unit-phasor average

Facts & Assumptions

[F1]

The Daido parameter is the average of the phasors $e^{i k θ_{x}}$ , independently of the chosen real representatives of the phases (Daido order parameters).

[F2]

For a nonempty finite family of unit phasors, the modulus of their average is at most one and equals one exactly when all the phasors coincide. For positive integer $k$ , equality for the average of $e^{i k θ_{x}}$ is equivalent to the $e^{i θ_{x}}$ lying in a common rotation of the $k$ th roots of unity (Rigidity and rotation of a unit-phasor average).

[F3]

A global rotation adds the same phase to each coordinate. For the mean phasor $m$ , rotation by $c$ changes it to $e^{i c} m$ ; if $m \neq 0$ , rotation by minus its argument makes it positive real (Diagonal phase rotations and relative-phase coordinates, Justification).

[F4]

For a finite undirected graph with nonempty vertex set and symmetric adjacency matrix, each phase has a unique representative in $(- π, π]$ (Global rotation equivalence of phase configurations).

Proof

Given: A nonempty finite set $V$ , phases $θ_{x}$ for $x \in V$ , and an integer $k \geq 1$ .

Goal: Establish the modulus and saturation claims, the interpretation of the argument, and the rotation and representative convention.

1.1F1F2given

Choose real representatives of the finitely many phases. By [F1], $ρ_{k}$ is their average $n^{- 1} \sum_{x} e^{i k θ_{x}}$ . Applying [F2] gives $∣ ρ_{k} ∣ \leq 1$ and, when equality holds, places the phasors $e^{i θ_{x}}$ in a common rotation of the $k$ th roots of unity. For $k = 1$ , the only first root of unity is $1$ , so equality makes all phasors equal and hence all phases coincide modulo $2 π$ .

1.2F1F3

By [F1], $ρ_{1}$ is the mean phasor, so for $ρ_{1} \neq 0$ its argument is precisely the direction described as average phase. By [F3], rotating by minus that argument makes the new $ρ_{1}$ equal to $∣ ρ_{1} ∣ > 0$ . If $ρ_{1} = 0$ , the rotation formula in [F3] leaves it zero; in this case no argument is defined and no preferred rotation is selected.

2.1F4step 1.1step 1.2construct∎

To apply [F4], equip $V$ with the edgeless graph $G = (V, \emptyset)$ and its zero adjacency matrix. This graph is finite and undirected, its vertex set is nonempty, and its adjacency matrix is symmetric. Hence [F4] supplies the unique representative of each rotated phase in $(- π, π]$ . No connectedness assumption is required by [F4]. Together with steps 1.1 and 1.2 this proves the claims.

Source notes

The claims and conventions are attributed to Expander graphs are globally synchronizing, PDF page 11, Section 2.1. The article subsequently assumes the graph is connected; connectedness is not needed for the finite phasor argument above.

Depends on

Used by · 16

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 page 11, Section 2.1, prose following equation (2.7)