Ordinary differential equations

The Lean Pool projects whose card's first MSC2020 code is in class 34, Ordinary differential equations: 1 article.

TheoremFinite-N Kuramoto Synchronization#

Formalizes the finite-N Kuramoto model of coupled phase oscillators: the order parameter and its unit bound, the potential/force gradient identities, smoothness and local Lipschitz continuity of the vector field with ODE existence and uniqueness, Lyapunov descent along trajectories, pairwise and semicircle contraction estimates, Hebbian phase/weight dynamics, and full convergence to synchrony under all-to-all coupling from initial phases in an open semicircle.

Quoted from the card LeanPool/projects/kuramoto.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

• kuramotoR_norm_le_one (theorem; a main declaration), declared in LeanPool/Kuramoto/OrderParameter.lean, line 28: “The Kuramoto order parameter has norm at most one for any phase configuration.”
• weighted_lyapunov_descent (theorem; a main declaration), declared in LeanPool/Kuramoto/Weighted.lean, line 185: “The weighted Kuramoto potential is non-increasing along the gradient flow, since the sum of force times potential-derivative over all oscillators is at most zero.”
• allToAll_convergence_to_synchrony (theorem), declared in LeanPool/Kuramoto/Frontier.lean, line 1019: “Under all-to-all coupling with positive strength and initial phases in an open semicircle, the order parameter norm tends to one, i.e. the oscillators synchronize.”

Project

• Authors: Ben Cassie.
• Source: Finite-N Kuramoto synchronization: order-parameter bounds and Lyapunov descent by Ben Cassie.
• Project repository: velvetmonkey/kuramoto-lean.
• Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
• License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
• MSC2020: 34D06.
• In Lean Pool: LeanPool/Kuramoto, from the card LeanPool/projects/kuramoto.yaml.

Sources

• Lean Pool at 2b205bf9: LeanPool/projects/kuramoto.yaml
• Lean Pool at 2b205bf9: LeanPool/Kuramoto

LeankuramotoR_norm_le_one · weighted_lyapunov_descent

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.