The Dupont equation
Now we consider the Dupont equation, E63 \(({x = y \diamond (x \diamond (x \diamond y))})\), which can be treated by a greedy translation invariant construction that is more complicated than the one considered for the Asterix law in The Asterix equation.
If we adopt a translation-invariant model
on some abelian group \(G\), then with \(y = x+h\), we have
and so the Dupont law \(x = y \diamond (x \diamond (x \diamond y))\) becomes the functional equation
One way to solve this equation is to have an automorphism \(T: G \to G\) that satisfies the identity
then one can just take \(f(h) = T(h)\). For instance, if \(G = \mathbb{Z}^3\), one can take the automorphism \(T: \mathbb{Z}^3 \to \mathbb{Z}^3\) defined by
We now extend this greedily to \(\mathbb{Z}^3 \times \mathbb{Z}\) as follows. Define a partial solution \((E_1,E_2,f)\) to be a pair \(\mathbb{Z}^3 \subseteq E_1 \subseteq E_2 \subseteq \mathbb{Z}^3 \times \mathbb{Z}\), and a function \(f: E_2 \to E_1\) satisfying the following axioms.
- (a) The set \(E_2 \backslash \mathbb{Z}^3\) is finite.
- (b) For \(h \in \mathbb{Z}^3\), \(f(h) = Th\); in particular, \(f\) is a bijection on \(\mathbb{Z}^3\).
- (c) For \(h \in E_1 \backslash \mathbb{Z}^3\), \(f(h) \in E_1\). Also, \(-h + f^2(h) \in E_1\) and \(f(-h + f^2(h)) = -h\). Note that this (and (b)) implies that \(-h \in E_1\), thus \(E_1\) is symmetric around the origin.
- (d) For \(h \in E_2 \backslash E_1\), \(f(h) \in E_1\).
- (e) The elements \(-h\), \(h - f^2(h)\), and \(f^2(h) - h\) for \(h \in E_2 \backslash E_1\) are all distinct from each other, and all lie outside of \(E_2\). In particular this forces \(f^2(h) \neq 0\), hence \(f(h) \neq 0\). It also forces \(f^2(h) \neq h\), hence \(f(h) \neq h\).
Thus for instance one can take \((\mathbb{Z}^3,\mathbb{Z}^3,T)\) as a partial solution. We say that a partial solution \((E'_1, E'_2, f')\) is an extension of \((E_1,E_2,f)\) if \(E_1 \subseteq E'_1\), \(E'_2 \subseteq E_2\), and \(f'\) agrees with \(f\) on \(E_2\).
Informally, \(E_1\) represents the portion of \(\mathbb{Z}^3 \times \mathbb{Z}\) where we have completely resolved the Dupont equation; the set \(E_2 \backslash E_1\) represents the portion for which \(f\) (and all forward iterates of \(f\)) have been defined, but the Dupont equation has not yet been verified; and the elements \(-h\), \(h - f^2(h)\), and \(f^2(h) - h\) for \(h \in E_2 \backslash E_1\) are the portion where \(f\) is not yet defined, but for which one is ready to “promote” these elements to \(E_2\) or \(E_1\) by defining \(f\) appropriately.
Iterating these lemmas in the usual fashion, we can conclude that any partial solution can be completed to a global model of E63.
Among other things, this permits one to generate models in which the function \(f\) is not injective. To see this, let \(a\) be a non-zero element of \(\mathbb{Z}^3\), let \(x\) be an element of \(\mathbb{Z}^3 \times \mathbb{Z}\) outside of \(\mathbb{Z}^3\), and consider the partial solution \((\mathbb{Z}^3, \mathbb{Z}^3 \cup \{x\}, f)\) where \(f(h) = Th\) for \(h \in \mathbb{Z}^3\) and \(f(x) = a\). One can check that this is a partial solution and is not injective, since \(f(x) = f(T^{-1} a)\). This non-injectivity implies in particular that the model is not left-cancellative, and hence does not satisfy the law
(equation 1692).
Second construction
We now give a second construction, with works on the integers \(G = \mathbb{Z}\).
We first define a seed solution \(f_0: E_0 \to \mathbb{Z}\) defined on the set \(E_0 := \{-7, -3, -2, -1, 0, 1, 3, 4, 6 \}\) with
In this construction, we define a partial solution to be a function \(f: E \to \mathbb{Z}\) defined on a finite subset of \(E\) satisfying the following axioms:
- (i) \(E\) contains \(E_0\), and \(f\) agrees with \(f_0\) on \(E_0\).
- (ii) If \(h \in E\) and \(f(h) \in E\), then \(f^2(h)-h\) is also in \(E\), and \(f(f^2(h)-h) = -h\).
- (iii) If \(h \in E\) and \(h \neq 3\), then \(f(h) \neq 0\).
- (iv) If \(a \neq a'\) are distinct elements of \(E\) with \(f(a)=f(a')\), and \(-a \in E\), then \(a' \neq a + f(-a)\).
- (v) If \(a \neq a'\) are distinct elements of \(E\) with \(f(a)=f(a')\), and \(-a, -a' \in E\), then \(a' + f(-a') \neq a + f(-a)\).
We say that a partial solution \(f': E' \to \mathbb{Z}\) extends another \(f: E \to \mathbb{Z}\) if \(E'\) contains \(E\) and \(f'\) agrees with \(f\) on \(E\).
LemmaExtension#
If \(f: E \to \mathbb{Z}\) is a partial solution and \(h_0 \in \mathbb{Z}\), then there exists an extension \(f': E' \to \mathbb{Z}\) for which axiom (ii) applies, i.e., \(h_0 \in E'\), \(f'(h_0) \in E'\), \((f')^2(h_0)-h_0 \in E'\), and \(f'((f')^2(h_0)-h_0) = -h_0\).
Proof
We divide into cases.
Case 1: \(h_0 \in E\) and \(f(h_0) \in E\). In this case we are already done thanks to axiom (ii).
Case 2: \(h_0 \in E\) but \(f(h_0) \not \in E\). This is the main case. Let \(H\) be the set of all \(h \in E\) such that \(f(h) = f(h_0)\); this is a finite set containing \(h_0\). Let \(H' \subseteq H\) be the set of all \(h' \in H\) such that \(-h' \in E\). We make the following observations:
- (a) All elements \(h\) of \(H\) are non-zero. For if \(h=0\) then \(f(h_0)=f(h)=1 \in E\), contradicting the hypothesis \(f(h_0) \not \in E\).
- (b) If \(h' \in H'\) then \(h' \neq h'+f(-h')\). Otherwise we would have \(f(-h')=0\), then by axiom (iii) we have \(h' = -3\), hence \(f(h_0) = f(h') = 4 \in E\) by axiom (i). But this again contradicts the hypothesis \(f(h_0) \not \in E\). (This is the main reason we take \(E_0\) to be so large.)
- (c) If \(h_1 \in H\) and \(h_2 \in H'\) are distinct then \(h_1 \neq h_2+f(-h_2)\). This follows from axiom (iv).
- (d) If \(h_1, h_2\in H'\) are distinct then \(h_1+f(-h_1) \neq h_2+f(-h_2)\). This follows from axiom (v).
From these observations, we see that if we take \(c\) to be a sufficiently large integer, the following claims hold:
-
- The expressions \(\pm c\), \(\pm(c - h)\) for \(h \in H\), and \(\pm(c-h'-f(-h'))\) for \(h \in H'\) are all distinct from each other.
-
- \(c\) is not expressible as the sum of four or fewer elements of \(\pm (E \cup f(E))\).
We select such a \(c\). We then promote \(f(h_0)\), \(c - h\) for \(h \in H\), and \(-c+h'+f(-h')\) for \(h' \in H'\), thus setting
We then extend \(f\) to \(f': E' \to \mathbb{Z}\) by setting
for all \(h \in H\) and \(h' \in H'\). Axiom (i) is then obvious. Axiom (ii) needs to be verified for the new elements \(h_0\) and \(c-h'\), \(h' \in H'\) of \(E'\) (the other elements will not satisfy the hypotheses of this axiom), but this is routine. In particular \(h_0\) satisfies the required conclusion of this lemma.
We need to verify (iii) for the new elements of \(E'\), but this is clear from property (a) and claim 2.
Now we need to verify (iv). It suffices to do so when at least one of \(a,a',-a\) are new elements of \(E'\). If neither of \(a\), \(-a\) are new, then the only new elements \(a'\) for which \(f(a')\) could equal \(f(a)\) take the form \(c-h\) (thanks to claim 2), but then \(a'\) cannot equal \(a+f(-a)\), again thanks to claim 2. If instead one of \(a, -a\) is new, then from claim 1 the new element must be \(f(h_0)\). There is no old element \(a'\) with \(f(a') = c = f(f(h_0))\), so we must have \(a = -f(h_0)\), but then \(a + f(-a) = -f(h_0)+c\) will not equal \(a'\), again thanks to claim 2.
Finally, we need verify to (v). We may assume that at least one of \(a,a',-a,-a'\) are new elements of \(E'\). As before, this forces the new element to be \(f(h_0)\), and this cannot be \(a\) or \(a'\), so without loss of generality we have \(a = -f(h_0)\) and \(a' \in E\). But then \(a + f(-a) = -f(h_0)+c\) will not equal \(a' + f(-a')\), again thanks to claim 2.
Case 3: \(h_0 \not \in E\) but \(h_0 \in f(E)\). Here we can write \(h_0 = f(h_1)\) where \(h_1\) is of the form in Case 2. Applying the Case 2 construction, we can pass to an extension in which \(f(h_1) = h_0\) lies in \(E\), and so we are now in either Case 1 or Case 2, and so we can again conclude.
Case 4: \(h_0 \not \in E\) and \(h_0 \not \in f(E)\). We let \(c\) be an integer so large that it is not expressible as the sum of four or fewer elements of \(\pm (E \cup f(E))\). We then promote \(h_0\) to \(E\) by setting
and define an extension \(f': E' \to \mathbb{Z}\) by setting \(f'(h_0) := c\). Axioms (i)-(iii) are obvious. For axiom (iv), since \(f'(h_0)\) is not equal to any other value of \(f'\), the only new case introduced is if \(-a = h_0\), but then \(a+f(-a) = -h_0+c\) is distinct from \(a'\) by choice of \(c\). A similar argument yields axiom (v). With this extension, we are now in Case 2, and so we repeat the previous analysis to conclude.
Lean
Stated as Eq63.Greedy.Extension.next; the blueprint marks no proof of it as formalized.
Sources
Iterating this lemma, we conclude
CorollaryGreedy completion of Dupont#
Every partial solution \(f: E \to \mathbb{Z}\) can be extended to a global solution \(f': \mathbb{Z} \to\mathbb{Z}\) of (1).
Lean
Stated as Eq63.Greedy.exists_extension; the blueprint marks no proof of it as formalized.
Sources
CorollaryNon-injective Dupont solution#
The Dupont equation admits non-injective solutions, and hence can violate Equation 1692.
Proof
It suffices to find a partial solution that violates injectivity. This can be done for instance by adjoining \(\{-13, 10\}\) to \(E_0\) and defining \(f(10)= 2 = f(6)\), \(f(-13)=-10\), and performing a finite check to verify that this is still a partial solution.
Lean
Stated as Eq63.Equation63_not_implies_Equation1692; the blueprint marks no proof of it as formalized.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.