How are diamond identities implied in congruence varieties? (Q1802262)

For \(n\geq 2\), an \((n+1)\)-tuple \(\vec a= (a_ 1,\dots,a_{n+1})\) of elements in a modular lattice \(L\) is called an \(n\)-diamond (after A. P. Huhn and C. Herrmann) if \(\sum^{0,n}_{i\neq k} a_ i=\sum^{0,n}_ i a_ i\) and \(a_ \ell\sum^{0,n}_{i\neq k,\ell} a_ i= \prod^{0,n}_ i a_ i\), for all \(k\neq\ell\). Let \(\lambda: p(x_ 1,\dots,x_ t)= q(x_ 1,\dots,x_ t)\) be a lattice identity. \(\lambda\) is called a diamond identity if \(\lambda\) implies modularity and, in addition, there are \((n+1)\)-ary lattice terms \(c_ 1(y_ 0,\dots,y_ n),\dots,c_ t(y_ 0,\dots,y_ n)\) for some \(n\geq 2\) such that for an arbitrary modular lattice \(L\) if \(p(c_ 1(\vec a),\dots,c_ n(\vec a))= q(c_ 1(\vec a),\dots,c_ n(\vec a))\) for every \(n\)-diamond \(\vec a\) in \(L\) then \(\lambda\) holds in \(L\). The distributive law is the simplest example. Given a set \(\Gamma\) of lattice identities, let \(\Gamma\models_ c\lambda\) denote that \(\lambda\) holds in every congruence variety satisfying \(\Gamma\). Suppose \(\lambda\) is a diamond identity. An algorithm is given to test whether \(\Gamma\models_ c\lambda\). It is shown that \(\Gamma\models_ c\lambda\) implies the existence of a finite subset \(\Delta\) of \(\Gamma\) such that \(\Delta\models_ c\lambda\).