Kuramoto-lean: Lean 4 Library for Finite-N Kuramoto Synchronisation Dynamics

kuramoto-lean is a Lean 4 / Mathlib library for finite-N Kuramoto oscillatordynamics, taking a finite-dimensional geometric approach distinct fromOtt-Antonsen / continuum-limit formalisms. It contains 39 public theoremdeclarations, all machine-checked sorry-free, admit-free, and with noproject-defined axioms; committed #print axioms transcript guards for theheadline frontier and discrete results record the footprint{propext, Classical.choice, Quot.sound}. Nine theorems form the algebraic core(order-parameter boundedness, gradient and Lyapunov-descent identities,contraction sign facts, Hebbian phase-plus-weight descent); fourteen frontiertheorems add ODE existence and uniqueness via Picard-Lindelof, Lyapunovstability along trajectories, and convergence to synchrony from anyopen-semicircle initial condition, first for all-to-all coupling and then forany symmetric coupling with a uniform positive off-diagonal floor; and sixteendiscrete theorems establish fixed-step skew confinement, a stochastic-matrixreformulation, geometric contraction, and convergence of the skew to zero. Thecontinuous convergence theorems are precisely scoped by their hypotheses, andthe discrete convergence theorem additionally requires at least threeoscillators and a positive step size; none is a general Kuramotosynchronisation result. The repository is the formal proof spine for thecompanion flywheel-universe project on budgeted Hebbian Kuramoto dynamics forMax-Cut.