Hopfield cyclic-sweep convergence (finite-state argument)

This file uses the tie-handling progress lemma from progress.lean to prove the classical finite-state global dynamics facts for cyclic sweeps:

• No nontrivial cycles for the full-sweep update cycleUpdate (hence convergence).
• A coarse convergence bound of at most 2^n sweeps (and therefore n * 2^n single-coordinate updates) from any initial state, by a pigeonhole argument on the finite state space Bool^n.

We keep the statement at the “sweep level” (one full pass over coordinates). Connecting this to seqStates with cyclicUseq is routine and can be layered on top.

noncomputable def NN.MLTheory.Proofs.Hopfield.f {n : ℕ} (p : Spec.Hopfield.Params ℝ n) : Spec.Hopfield.State n → Spec.Hopfield.State n

The full-sweep update map whose iterates define Hopfield cyclic dynamics.

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_no_nontrivial_cycles {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) {k : ℕ} (hk : 0 < k) (s : Spec.Hopfield.State n) (hcyc : (f p)^[k] s = s) : f p s = s

With symmetric weights and zero diagonal, a periodic orbit of the sweep is a fixed point.

This is the heart of the Hopfield convergence argument: energy never increases along a sweep, so on a cycle it must be constant, and then the active-unit count would have to strictly increase around the cycle and return to its starting value, which is impossible.

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_exists_fixedpoint_le_card {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s0 : Spec.Hopfield.State n) : ∃ m ≤ Fintype.card (Spec.Hopfield.State n), (f p)^[m + 1] s0 = (f p)^[m] s0

A fixed point is reached within Fintype.card (State n) sweeps.

Finitely many states plus no nontrivial cycles gives termination; the bound is the crude pigeonhole one, not a claim about how fast the network actually settles.

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_exists_fixedpoint_le_pow {n : ℕ} (p : Spec.Hopfield.Params ℝ n) (hsym : SymmetricW p) (hdiag : DiagonalZero p) (s0 : Spec.Hopfield.State n) : ∃ m ≤ 2 ^ n, (f p)^[m + 1] s0 = (f p)^[m] s0

The same bound written as 2 ^ n, since a state is one bit per unit.