Watch a fleet of agents provably reach consensus — and what happens the instant you break the guarantee’s assumptions.
‖R‖ is the exact quantity the theorem bounds:
‖kuramotoR N (θ t)‖ → 1. Dynamics on this page:
dθᵢ/dt = K·Σⱼ Wᵢⱼ·sin(θⱼ − θᵢ) — the theorem’s vector field with no
hidden terms (no frequency detuning, no noise, no normalisation, no mean-field pull).
Classical RK4, Δt = 0.02, seeded and deterministic.
All coupling between the two halves of the fleet is now zero, so mini≠j Wij = 0: no positive floor exists and the theorem is silent. This coupling — two disconnected islands — is one it permits where global consensus genuinely fails: each island agrees internally, the fleet never does, and ‖R‖ plateaus below 1. Note the claim carefully: cutting the floor does not always break synchrony; it removes the guarantee. This is a witness that the guarantee is gone.
The fleet now starts as two antipodal clusters, so the initial phase diameter is exactly π — not inside an open semicircle. In exact arithmetic this configuration is a stationary solution of the very same dynamics (every phase difference is 0 or π, so every coupling term vanishes): it would never move toward consensus. Watch the numerics closely: ‖R‖ sits at 0 on this knife-edge until floating-point crumbs (~10⁻¹⁶) tip the integrator off the unstable equilibrium — after which this particular fleet happens to re-synchronise. The theorem never promised that. Outside the semicircle the guarantee is gone and the outcome is luck, not law: the hypothesis is sufficient, not necessary — violating it doesn’t force failure, it removes the guarantee. This is a witness that the guarantee is gone.
theorem floor_coupling_convergence_to_synchrony
(K : ℝ) (hK : 0 < K) (N : ℕ) (hN : 2 ≤ N)
(W : Fin N → Fin N → ℝ) (hWsym : ∀ i j, W i j = W j i)
(w_min : ℝ) (hw : 0 < w_min)
(hWfloor : ∀ i j, i ≠ j → w_min ≤ W i j)
(θ : ℝ → Fin N → ℝ)
(hsol : ∀ t, HasDerivAt θ (kuramotoVectorField K N W (θ t)) t)
(hsemi : ∀ a b : Fin N, |θ 0 a - θ 0 b| < Real.pi) :
Filter.Tendsto (fun t => ‖kuramotoR N (θ t)‖) Filter.atTop (nhds 1)
The mathematics. For the exact ODE shown above, under the five hypotheses in the
panel, the order-parameter norm ‖R‖ tends to 1. Machine-checked in Lean 4
(floor_coupling_convergence_to_synchrony, kuramoto-lean, sorry-free, axiom
footprint {propext, Classical.choice, Quot.sound}).
This page’s numerics. The browser integrator (RK4, finite Δt, floating
point) is a faithful numerical illustration of the theorem, not a machine-checked
simulation.
Real agent fleets. This is a stylized model of multi-agent phase coordination —
not a claim that any deployed system is proven stable.
General coupling. Sign-indefinite weights, coupling without a uniform positive
floor, and initial data outside an open semicircle are open problems — the theorem is
silent there.