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

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

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

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