Documentation

FormalConjectures.GreensOpenProblems.«57»

Ben Green's Open Problem 57 #

Reference: Ben Green's Open Problem 57

Let $G$ be a finite abelian group. Consider the space $\Phi(G)$ of all functions on $G$ which are "convex combinations" (in the sense of complex coefficients $c_i$ with $\sum |c_i| \le 1$) of functions of the form $$\phi(g) := \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)$$ with $\|f_i\|_\infty \le 1$ (where $f_i : G \times G \to \mathbb{C}$).

Let $\Phi'(G)$ be the space defined similarly, but with $f_3(x_1, x_2)$ required to be a function of $x_1 + x_2$. Do $\Phi(G)$ and $\Phi'(G)$ coincide?

Note: The "convex combination" here uses complex coefficients whose absolute values sum to at most 1 (cf. personal communication with B. Green, April 2026). Since the base sets are balanced (closed under multiplication by unit complex numbers), this absolutely convex hull equals the real convex hull of the complex-valued base set.

Motivation: $\Phi(G)$ is a 'generalised convolution algebra' as considered by Conlon–Fox–Zhao, whereas $\Phi'(G)$ consists of Tao's $\text{UAP}_2(G)$-functions.

def Green57.tripleKernel (G : Type u_1) [AddCommGroup G] [Fintype G] (f₁ f₂ f₃ : G × G) :
G

Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g. The functions fᵢ are complex-valued.

Equations
Instances For
    def Green57.baseΦ (G : Type u_1) [AddCommGroup G] [Fintype G] :
    Set (G)

    The generating family of functions for Φ(G). The functions fᵢ : G × G → ℂ are bounded by 1 in sup norm.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Green57.baseΦ' (G : Type u_1) [AddCommGroup G] [Fintype G] :
      Set (G)

      The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Green57.Φ (G : Type u_1) [AddCommGroup G] [Fintype G] :
        Set (G)

        The space Φ(G) of "convex combinations" of kernels from baseΦ.

        Since baseΦ G is balanced (closed under multiplication by unit complex numbers) and contains 0, the absolutely convex hull over ℂ (i.e., the set of $\sum c_i \phi_i$ with $\phi_i \in \text{baseΦ}$ and $\sum |c_i| \le 1$) coincides with the real convex hull.

        Equations
        Instances For
          def Green57.Φ' (G : Type u_1) [AddCommGroup G] [Fintype G] :
          Set (G)

          The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ'.

          Equations
          Instances For
            def Green57.functional (G : Type u_1) [Fintype G] (a φ : G) :

            The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g.

            Equations
            Instances For
              def Green57.supportFn (G : Type u_1) [Fintype G] (a : G) (S : Set (G)) :

              The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩.

              Equations
              Instances For
                theorem Green57.green_57.variants.z3_functional :
                have a := ![-1, -3, 3]; True supportFn (ZMod 3) a (Φ' (ZMod 3)) < supportFn (ZMod 3) a (Φ (ZMod 3))

                For $G = \mathbb{Z}/3\mathbb{Z}$ and the functional $a(0) = -1$, $a(1) = -3$, $a(2) = 3$, does the support function of $\Phi$ at $a$ strictly exceed that of $\Phi'$?

                Numerical evidence suggests the answer is yes: $$\sup_{\varphi \in \Phi'(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle \;<\; \sup_{\varphi \in \Phi(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle.$$

                The DeepMind prover agent provided a formal proof, showing that $\frac{183095}{30000}$ separates the support functions.

                Do $\Phi(\mathbb{Z}/3\mathbb{Z})$ and $\Phi'(\mathbb{Z}/3\mathbb{Z})$ coincide?

                Numerical evidence suggests the answer is no: the integer functional $a = (-1, -3, 3)$ separates the two spaces. A branch-and-bound verification over the phase variables shows $\max_{\Phi'} \operatorname{Re}\langle a, \varphi \rangle < 6.112 < 6.115 \approx \max_{\Phi} \operatorname{Re}\langle a, \varphi \rangle$.

                theorem Green57.green_57 :
                False ∀ (G : Type) [inst : AddCommGroup G] [inst_1 : Fintype G] [DecidableEq G], Φ G = Φ' G

                Is it true that for every finite abelian group $G$ the spaces $\Phi(G)$ and $\Phi'(G)$, obtained from kernels $\phi(g) = \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)$ with $\lVert f_i \rVert_\infty \le 1$ (where $f_i : G \times G \to \mathbb{C}$), still coincide when the third kernel is required to depend only on $x_1 + x_2$?

                Green guesses that the answer is probably 'no'.