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.