Hopfield: basic lemmas

This file contains small, reusable lemmas about the spec-level Hopfield definitions.

The “paper theorems” (energy monotonicity, convergence, Hebbian stability) should live in separate files once proved.

@[simp]

theorem NN.MLTheory.Proofs.Hopfield.updateAt_apply_eq_update {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) (u : Fin n) : Spec.Hopfield.updateAt p s u = Function.update s u (decide (p.θ u ≤ Spec.Hopfield.net p s u))

One asynchronous update is a Function.update at the chosen unit, with the threshold test as the new value. Stating it this way lets the Mathlib Function.update lemmas do the bookkeeping.

@[simp]

theorem NN.MLTheory.Proofs.Hopfield.updateAt_apply_self {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) (u : Fin n) : Spec.Hopfield.updateAt p s u u = decide (p.θ u ≤ Spec.Hopfield.net p s u)

At the updated unit, the new state is the threshold test.

@[simp]

theorem NN.MLTheory.Proofs.Hopfield.updateAt_apply_ne {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) {u v : Fin n} (h : v ≠ u) : Spec.Hopfield.updateAt p s u v = s v

Every other unit is untouched, which is what makes the update asynchronous.

theorem NN.MLTheory.Proofs.Hopfield.pluses_updateAt_eq_succ_of_set_true {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) (u : Fin n) (hsu : s u = false) (hdec : decide (p.θ u ≤ Spec.Hopfield.net p s u) = true) : Spec.Hopfield.pluses (Spec.Hopfield.updateAt p s u) = Spec.Hopfield.pluses s + 1

Flipping a unit from false to true raises the count of active units by one.

The active count is the tie-breaking measure in the convergence proof: when the energy stays flat, a real state change still has to move this counter, and it cannot rise forever.

theorem NN.MLTheory.Proofs.Hopfield.pluses_updateAt_eq_pred_of_set_false {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) (u : Fin n) (hsu : s u = true) (hdec : decide (p.θ u ≤ Spec.Hopfield.net p s u) = false) : Spec.Hopfield.pluses (Spec.Hopfield.updateAt p s u) + 1 = Spec.Hopfield.pluses s

Flipping a unit from true to false lowers the active count by one.