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 ExecFloat.Binary 8 23; 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 → ℝ

Bipolar activation vector of a state, ±1 per unit.

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

The index set of all units, named so the sums below read like the paper.

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

Net input at u, written as a function of the activation vector rather than the Boolean state.

The energy computations are all linear algebra over ℝ, so working with x instead of s keeps Function.update and Finset.sum lemmas applicable throughout.

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

The quadratic form ∑ᵢⱼ Wᵢⱼ xᵢ xⱼ.

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

Energy as a function of the activation vector: -½ xᵀWx + θᵀx.

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)

The state-level energy and the vector-level one agree.

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

Likewise for the net input.

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)))

An update of the state becomes a Function.update of the activation vector.

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)

Changing coordinate u shifts the net input at u only through the self-weight W u u, which the zero-diagonal hypothesis later kills.

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)

Contribution of a single row i ≠ u to the change in the quadratic form.

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

Change in the quadratic form under a single-unit update: 2 (x'ᵤ - xᵤ) · netᵤ.

Symmetry is what merges the row and column contributions into a single factor of two, and the zero diagonal is what removes the term where the unit acts on itself. Without either hypothesis the energy can increase and the network need not converge.

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

A single asynchronous update never increases the energy.

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)

Exact energy change of one update: -(x'ᵤ - xᵤ)(netᵤ - θᵤ).

The sign is forced: the update sets x'ᵤ to agree with the sign of netᵤ - θᵤ, so the product is nonnegative and the energy change is nonpositive. Everything else in this file is a corollary.

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

Exactly at the threshold the energy does not move, which is the flat case the active-unit counter has to handle.

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

Away from the threshold, a state change strictly lowers the energy.