Hopfield energy: single-step dynamics (spec layer)

This file proves the key “global dynamics” lemma from the Hopfield literature:

Under symmetric, zero-diagonal weights, the Hopfield energy is non-increasing under an asynchronous update.

We work over ℝ, where the classical energy argument is algebraic. The executable Hopfield implementation uses IEEE32Exec; floating-point executions are connected to this theorem only through explicit runtime/rounding bridge statements, not by silently reusing real arithmetic laws.

def NN.MLTheory.Proofs.Hopfield.SymmetricW {n : ℕ} (p : Spec.Hopfield.Params ℝ n) : Prop

Symmetry condition on Hopfield weights: W i j = W j i.

def NN.MLTheory.Proofs.Hopfield.DiagonalZero {n : ℕ} (p : Spec.Hopfield.Params ℝ n) : Prop

Zero-diagonal condition on Hopfield weights: W i i = 0.

noncomputable def NN.MLTheory.Proofs.Hopfield.x {n : ℕ} (s : Spec.Hopfield.State n) : Fin n → ℝ

noncomputable def NN.MLTheory.Proofs.Hopfield.U {n : ℕ} : Finset (Fin n)

noncomputable def NN.MLTheory.Proofs.Hopfield.netx {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (x : Fin n → ℝ) (u : Fin n) : ℝ

noncomputable def NN.MLTheory.Proofs.Hopfield.quad {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (x : Fin n → ℝ) : ℝ

noncomputable def NN.MLTheory.Proofs.Hopfield.energyU {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (x : Fin n → ℝ) : ℝ

theorem NN.MLTheory.Proofs.Hopfield.energy_eq_energyU {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (s : Spec.Hopfield.State n) : Spec.Hopfield.energy p s = energyU p (x s)

theorem NN.MLTheory.Proofs.Hopfield.net_eq_netx {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (s : Spec.Hopfield.State n) (u : Fin n) : Spec.Hopfield.net p s u = netx p (x s) u

theorem NN.MLTheory.Proofs.Hopfield.x_updateAt_eq_update {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (s : Spec.Hopfield.State n) (u : Fin n) : x (Spec.Hopfield.updateAt p s u) = Function.update (x s) u (Spec.Hopfield.act (decide (p.θ u ≤ Spec.Hopfield.net p s u)))

theorem NN.MLTheory.Proofs.Hopfield.netx_update_eq {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (x0 : Fin n → ℝ) (u : Fin n) (xu' : ℝ) : netx p (Function.update x0 u xu') u = netx p x0 u + p.W u u * (xu' - x0 u)

theorem NN.MLTheory.Proofs.Hopfield.quad_inner_delta_ne {n : ℕ} (p : Spec.Hopfield.Params ℝ n) {u i : Fin n} (hi : i ≠ u) (x0 : Fin n → ℝ) (xu' : ℝ) : ∑ j ∈ U, p.W i j * x0 i * Function.update x0 u xu' j - ∑ j ∈ U, p.W i j * x0 i * x0 j = p.W i u * x0 i * (xu' - x0 u)

theorem NN.MLTheory.Proofs.Hopfield.quad_delta_update {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (x0 : Fin n → ℝ) (u : Fin n) (xu' : ℝ) : quad p (Function.update x0 u xu') - quad p x0 = 2 * (xu' - x0 u) * netx p x0 u

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

theorem NN.MLTheory.Proofs.Hopfield.energy_updateAt_delta {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s : Spec.Hopfield.State n) (u : Fin n) : have x0 := x s; have xu' := Spec.Hopfield.act (decide (p.θ u ≤ Spec.Hopfield.net p s u)); Spec.Hopfield.energy p (Spec.Hopfield.updateAt p s u) - Spec.Hopfield.energy p s = -(xu' - x0 u) * (Spec.Hopfield.net p s u - p.θ u)

theorem NN.MLTheory.Proofs.Hopfield.energy_updateAt_eq_of_net_eq_theta {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s : Spec.Hopfield.State n) (u : Fin n) (hnet : Spec.Hopfield.net p s u = p.θ u) : Spec.Hopfield.energy p (Spec.Hopfield.updateAt p s u) = Spec.Hopfield.energy p s

theorem NN.MLTheory.Proofs.Hopfield.energy_updateAt_lt_of_change_of_ne {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s : Spec.Hopfield.State n) (u : Fin n) (hchange : Spec.Hopfield.updateAt p s u ≠ s) (hne : Spec.Hopfield.net p s u ≠ p.θ u) : Spec.Hopfield.energy p (Spec.Hopfield.updateAt p s u) < Spec.Hopfield.energy p s