The mixed-memory hierarchy is not complete

Abstract

An asymmetric five-pattern mixed memory for quadratic activation lies outside the composition hierarchy. Exact correlations on the five-dimensional cube and the strong law yield its limiting overlaps.

Definition 1.1 (Allowable compositions).

$$\forall n:\mathbb{N},\forall c:\mathrm{Composition}\left(n\right),(\mathrm{allowable}\left(c\right))\iff (((\neg c.\mathrm{blocks}=[])\wedge (\forall a:\mathbb{N},(a\in \mathrm{List}.\mathrm{dropLast}\left(c.\mathrm{blocks}\right))\Rightarrow ((2\le a)\wedge (\mathrm{Even}\left(a\right)))))\wedge (\mathrm{Odd}\left(\mathrm{List}.\mathrm{getLastD}\left(c.\mathrm{blocks},0\right)\right)))$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.allowable (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

Printed p. 5: “We call an $\ell$-composition ($n_1$,…,$n_{\ell }$) allowable if $n_k\ge 2$ is even for all $1\le k\le \ell -1$ and $n_{\ell }\ge 1$ is odd.” Mathlib Composition(n) is a list of strictly positive natural blocks summing to n. dropLast removes the last block; getLastD selects it, using zero only for an empty list. Nonemptiness excludes the empty composition. Indices are zero-based.

Definition 1.2 (Products along a composition).

$$\forall n:\mathbb{N},\forall c:\mathrm{Composition}\left(n\right),\forall k:\mathrm{Fin}\left(c.\mathrm{length}\right),\mathrm{gamma}\left(c,k\right)=\mathrm{List}.\mathrm{prod}\left(\mathrm{List}.\mathrm{map}\left(PrecessionSpinOneSeparableBound.c,\mathrm{List}.\mathrm{take}\left(\mathrm{val}\left(k\right)+1,c.\mathrm{blocks}\right)\right)\right)$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.gamma (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

For every positive block size a, PrecessionSpinOneSeparableBound.c(a) is the source’s α^(a) = 2^(-a+1) binom(a-1,floor((a-1)/2)), reused from D5.S3.Quantum.Entanglement.PrecessionSpinOneSeparableBound; the source’s (1.2.1.5), printed (1.10), p. 5, defines gamma(k) as the product of these factors in the first k blocks. Fin indices begin at zero, so gamma(c,k) takes k.val+1 blocks.

Definition 1.3 (The strict hierarchy inequalities).

$$\forall n:\mathbb{N},\forall F:(\mathbb{R})\to (\mathbb{R}),\forall c:\mathrm{Composition}\left(n\right),(\mathrm{hierarchySystem}\left(F,c\right))\iff (\forall k:\mathrm{Fin}\left(c.\mathrm{length}\right),(\mathrm{val}\left(k\right)+1<c.\mathrm{length})\Rightarrow (2\cdot \mathrm{deriv}\left(F,\mathrm{gamma}\left(c,k\right)\right)>\sum _{r:\mathrm{Fin}\left(c.\mathrm{length}\right)}\mathrm{if}(k<r)\mathrm{then}(c.\mathrm{blocksFun}\left(r\right):\mathbb{R})\cdot \mathrm{deriv}\left(F,\mathrm{gamma}\left(c,r\right)\right)\mathrm{else}0))$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.hierarchySystem (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

The source’s system S, (1.2.1.12bis), printed (1.13), p. 5: for each nonfinal block, twice the derivative at its gamma value exceeds the sum of all later block lengths times the derivatives at their gamma values. The last block imposes no inequality.

Definition 1.4 (The padded block vector).

$$\forall n:\mathbb{N},\forall c:\mathrm{Composition}\left(n\right),\forall mu:\mathbb{N},\mathrm{blockVector}\left(c,mu\right)=\mathrm{if}h:mu<n\mathrm{then}\mathrm{gamma}\left(c,c.\mathrm{index}\left(\mathrm{Fin}.\mathrm{mk}\left(mu,h\right)\right)\right)\mathrm{else}0$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.blockVector (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

Printed p. 5: “Given ${\gamma }_n\in {\mathcal{G}}_{n,F}$, let $m({\gamma }_n)=(m_{\mu }({\gamma }_n){)}_{1\le \mu \le M}$ be the vector whose components are constant and equal to ${\gamma }^{(k)}$ on consecutive blocks of length $n_k$, $1\le k\le \ell$, and are $0$ beyond,” as displayed in (1.2.1.8), printed (1.14). Composition.index selects the unique block containing the zero-based coordinate mu; the dependent Fin constructor contains its bound proof h.

Definition 1.5 (The literal coefficient set).

$$\forall n:\mathbb{N},\forall F:(\mathbb{R})\to (\mathbb{R}),\forall M:\mathbb{N},\forall m:(\mathrm{Fin}\left(M\right))\to (\mathbb{R}),(m\in \mathrm{coefficientSet}\left(n,F,M\right))\iff (\exists c:\mathrm{Composition}\left(n\right),((\mathrm{allowable}\left(c\right))\wedge (\mathrm{hierarchySystem}\left(F,c\right)))\wedge (\exists pi:\mathrm{Equiv}.\mathrm{Perm}\left(\mathrm{Fin}\left(M\right)\right),\exists eps:(\mathrm{Fin}\left(M\right))\to (\mathbb{R}),(\forall mu:\mathrm{Fin}\left(M\right),(eps\left(mu\right)=-1)\vee (eps\left(mu\right)=1))\wedge (\forall mu:\mathrm{Fin}\left(M\right),m\left(mu\right)=eps{\left(mu\right)}^{\mathrm{if}(\forall x:\mathbb{R},\mathrm{deriv}\left(F,-x\right)=-\mathrm{deriv}\left(F,x\right))\mathrm{then}1\mathrm{else}2}\cdot \mathrm{blockVector}\left(c,\mathrm{val}\left(pi\left(mu\right)\right)\right))))$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.coefficientSet (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

The source’s (1.2.1.15), printed (1.15), p. 6, takes all allowable compositions satisfying S, all permutations of the M coordinates, and all coordinate signs. The sign exponent is 1 if the derivative is odd and 2 otherwise. Here coefficientSet(n,F,M) is a Set of functions Fin(M) → R.

Definition 1.6 (The mixed configuration).

$$\forall Omega:\mathrm{Type},\forall F:(\mathbb{R})\to (\mathbb{R}),\forall M:(\mathbb{N})\to (\mathbb{N}),\forall m:(\mathbb{N})\to (\mathbb{R}),\forall xi:(\mathbb{N})\to ((\mathbb{N})\to ((Omega)\to (\mathbb{R}))),\forall N:\mathbb{N},\forall i:\mathbb{N},\forall omega:Omega,\mathrm{memorySpin}\left(F,M,m,xi,N,i,omega\right)=\mathrm{Real}.\mathrm{sign}\left(\sum _{mu\in \mathrm{Finset}.\mathrm{range}\left(M\left(N\right)\right)}xi\left(mu,i,omega\right)\cdot \mathrm{deriv}\left(F,m\left(mu\right)\right)\cdot \mathrm{if}(\neg m\left(mu\right)=0)\mathrm{then}1\mathrm{else}0\right)$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.memorySpin (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

Definition 1.1, p. 4, defines xi_i(m) = sign(sum_mu xi_i^mu F’(m_mu) 1_{m_mu ≠ 0}). The pattern and site indices are shifted by one: Lean mu and i correspond to source mu+1 and i+1. The source’s sign convention (2.2.2), printed (2.25), p. 15, is +1 above zero, -1 below zero, and 0 at zero; Real.sign has precisely this convention. M(N) permits the number of patterns to vary with N.

Definition 1.7 (Mixed memories of type F).

$$\forall Omega:\mathrm{Type},[\mathrm{MeasurableSpace}\left(Omega\right)]\forall P:\mathrm{Measure}\left(Omega\right),\forall n:\mathbb{N},\forall F:(\mathbb{R})\to (\mathbb{R}),\forall M:(\mathbb{N})\to (\mathbb{N}),\forall m:(\mathbb{N})\to (\mathbb{R}),\forall xi:(\mathbb{N})\to ((\mathbb{N})\to ((Omega)\to (\mathbb{R}))),(\mathrm{mixedMemory}\left(P,n,F,M,m,xi\right))\iff ((\forall N:\mathbb{N},\forall i:\mathbb{N},(i<N)\Rightarrow (\mathrm{Filter}.\mathrm{Eventually}\left((omega:Omega\mapsto (\mathrm{memorySpin}\left(F,M,m,xi,N,i,omega\right)=-1)\vee (\mathrm{memorySpin}\left(F,M,m,xi,N,i,omega\right)=1)),\mathrm{ae}\left(P\right)\right)))\wedge (\exists V:\mathrm{Finset}\left(\mathbb{N}\right),(((V.\mathrm{card}=n)\wedge (\forall N:\mathbb{N},(V\subseteq \mathrm{Finset}.\mathrm{range}\left(M\left(N\right)\right))\wedge (\forall mu:\mathbb{N},(mu\in \mathrm{Finset}.\mathrm{range}\left(M\left(N\right)\right))\Rightarrow ((\neg m\left(mu\right)=0)\iff (mu\in V)))))\wedge (\forall mu:\mathbb{N},(mu\in V)\Rightarrow (\mathrm{Filter}.\mathrm{Eventually}\left((omega:Omega\mapsto \mathrm{Tendsto}\left((N:\mathbb{N}\mapsto (N:\mathbb{R}{)}^{-1}\cdot \sum _{i\in \mathrm{Finset}.\mathrm{range}\left(N\right)}xi\left(mu,i,omega\right)\cdot \mathrm{memorySpin}\left(F,M,m,xi,N,i,omega\right)),\mathrm{atTop},\mathrm{nhds}\left(m\left(mu\right)\right)\right)),\mathrm{ae}\left(P\right)\right))))\wedge (\forall mu:\mathbb{N},(\exists N:\mathbb{N},mu<M\left(N\right))\Rightarrow ((\neg mu\in V)\Rightarrow (\mathrm{Filter}.\mathrm{Eventually}\left((omega:Omega\mapsto \mathrm{Tendsto}\left((N:\mathbb{N}\mapsto (N:\mathbb{R}{)}^{-1}\cdot \sum _{i\in \mathrm{Finset}.\mathrm{range}\left(N\right)}xi\left(mu,i,omega\right)\cdot \mathrm{memorySpin}\left(F,M,m,xi,N,i,omega\right)),\mathrm{atTop},\mathrm{nhds}\left(0\right)\right)),\mathrm{ae}\left(P\right)\right))))))$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.mixedMemory (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

Definition 1.1, p. 4: “Let $F$ be a smooth function whose derivative satisfies $F^{\prime }(x)>0$, for all $x>0$. Given $n\in \mathbb{N}$ independent of $N$, $n$-mixed memories of type $F$ are configurations in ${\mathcal{S}}_N$ denoted by ${\xi }^{(N)}(m)=({\xi }_i(m){)}_{1\le i\le N}$ and defined as” the displayed spin formula. “(i) $m$ has exactly $n$ non-zero components, i.e. there exists a subset $V$⊂{1,…,M} of cardinality $|V|=n$ such that $m_{\mu }\ne 0$ if and only if $\mu \in V$.” “Let {μ₁,…,μₙ} be an enumeration of the elements of $V$ and, for each $1\le \nu \le n$, set $m_{{\mu }_{\nu }}={\hat{m}}_{\nu }$. Then, for each $1\le \nu \le n$, the normalised overlap of ${\xi }^{(N)}(m)$ with the pattern ${\xi }^{{\mu }_{\nu }}$ converges to ${\hat{m}}_{\nu }$ as $N$ diverges,” and “and it converges to zero else,” with probability one in (1.2.1.2) and (1.2.1.3). The formula records that configurations are binary almost surely. Each occupied coordinate converges to its coefficient; every coordinate appearing at some size and outside V converges to zero. The support V is independent of N. The hypotheses on F, n, M and the coordinate bounds are bound in claim.

Definition 1.8 (Gayrard’s Conjecture 1.4).

$$(claim)\iff (\forall Omega:\mathrm{Type},[\mathrm{MeasurableSpace}\left(Omega\right)]\forall P:\mathrm{Measure}\left(Omega\right),[\mathrm{IsProbabilityMeasure}\left(P\right)]\forall xi:(\mathbb{N})\to ((\mathbb{N})\to ((Omega)\to (\mathbb{R}))),(\forall mu:\mathbb{N},\forall i:\mathbb{N},\mathrm{Measurable}\left(xi\left(mu,i\right)\right))\Rightarrow ((\mathrm{iIndepFun}\left((pair:\mathbb{N}\times \mathbb{N}\mapsto xi\left(pair.\mathrm{fst},pair.\mathrm{snd}\right)),P\right))\Rightarrow ((\forall mu:\mathbb{N},\forall i:\mathbb{N},(P\left(\{omega:Omega\mid xi\left(mu,i,omega\right)=1\}\right)=\frac{1}{2})\wedge (P\left(\{omega:Omega\mid xi\left(mu,i,omega\right)=-1\}\right)=\frac{1}{2}))\Rightarrow (\forall F:(\mathbb{R})\to (\mathbb{R}),(\mathrm{ContDiff}\left(\mathbb{R},\mathrm{Top}.\mathrm{top},F\right))\Rightarrow ((\forall x:\mathbb{R},(0<x)\Rightarrow (0<\mathrm{deriv}\left(F,x\right)))\Rightarrow (\forall n:\mathbb{N},(\mathrm{Odd}\left(n\right))\Rightarrow (\forall M:(\mathbb{N})\to (\mathbb{N}),(\mathrm{Monotone}\left(M\right))\Rightarrow (\forall m:(\mathbb{N})\to (\mathbb{R}),(\forall mu:\mathbb{N},(-1\le m\left(mu\right))\wedge (m\left(mu\right)\le 1))\Rightarrow ((\mathrm{mixedMemory}\left(P,n,F,M,m,xi\right))\iff (\forall N:\mathbb{N},(mu:\mathrm{Fin}\left(M\left(N\right)\right)\mapsto m\left(\mathrm{val}\left(mu\right)\right))\in \mathrm{coefficientSet}\left(n,F,M\left(N\right)\right)))))))))))$$

Formalization. D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.claim (✓ std3).

Citation. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

Conjecture 1.4, printed p. 6: “Given any $n\in \mathbb{N}$ odd, ${\xi }^{(N)}(m)$ is an $n$-mixed memory of type $F$ if and only if $m\in {\mathcal{M}}_{n,F}$.” The standing sentence on p. 4 is: “Throughout the paper, $n\in \mathbb{N}$ is chosen to be independent of $N$ and $M$ is chosen to be a non-decreasing function of $N$.” An infinite deterministic sequence m represents coherent restrictions to the first M(N) coordinates. Membership is checked on each restriction. The probability space and jointly independent measurable family xi are arbitrary; both signs have mass 1/2. F is smooth with positive derivative on the positive half-line, n is odd, M is monotone, and every coefficient lies in [-1,1]. The two bracketed Lean instance arguments are anonymous.

Theorem 1.9 (An asymmetric five-pattern counterexample).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.result (✓ std3). ∎

Resolves. Problems/gayrard-2025-mixed-memory-converse-refutation (refuted) by D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.result.

Source. Repository-derived.

Acknowledgement. Véronique Gayrard (2025). Mixed memories in Hopfield networks. URL: https://arxiv.org/abs/2504.04879v2.

Commentary.

For F(x)=x²/2 and M(N)=5, take m=(5/8,3/8,3/8,1/8,1/8), padded by zeros. The integer fields 5x₁+3x₂+3x₃+x₄+x₅ never vanish. Summing each coordinate times their sign over all 32 cube points gives (20,12,12,4,4). An infinite product of fair Boolean coordinates supplies the independent patterns; the strong law yields the five normalized overlap limits. There are no unused coordinates among the first five. The allowable compositions of five are (5), (2,3), (4,1), (2,2,1), and every padded block coordinate has absolute value at most 1/2. Permutations and the prescribed sign powers preserve this bound, while m₁=5/8. Theorem 1.2’s sufficient direction is compatible with this failure of necessity. No local-minimum assertion is made.

References

• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.allowable
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.blockVector
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.claim
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.coefficientSet
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.gamma
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.hierarchySystem
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.memorySpin
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.mixedMemory
• Truth anchor: D5/S3/StatisticalMechanics/Hopfield/GayrardMixedMemoryRefutation.result
• Dependency: D5/S3/Combinatorics/IsingUniquenessSets
• Dependency: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound