Alphabeta Math
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.

Rotating-frame gradient formulation

PDF p. 2: Section 1, rotating frame and gradient flow; PDF p. 3: Section 1, rotating frame and gradient flow

Statement

Assume countable choice. Let G=(V,E) be a finite undirected graph with nonempty vertex set and symmetric adjacency matrix A, allowing self-loops. Let θ:R→TV=RV/(2πZ)V be a trajectory of the graph Kuramoto system with common intrinsic frequency ω∈R. Thus, in local real angular lifts, θ˙x=ω−∑y∈VAx,ysin⁡(θx−θy).

Define the rotating-frame state ϕ(t)=R−ωtθ(t), meaning ϕx(t)=θx(t)−ωt modulo 2π for every x. Equip TV with its flat metric, and define the homogeneous Kuramoto energy by EG(ϕ)=12∑x,y∈VAx,y(1−cos⁡(ϕx−ϕy)). Then ϕ is a downward gradient trajectory: ϕ˙=−∇EG(ϕ). Conversely, adding ωt to every coordinate of such a trajectory gives a trajectory of the homogeneous Kuramoto system.

Facts & Assumptions

[F1]

In local angular lifts the homogeneous system has components θ˙x=ω−∑yAx,ysin⁡(θx−θy); under countable choice its trajectories are defined for all real time (Graph Kuramoto differential equations, The Axiom of Countable Choice (AC_ω)).

[F2]

The phase torus is the quotient by coordinatewise integer multiples of 2π; its angular chart transitions are locally translations and its flat metric has Euclidean coefficients (Finite phase tori, local lifts and the flat metric). Diagonal rotation adds one common phase to every coordinate (Diagonal phase rotations and relative-phase coordinates).

[F3]

Sine is unchanged by shifting an argument by an integer multiple of 2π, and differentiable real functions satisfy the sum and scalar multiplication rules (Phasors, trigonometric identities and periodic derivatives).

[F4]

For this graph and energy, the flat gradient has components (∇EG(ϕ))x=∑y∈VAx,ysin⁡(ϕx−ϕy) (Homogeneous Kuramoto energy, Gradient and Hessian formulas).

[F5]

A downward gradient trajectory is an integral curve of the negative gradient; for a smooth potential on this compact phase torus, countable choice gives a unique such maximal trajectory defined on R (Gradient trajectories and complete compact phase dynamics, The Axiom of Countable Choice (AC_ω)).

Proof

Given: The graph, common frequency, homogeneous trajectory θ and rotating-frame state ϕ in the Statement.

Goal: Prove the negative-gradient equation for ϕ and the converse transformation.

1.1givenF1F2F3

Fix a time and choose local real angular lifts ux of θx. By [F2], vx(t)=ux(t)−ωt locally lifts ϕx, and vx−vy=ux−uy. The derivative rules and homogeneous equation give v˙x=u˙x−ω=−∑yAx,ysin⁡(vx−vy). This calculation is independent of lift choices by the translation transitions and sine periodicity in [F2] and [F3].

2.1F1F2F3F4F5step 1.1∎

By [F4], the right side in step 1.1 is −(∇EG(ϕ))x in every coordinate. Thus ϕ is an integral curve of the negative gradient. It is defined for all real time by [F1], so it is maximal; [F5] identifies it as the downward gradient trajectory through its initial state. Conversely, for a downward gradient trajectory with local lifts vx, put ux=vx+ωt. The same derivative and difference identities yield u˙x=ω−∑yAx,ysin⁡(ux−uy), which is the homogeneous system. The quotient construction makes these local equations independent of lifts.

Source notes

The rotating-frame formulation is attributed to Expander graphs are globally synchronizing, PDF pages 2–3. The proof above uses the stated mathematical suppliers.

Depends on

Used by · 10

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