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
plusesstrictly increases.
noncomputable def
NN.MLTheory.Proofs.Hopfield.cycleUpdate
{n : ℕ}
(p : Spec.Hopfield.Params ℝ n)
(s : Spec.Hopfield.State n)
:
Instances For
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)
:
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