Running a greedy algorithm

Define a partial 854 magma to be a partial function \(\diamond: \mathbb{N} \times \mathbb{N} \to \mathbb{N}\) satisfying the following axioms:

  • (Equation 854) If \(x,y,z \in \mathbb{N}\) are such that \((y \diamond z) \diamond (x \diamond z)\) is well-defined, then \(x \diamond ((y \diamond z) \diamond (x \diamond z))\) is well-defined and equal to \(x\).
  • (Equation 8) If \(x \in \mathbb{N}\) are such that \(x \diamond x\) is well-defined, then \(x \diamond (x \diamond x)\) is well-defined and equal to \(x\).
  • (Equation 101) If \(x,y \in \mathbb{N}\) are such that \((x \diamond y) \diamond x\) is well-defined, then \(x \diamond ((x \diamond y) \diamond x)\) is well-defined and equal to \(x\).
  • (Equation 46155) If \(x,y \in \mathbb{N}\) are such that \(x \diamond (x \diamond y)\) is well-defined, then \((x \diamond y) \diamond (x \diamond (x \diamond y))\) is well-defined and equal to \(x \diamond y\).
  • (Equation 378) If \(x,y \in \mathbb{N}\) is such that \(x \diamond y\) is well-defined, then \((x \diamond y) \diamond y\) is well-defined and equal to \(x \diamond y\).
  • (No idempotence) If \(x \in \mathbb{N}\) is such that \(x \diamond x\) is well-defined, then \(x \diamond x \neq x\).
  • (Auxiliary law) If \(x,y \in \mathbb{N}\) are such that \(x \diamond (x \diamond y)\) is well-defined and equal to \(x\), then \(x=y\).
  • (Unique factorization) If \(x,y,x',y' \in \mathbb{N}\) are such that \(x \diamond y\), \(x' \diamond y'\) are well-defined and equal to each other, then at least one of the assertions \(x \diamond y = x\), \(x' \diamond y' = x'\), or \((x,y) = (x',y')\) is true.
  • (Monotonicity) If \(x,y \in \mathbb{N}\) is such that \(x \diamond y\) is defined, then either \(x \diamond y = x\) or \(x \diamond y > x, y\).

The first five laws are known consequences of 854. The no idempotence law was known for the free magma \(M_{854}\) because it maps to finite magmas without idempotents, such as \(\mathbb{Z}/3\mathbb{Z}\) with law \(x \diamond y = x - 1_{x=y}\). The unique factorization law is also known for the free magma by Unique factorization. The auxiliary law is a “leap of faith” that helped close the greedy argument, and the monotonicity property is a technical consequence of the greedy construction that will also help close the argument.

The following observation is key.

PropositionGreedy construction#

Suppose one has a partial 854 magma on \(\mathbb{N}\) that is only finitely defined, and let \(a,b \in G\) be such that \(a \diamond b\) is currently undefined. Then it is possible to extend the magma to a larger partial 854 magma, such that \(a \diamond b\) is now defined.

Proof

Define a directed graph by writing \(x \to y\) if \(y \diamond x\) is defined and equal to \(y\). By Equation 378, we see that \(x \to y\) if and only if \(z \diamond x\) is well-defined and equal to \(y\) for some \(z\).

From unique factorization, we see that \(b\) has at most one representation of the form \(b = b_1 \diamond b_2\) with \(b_1 \neq b\), or equivalently \(b_2 \not \to b_1\). We define \(b_1, b_2\) accordingly if such a representation exists, otherwise we leave \(b_1, b_2\) undefined. We say that \(b_1\) is relevant if \(b_2 \to a\). Note that this forces \(a \neq b_1\) since \(b_2 \not \to b_1\). Also, if \(b_1,b_2\) exist, we see from monotonicity that \(b = b_1 \diamond b_2 > b_1, b_2\).

Let \(c\) be a natural number that is larger than any number appearing in anywhere in the partial 854 magma multiplication table (in particular it is larger than \(a,b\), as well as \(b_1,b_2\) if they are defined). We then extend the multiplication table by defining \(a \diamond b = c\), \(b \diamond c = b\), and \(c \diamond b = c\). If \(b_1\) exists and is relevant, we also define \(b_1 \diamond c = b_1\). Finally, if \(b_1\) exists and is relevant, and additionally \(b \to b_1\), then we also define \(c \diamond b_1 = c\). We remark that all new entries added are of the left absorptive form \(x \diamond y = x\), except for \(a \diamond b = c\).

We now verify that all of the axioms of a partial 854 magma continue to hold. We begin with all the axioms except for 854:

  • Monotonicity: Observe that all the new values \(x \diamond y\) of the multiplication table introduced are either equal to \(x\), or larger than both \(x\) and \(y\), so the monotonicity property is preserved.
  • Unique factorization: the only way unique factorization breaks is if there is an element \(z\) that has two distinct factorizations \(z = x \diamond y = x' \diamond y'\) with neither \(x \diamond y\) nor \(x' \diamond y'\) a left absorptive product. Since the only non-left-absorptive product introduced is \(a \diamond b = c\), and \(c\) has no prior representation as a product, we see that the unique factorization property is preserved.
  • No idempotence: The only possible product \(x \diamond x\) that could be introduced here is \(a \diamond b\) if \(x=a=b\), but in that case \(x \diamond x = a \diamond b = c\) is clearly not equal to \(x\), so the no idempotence property is preserved.
  • Equation 8: If \(x \diamond x\) were already defined in the previous magma, the claim would already be established, so \(x \diamond x\) must be one of the new products \(a \diamond b\), \(b \diamond c\), \(c \diamond b\), \(b_1 \diamond c\), or \(c \diamond b_1\). As \(c \neq a,b,b_1\), the only option is \(x = a = b\), but then \(x \diamond (x \diamond x) = b \diamond c = b = x\), as required.
  • Equation 101: By Equation 8, we may assume \(x \diamond y \neq x\), which implies \(y \neq c\) since \(x \diamond c = x\) whenever the left-hand side is defined. We can also assume \(x \neq c\), since we have \(c \diamond z = c\) whenever the left-hand side is defined. If \(x \diamond y = c\), then \((x,y) = (a,b)\); as \((x \diamond y) \diamond x = c \diamond x\) is well-defined, \(x=a\) is then either equal to \(b\), or equal to \(b_1\) if the latter exists and is relevant. But the second case cannot occur since \(a \neq b_1\), so we have \(x = b\), and then \(x \diamond ((x \diamond y) \diamond x) = b \diamond (c \diamond b) = b = x\), giving the claim. So we may assume \(x \diamond y \neq c\). If \((x \diamond y, x) \neq (a,b)\), then \((x \diamond y) \diamond x\) was already defined in the original partial magma, and the claim follows from Equation 101; hence we may assume \((x \diamond y, x) = (a,b)\), then \(x \diamond ((x \diamond y) \diamond x) = b \diamond c = b = x\), giving the claim.
  • Equation 46155: By Equation 8, we may assume \(x \diamond y \neq x\) and hence \(y \neq c\) as before. The case \(x=c\) is not possible, as this forces \(x \diamond y = c\) and then \(x \diamond (x \diamond y)\) is undefined. If \(x \diamond y = c\), then \((x,y) = (a,b)\); in order for \(x \diamond (x \diamond y) = a \diamond c\) to be defined, either \(a=b\) or \(a=b_1\) with \(b_1\) relevant, but the latter is impossible since \(a \neq b_1\); thus \(x=y=a=b\) and \((x \diamond y) \diamond (x \diamond (x \diamond y)) = c \diamond (b \diamond c) = c = (x \diamond y)\), giving the claim. Thus we may assume \(x \diamond y \neq c\). If \((x, x \diamond y) \neq (a,b)\) then \(x \diamond (x \diamond y)\) was already defined in the original partial magma, and the claim follows from Equation 46155; hence we may assume \((x, x \diamond y) = (a,b)\), and we have \((x \diamond y) \diamond (x \diamond (x \diamond y)) = b \diamond c = b = x \diamond y\), giving the claim.
  • Equation 378: We can assume \(x \diamond y \neq x\), since the claim is trivial otherwise. This rules out the \(y=c\) and \(x=c\) cases. The only new case is then if \(x \diamond y = c\), but forces \((x,y) = (a,b)\), and then \((x \diamond y) \diamond y = c \diamond b = c = x \diamond y\), giving the claim.
  • Auxiliary law: if \(x=c\), then the only possible value for \(x \diamond y\) is \(c\), and \(c \diamond c\) is undefined, contradiction; thus \(x \neq c\). If \(y = c\), then the only possible value for \(x \diamond y\) is \(x\), and then \(x \diamond (x \diamond y)\) cannot equal \(x\) by the no idempotence law. Thus \(y \neq c\). Since \(x \diamond (x \diamond y) = x\) is not equal to \(c\), \((x,x \diamond y)\) is not equal to \((a,b)\). If \((x,y) \neq (a,b)\), then both \(x \diamond y\) and \(x \diamond (x \diamond y)\) were already defined in the original partial magma, and the claim follows from the auxiliary law for that magma. Thus we may assume \((x,y) = (a,b)\), in which case \(a \diamond c = a\), hence by construction either \(a=b\) or \(a=b_1\). If \(a=b\) then we are done. If \(a = b_1\), then \(b_1\) cannot be relevant, and then \(a \diamond c = b_1 \diamond c\) remains undefined, a contradiction.

Now we tackle the most difficult verification, which is 854. This splits into a large number of cases.

  • Case 1: \(x=c\). Then \(x \diamond z\) can only equal \(c\), hence \(z\) equals \(b\) or \(b_1\); and \(y \diamond z\) can also only equal \(b\) or \(b_1\), and \((y \diamond z) \diamond (x \diamond z)\) is equal to \(y \diamond z\). If \(y \diamond z = b\), then we are done since \(c \diamond b = c\). If \(y \diamond z = b_1\), then \(b_1 \diamond c\) needs to be defined, so \(b_1\) is relevant. Furthermore, from equation 378 we have \(b_1 \diamond z = b_1\), hence by the no idempotence property \(z\) must equal \(b\), so \(b \to b_1\), and hence \(c \diamond b_1 = c\), giving the claim.
  • Case 2: \(x \neq c\), \(z = c\). This forces \(x,y=b,b_1\) with \(y \diamond z = y\) and \(x \diamond z = x\), thus \(y \diamond x\) is well-defined and we need \(x \diamond (y \diamond x)\) well-defined and equal to \(x\). If \(x=y\), this follows from Equation 8; otherwise, either \(x = b_1 \diamond b_2\) and \(y = b_1\) or \(x = b_1\) and \(y = b_1 \diamond b_2\), and the claim follows from Equation 101 or Equation 46155 respectively.
  • Case 3: \(x, z \neq c\), \(y = c\). Then \(z\) must equal \(b\) or \(b_1\), \(y \diamond z\) must equal \(c\), and \(x \diamond z\) must equal \(b\) or \(b_1\), and \((y \diamond z) \diamond (x \diamond z)\) must equal \(c\), with the \(b_1\) options only available if \(b_1\) is relevant. If \(x \diamond z = z\) then by equation 378, \(z \diamond z = z\), contradicting the no idempotence law. Thus we either have \(z=b_1, x \diamond z = b\) or \(z = b, x \diamond z = b_1\), and in either case \(b_1\) must be relevant. If \(z \to x\), then either have \(x=b\), or \(x = b_1\) and \(b_1\) is relevant, and in either case we have \(x \diamond c = x\) as required. So we may assume \(z \not \to x\). In the case \(z = b_1, x \diamond z = b = b_1 \diamond b_2\) we may then apply unique factorization to conclude that \(z = b_2\) and \(x = b_1\), thus \(x \diamond c = x\) as required. In the opposite case \(z = b\), \(x \diamond z = b_1\) with \(z \not \to x\), we see from monotonicity that \(b_1 = x \diamond z > z = b\); but from monotonicity again \(b = b_1 \diamond b_2 > b_1\), a contradiction.
  • Case 4: \(x,y,z \neq c\), \((y,z) = (a,b)\). Here, \(y \diamond z\) and \((y \diamond z) \diamond (x \diamond z)\) must equal \(c\), and \(x \diamond z\) must then equal \(b\) or \(b_1\), with the latter an option only if \(b_1\) is relevant. If \(x \diamond z = b\), then by Equation 378, \(b \diamond b = b\), contradicting idempotence, thus \(x \diamond z = b_1\) and \(b_1\) is relevant, and then \(b \to b_1\) by Equation 378 again. If \(z \to x\), then \(x = b_1\), and the claim follows since \(b_1 \diamond c = c\), so we may assume \(z \not \to x\). By monotonicity, this forces \(b_1 = x \diamond z > z = b\) and \(b = b_1 \diamond b_2 > b_1\), a contradiction.
  • Case 5: \(x,y,z \neq c\), \((y,z) \neq (a,b)\), \((x,z) = (a,b)\). Now \(x \diamond z = c\), and \(y \diamond z\) must equal \(b\) or \(b_1\). If \(y \diamond z = b\), then by Equation 378, \(b \diamond b = b\), contradicting idempotence, thus \(y \diamond z = b_1\) and \(b_1\) is relevant, and then \(b \to b_1\) by Equation 378 again, so \(b_1 \diamond (b_1 \diamond b_2) = b_1\). By the auxiliary law, this forces \(b_1 = b_2\), so \(x = b_1\), and then we are done since \(b_1 \diamond c = b_1\).
  • Case 6: \(x,y,z \neq c\), \((y,z), (x,z) \neq (a,b)\), \((y \diamond z, x \diamond z) = (a,b)\). Here \(x \diamond z = b\) and \((y \diamond z) \diamond (x \diamond z) = c\). If \(z \to x\), then \(x=b\) and we are done since \(b \diamond c = b\). If \(z \not \to x\), then by unique factorization applied to \(x \diamond z = b_1 \diamond b_2\) we have \((x,z) = (b_1,b_2)\). By Equation 378, we have \(z \to y \diamond z\), hence \(b_2 \to a\), so \(b_1\) is relevant. We are now done since \(b_1 \diamond c = b_1\).
  • Case 7: \(x,y,z \neq c\), \((y,z), (x,z) \neq (a,b), (y \diamond z, x \diamond z) \neq (a,b)\). In this case \(x \diamond ((y \diamond z) \diamond (x \diamond z))\) would already have been defined and equal to \(x\) in the previous partial magma, thanks to Equation 854.
Lean

Stated as Refutation_854.Greedy.Extension1.next_ok; the blueprint marks no proof of it as formalized.

Sources
LeanRefutation_854.Greedy.Extension1.next_ok

Iterating this in the usual fashion, we obtain

Corollary854 extension#

Suppose one has a partial 854 magma on \(\mathbb{N}\) that is only finitely defined. Then it can be extended to a complete 854 magma that additionally satisfies the no idempotence law, the monotonicity law, the auxiliary law, and the unique factorization law.

Proof

Apply the usual greedy algorithm.

Lean

Stated as Refutation_854.Greedy.exists_extension; the blueprint marks no proof of it as formalized.

Sources
LeanRefutation_854.Greedy.exists_extension

Corollary854 does not not imply 413#

There is an 854 magma which does not satisfy the 413 law \(x = x \diamond (x \diamond (x \diamond (y \diamond x)))\).

Proof

Create a partial magma by imposing the laws \(1 \diamond 0 = 2\), \(0 \diamond 2 = 3\), \(2 \diamond 0 = 2\), \(3 \diamond 2 = 3\). One can check that this is a partial magma. We then extend it to a global magma using 854 extension. We claim that we have the 413 violation

\[ 0 \diamond (0 \diamond (0 \diamond (1 \diamond 0))) = 0 \]

or equivalently

\[ 0 \diamond (0 \diamond 3) = 0. \]

Indeed this is immediate from the auxiliary law.

Lean

Stated as Refutation_854.not_413_1045; the blueprint marks no proof of it as formalized.

Sources
LeanRefutation_854.not_413_1045

Corollary854 does not not imply 1045#

There is an 854 magma which does not satisfy the 1045 law \(x = x \diamond ((y \diamond (y \diamond x)) \diamond x)\).

Proof

Similar to previous, but start with the seed

\[ 0 \diamond 0 = 2; 0 \diamond 1 = 0 \diamond 2 = 0; 1 \diamond 2 = 3; 2 \diamond 0 = 2 \diamond 1 = 2 \diamond 3 = 2; 3 \diamond 2 = 3 \]

which already violates the law with \(x=1,y=0\), and can be verified to be a partial 854 magma.

Lean

Stated as Refutation_854.not_413_1045; the blueprint marks no proof of it as formalized.

Sources
LeanRefutation_854.not_413_1045

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.