theorem PlunneckeInequality.cube_diff_expansion (s : ℝ) (hs0 : 0 < s) (hs1 : s < 1) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (A : Finset (ZMod p)), ↑A.card = ↑p ^ s → ↑(A * A * A - A * A * A).card ≥ ↑p ^ (s + ε)

Plünnecke cube-difference expansion lemma. If $A \subset \mathbb{F}_p$ with $|A| = p^s$ for $0 < s < 1$, then there exists some $\varepsilon = \varepsilon(s) > 0$ such that $|A^3 - A^3| \ge p^{s + \varepsilon}$, witnessing genuine expansion under the combined operations of (multiplicative) cubing and (additive) differencing.