Lemma. A shifted product rule [fdip-0009]

Let \(R\) be a commutative unital ring and let \(n\ge 1\). On \(\mathcal F_R(\mathbb Z/n\mathbb Z)\), let \(T\) and \(\Delta \) be the cyclic shift and forward difference.

For \(f,g\) in that module, \[\Delta (fg)=(\Delta f)(Tg)+f\Delta g.\] Equivalently, \[\Delta (fg)=(\Delta f)g+f\Delta g+(\Delta f)(\Delta g).\] Wingate defines forward and backward differences with lattice spacing \(a\) in [wingate2025lattice, Section 4, Equations (4.2)-(4.3), p. 3]. Here \(a=1\); the ring-valued finite identities are direct calculations, with no continuum approximation.

At \(n=1\), the cycle has a loop and \(T=I\), \(\Delta =0\). At \(n=2\), its two edges have opposite orientations between the same vertices; it is not a single simple edge. The unshifted Leibniz rule fails by the correction \(\,(\Delta f)(\Delta g)\). On the four-cycle, \(f=\delta _1\) satisfies \(f^2=f\); at vertex \(0\), \(\,(\Delta (f^2))(0)=1\) and \(\,((\Delta f)f+f\Delta f)(0)=0\), while \(\,((\Delta f)(Tf)+f\Delta f)(0)=1\). Lemma [fdip-0014] adds a real pairing and identifies the positive kinetic factorization.

Mathlib's fwdDiff_smul proves the three-term formula for an additive commutative monoid, a ring and a module over it. Take the index monoid \(\mathbb Z/n\mathbb Z\), step \(1\), and the regular \(R\)-module \(R\). Scalar multiplication is ring multiplication. Substituting \(Tg=g+\Delta g\) yields the shifted formula; this marker does not claim the endpoint incidence or counting-adjoint theorem.