Hopfield cyclic sweep progress (tie-handling)

This file proves the key “tie-handling” lemma needed for paper-style Hopfield global-dynamics claims under the update convention s[u] := (θ[u] ≤ net[u]) (“ties go to +1”).

Energy is non-increasing under each coordinate update, but in the tie case net = θ the energy can stay constant while the state changes. We show that in this tie case, the number of +1s (pluses) strictly increases. This yields a lexicographic progress measure.

We package the statement for a full cyclic sweep over coordinates:

• Either energy strictly decreases, or energy is unchanged and pluses strictly increases.

noncomputable def NN.MLTheory.Proofs.Hopfield.cycleUpdate {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (s : Spec.Hopfield.State n) : Spec.Hopfield.State n

One full cyclic sweep of coordinate updates over Fin n.

theorem NN.MLTheory.Proofs.Hopfield.energy_cycleUpdate_le {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s : Spec.Hopfield.State n) : Spec.Hopfield.energy p (cycleUpdate p s) ≤ Spec.Hopfield.energy p s

A full sweep over all units never increases the energy, by composing the single-unit bound.

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_progress {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s : Spec.Hopfield.State n) (hchange : cycleUpdate p s ≠ s) : Spec.Hopfield.energy p (cycleUpdate p s) < Spec.Hopfield.energy p s ∨ Spec.Hopfield.energy p (cycleUpdate p s) = Spec.Hopfield.energy p s ∧ Spec.Hopfield.pluses (cycleUpdate p s) > Spec.Hopfield.pluses s

Every sweep that changes the state makes progress: either the energy strictly drops, or it stays equal and the number of active units strictly rises.

This lexicographic measure is what Convergence.lean turns into termination. Energy alone is not enough, because a unit sitting exactly at its threshold can flip without changing the energy.