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.
Global rotation equivalence of phase configurations
PDF p. 3: Footnote 2; PDF p. 11: Section 2.1 phase convention
Definition
Let be a finite undirected graph with nonempty vertex set and symmetric adjacency matrix . A phase is a real number modulo , and a configuration is an element . For a phase , the global rotation sends to the configuration with coordinates modulo . Configurations and are equivalent up to global rotation if there is a common real such that modulo for every . Each phase may be represented by its unique real representative in .
The homogeneous Kuramoto energy is invariant under . Assuming countable choice, the homogeneous Kuramoto dynamics , with common real frequency , are equivariant: the trajectory starting at is the rotation by of the trajectory starting at .
Definition references
Facts & Assumptions
The phase torus identifies real vectors whose corresponding coordinates differ by integer multiples of ; diagonal rotation is an action, and its orbit relation is an equivalence relation (Finite phase tori, local lifts and the flat metric, Diagonal phase rotations and relative-phase coordinates).
The integer-part lemma gives a representative of each real number modulo in (math:lem-integer-part).
Sine and cosine are -periodic, so their values on phase differences are independent of lifts (Phasors, trigonometric identities and periodic derivatives).
The energy has the displayed finite-sum formula (Homogeneous Kuramoto energy).
Under countable choice, the displayed homogeneous system has a unique trajectory through each initial configuration, defined for all real time; derivatives are taken using local real lifts (The Axiom of Countable Choice (AC_ω), Graph Kuramoto differential equations).
Justification
Given: The graph, configurations and rotation above; for the trajectory assertion assume countable choice and fix a common real frequency .
Goal: Verify the equivalence relation and representative convention, energy invariance, and equivariance of the dynamics.
1.1 The relation for all says precisely that ; the orbit relation is therefore an equivalence relation by [F1]. For any real lift, [F2] gives a congruent ; use if and otherwise. This yields a representative in . Two representatives in that interval differ by less than in absolute value, so if their difference is an integer multiple of it is zero. Thus the representative is unique. [F1, F2, algebra]
2.1 A common rotation leaves every phase difference unchanged modulo . By [F3], all sine and cosine terms in the displayed formulas are consequently unchanged. The finite energy sum is therefore unchanged by [F4]. If is a trajectory, adding the fixed phase to each local lift leaves its derivative unchanged and gives the same right-hand side at the rotated configuration. Hence is a trajectory with initial configuration . Uniqueness in [F5] identifies it with the trajectory starting there, establishing equivariance. [F3, F4, F5, step 1.1, algebra] ∎
Source notes
The rotation equivalence and the phase convention are attributed to Expander graphs are globally synchronizing, PDF page 3, footnote 2, and page 11, Section 2.1. The justification uses the mathematical inputs above.
Depends on
- Finite phase tori, local lifts and the flat metric
- Diagonal phase rotations and relative-phase coordinates
- Phasors, trigonometric identities and periodic derivatives
- Homogeneous Kuramoto energy
- Graph Kuramoto differential equations
- Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1
- The Axiom of Countable Choice (AC_ω)
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, footnote 2; PDF p. 11, Section 2.1