Hopfield networks (spec-level)

This file gives a Hopfield network model as a set of explicit mathematical definitions.

• A state is a Boolean vector Fin n → Bool (activation true ↦ +1, false ↦ -1).
• Parameters are a weight matrix W : Fin n → Fin n → α and thresholds θ : Fin n → α.
• An asynchronous update picks a neuron u and updates only that coordinate.

Intended use: mathematical scalars (ℚ, ℝ, etc.) and theorem statements/proofs. For computation, instantiate α := ℚ (or Rat) and evaluate seqStates / energy via #eval in an example file.

Note: we also provide Tensor-shaped wrappers (StateT, ParamsT) so users can work with Tensor _ (.dim n .scalar) instead of raw Fin n → _.

References

• Hopfield (1982), "Neural networks and physical systems with emergent collective computational abilities": https://www.pnas.org/doi/10.1073/pnas.79.8.2554 ("Neurons with graded response have collective computational properties " ++ "like those of two-state neurons"): https://www.pnas.org/doi/10.1073/pnas.81.10.3088
• Ramsauer et al. (2020), "Hopfield Networks is All You Need": https://arxiv.org/abs/2008.02217

Relationship to the Hopfield formalization case study

This file provides the definitions (update rule, energy, trajectories). The global-dynamics results (energy monotonicity, fixed-point convergence bounds, tie-handling lemmas, etc.) are proved in NN/MLTheory/Proofs/Hopfield/* against these definitions.

If you’re reading this alongside “Formalized Hopfield Networks and Boltzmann Machines” (2025), the correspondence is:

• updateAt / seqStates formalize the asynchronous update dynamics,
• energy is the Lyapunov/energy functional used for convergence arguments,
• theorems in NN.MLTheory.Proofs.Hopfield.Energy and NN.MLTheory.Proofs.Hopfield.Convergence capture the classic “energy decreases ⇒ convergence” theorem pattern for finite state spaces.

Core data

def Spec.Hopfield.act {α : Type} [One α] [Neg α] : Bool → α

Boolean activations interpreted as ±1.

We intentionally store Hopfield states as Bool (instead of α) because many proofs are simpler when the only possible activations are +1 and -1. The embedding into a numeric scalar α is explicit via act.

@[simp]

theorem Spec.Hopfield.act_true {α : Type} [One α] [Neg α] : act true = 1

@[simp]

theorem Spec.Hopfield.act_false {α : Type} [One α] [Neg α] : act false = -1

@[reducible, inline]

abbrev Spec.Hopfield.State (n : ℕ) : Type

Hopfield state as a Boolean activation vector.

@[reducible, inline]

abbrev Spec.Hopfield.StateT (n : ℕ) : Type

Hopfield state as a vector tensor Tensor Bool (.dim n .scalar).

This is a convenience wrapper so Hopfield models can interoperate with the rest of TorchLean's tensor-shaped spec APIs.

def Spec.Hopfield.StateT.toFun {n : ℕ} (s : StateT n) : State n

Convert a tensor state to the underlying function representation.

def Spec.Hopfield.StateT.ofFun {n : ℕ} (s : State n) : StateT n

Convert a function state to a tensor state.

@[simp]

theorem Spec.Hopfield.StateT.toFun_ofFun {n : ℕ} (s : State n) : (ofFun s).toFun = s

@[simp]

theorem Spec.Hopfield.StateT.ofFun_toFun {n : ℕ} (s : StateT n) : ofFun s.toFun = s

def Spec.Hopfield.actVec {α : Type} [One α] [Neg α] {n : ℕ} (s : State n) : Fin n → α

The ±1 activation vector associated to a Boolean state.

def Spec.Hopfield.dot {α : Type} [AddCommMonoid α] [Mul α] {n : ℕ} (x y : Fin n → α) : α

Dot product on vectors indexed by Fin n.

We define this directly as a Fin-indexed sum. This keeps the model independent from any concrete matrix representation.

def Spec.Hopfield.mulVec {α : Type} [AddCommMonoid α] [Mul α] {n : ℕ} (W : Fin n → Fin n → α) (x : Fin n → α) : Fin n → α

Matrix-vector product (as a function, not an array-backed matrix).

structure Spec.Hopfield.Params (α : Type) (n : ℕ) : Type

Hopfield parameters:

• W is the weight matrix
• θ is the per-unit threshold / bias

Classic convergence results typically assume W is symmetric and has a zero diagonal. Those assumptions are not baked into this structure; they are stated and proved where needed.

• W : Fin n → Fin n → α

  W.

• θ : Fin n → α

structure Spec.Hopfield.ParamsT (α : Type) (n : ℕ) : Type

Hopfield parameters as tensor-shaped weights and thresholds.

• W : Tensor α (Shape.dim n (Shape.dim n Shape.scalar))

  W.

• θ : Tensor α (Shape.dim n Shape.scalar)

def Spec.Hopfield.ParamsT.toFun {α : Type} {n : ℕ} (p : ParamsT α n) : Params α n

Convert tensor-shaped parameters to the function representation.

Hopfield update dynamics

def Spec.Hopfield.net {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] {n : ℕ} (p : Params α n) (s : State n) (u : Fin n) : α

Net input to unit u: (W * x)_u, where x = actVec s is the ±1 encoding of the state.

def Spec.Hopfield.netT {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] {n : ℕ} (p : ParamsT α n) (s : StateT n) (u : Fin n) : α

Tensor-shaped wrapper for net (useful for interop with TorchLean tensor APIs).

def Spec.Hopfield.updateAt {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (s : State n) (u : Fin n) : State n

Asynchronous update at a single coordinate u.

We implement the standard thresholded sign rule:

s[u] := (θ_u ≤ net_u)

Interpreting true ↦ +1 and false ↦ -1, this corresponds to:

x_u := +1 if net_u ≥ θ_u, otherwise x_u := -1.

Tie-handling (net_u = θ_u) matters for formal convergence arguments; we pick the convention "ties go to +1" via ≤.

def Spec.Hopfield.updateAtT {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : ParamsT α n) (s : StateT n) (u : Fin n) : StateT n

Tensor-shaped wrapper for updateAt.

def Spec.Hopfield.IsStable {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (s : State n) : Prop

A state is stable (a fixed point) if updating any single coordinate does nothing.

def Spec.Hopfield.pluses {n : ℕ} (s : State n) : ℕ

Count how many units are in the true (+1) state.

Hopfield energy

def Spec.Hopfield.energy {α : Type} [Field α] {n : ℕ} (p : Params α n) (s : State n) : α

The classical Hopfield energy for a state s (quadratic term + linear threshold term).

With x = actVec s the ±1 encoding, the energy is:

E(s) = -1/2 * Σ_i Σ_j W_ij x_i x_j + Σ_i θ_i x_i.

When W is symmetric and has a zero diagonal, asynchronous updates are known to monotonically decrease (or not increase) E, which is the classic Lyapunov-style argument for convergence.

def Spec.Hopfield.energyT {α : Type} [Field α] {n : ℕ} (p : ParamsT α n) (s : StateT n) : α

Tensor-shaped wrapper for energy.

def Spec.Hopfield.seqStates {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (useq : ℕ → Fin n) (s0 : State n) : ℕ → State n

State sequence induced by an asynchronous update schedule useq.

useq : Nat → Fin n picks which coordinate to update at each discrete time step.

PyTorch analogy: there is no direct equivalent in typical NN libraries, but you can think of it as an explicit, deterministic "update schedule" for coordinate descent.

def Spec.Hopfield.seqStatesT {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : ParamsT α n) (useq : ℕ → Fin n) (s0 : StateT n) : ℕ → StateT n

Tensor-shaped wrapper for seqStates.

def Spec.Hopfield.cyclicUseq (n : ℕ) (hn : 0 < n) : ℕ → Fin n

A cyclic update schedule (0,1,2,...,n-1,0,1,...) for n > 0.

Executable Hopfield (backend-friendly)

The definitions above (net, energy, …) are written in a math-first style using ∑ over Fin n. That is the right presentation for proofs, but it bakes in algebraic typeclasses like AddCommMonoid and uses Finset sums.

When we execute Hopfield over IEEE-like scalars (e.g. Float, IEEE32Exec), we do not want to pretend those algebraic laws hold exactly: NaNs and rounding make addition non-associative and non-commutative in general. So for runtime execution we provide a “plain loop” variant that:

• requires only the operations from [Context α],
• uses explicit List.foldl iteration over Fin n.

This is the same model, just written in a way that stays honest about runtime arithmetic.

References:

• IEEE 754-2019 (why NaNs/rounding break algebraic laws): https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991), classic floating-point background: https://doi.org/10.1145/103162.103163

@[inline]

def Spec.Hopfield.Exec.act {α : Type} [Context α] : Bool → α

@[inline]

def Spec.Hopfield.Exec.theta {α : Type} {n : ℕ} (p : ParamsT α n) (i : Fin n) : α

@[inline]

def Spec.Hopfield.Exec.weight {α : Type} {n : ℕ} (p : ParamsT α n) (i j : Fin n) : α

def Spec.Hopfield.Exec.net {α : Type} [Context α] {n : ℕ} (p : ParamsT α n) (s : StateT n) (u : Fin n) : α

Net input to unit u computed by explicit iteration.

This matches Hopfield.netT, but avoids Finset sums so it can execute over IEEE-like scalars.

def Spec.Hopfield.Exec.updateAt {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : ParamsT α n) (s : StateT n) (u : Fin n) : StateT n

Asynchronous update of a single coordinate u, using the same “ties go to +1” convention as the spec definition (θ_u ≤ net_u).

def Spec.Hopfield.Exec.seqStates {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : ParamsT α n) (useq : ℕ → Fin n) (s0 : StateT n) : ℕ → StateT n

State sequence induced by an update schedule useq : Nat → Fin n (loop-based).

def Spec.Hopfield.Exec.energy {α : Type} [Context α] {n : ℕ} (p : ParamsT α n) (s : StateT n) : α

Hopfield energy computed by explicit iteration.

This matches the standard formula: E(s) = -1/2 * Σ_i Σ_j W_ij x_i x_j + Σ_i θ_i x_i, with x_i ∈ {+1,-1} obtained from the Boolean state.