1323

Stream: Equational

[Bernhard Reinke]

The implication 1323 => 2744 is the last open implication for 1323.

First let's summarize what is known so far:

If we write $L_y(x) = y \diamond x, R_y(x) = x \diamond y$, then 1323 can be written as $L_y \circ R_y \circ L_{y^2} = Id$, whereas 2744 is $R_y \circ L_{y^2} \circ L_y = Id$.

This implies that $L_y$ is always surjective and $L_{y^2}$ is injective, so in fact $L_{y^2}$ is a bijection. So we can conjugate 1323 by $L_{y^2}$ and show the implication 1323 => 1526. In particular, $R_y$ is always injective, so the magma is right cancellative. Moreover, a model of 1323 satisfies 2744 iff $L_{y}$ is a bijection, as we then conjugate the equation by $L_{y}$. This rules out counterexamples that are finite or where every element is a square (i.e., transitive models), or linear models.

Here is my current line of attack: 1323 has a model of size 2 that is just $\mathbb F_2$ with addition. I want to construct a model that admits a magma homomorphism to $\mathbb F_2$ (and a little bit more). I think the following should be possible:

There is an infinite set $X$ together with four functions $a,b,c,d : X \times X \rightarrow X$ satisfying $a(x,x) = b(x,x) = c(x,x) = d(x,x) = x$ such that the magma on $X \times \{0, 1\}$ defined via

$$(x,0) \diamond (y,0) = (a(x,y), 0) \\ (x,0) \diamond (y,1) = (b(x,y), 1) \\ (x,1) \diamond (y,0) = (c(x,y), 1) \\ (x,1) \diamond (y,1) = (d(x,y), 0)$$

satisfies 1323 but not 2744.

For such a magma, we have that the squares are exactly the elements of the form $(x,0)$, every square is idempotent. The squares form a submagma that satisfies 125. In particular, a is left and right cancellative.

Let us note that $(x,0) \diamond (x,0) = (x, 0)$ and $(x,1) \diamond (x,1) = (x,0)$ as we assumed $a(x,x) = d(x,x) = x$. So, we can write 1323 in the functions a,b,c,d in the following way (already in a suggestive "rule" version): (here I enumerate the 4 cases for the starting values in {0,1}:

$$a(y,x) = z \wedge a(z,y) = w \Rightarrow a(y,w) = x \\ b(y,x) = z \wedge c(z,y) = w \Rightarrow b(y,w) = x \\ a(y,x) = z \wedge b(z,y) = w \Rightarrow d(y,w) = x \\ b(y,x) = z \wedge d(z,y) = w \Rightarrow c(y,w) = x \\$$

Since our magma is right cancellative, we have that each of the a,b,c,d should be right cancellative. Also, since left-multiplication with squares is a bijection, we also get that a and b are left-cancellative. A magma that fails to satisfy 2744 should have c or d to be not left-cancellative.

My hope is that these observations can be the basis of a greedy argument now working with four relations $A, B, C, D \subset X \times X \times X$ that are partial assignments for $a,b,c,d$. Part of the reason I am optimistic is that the greedy algorithm for 125 with the relation a(x,x) = x seems to terminate.

Attached is my tptp file that should model the construction I have in mind. I have still to figure out how to adjust the greedy algorithm to multiple relations.

1323_functional.p

Edit: I fixed some naming issues in the file. Also now, the there is again the proper conjecture that d is left-cancellative.

[Michael Bucko]

@Bernhard Reinke Thank you for sharing the tptp. That's very helpful.

[Bernhard Reinke]

@Michael Bucko I fixed some minor issues in the file, if you want, you can have a look at the new version

[Daniel Weber]

This looks interesting, I'll see tomorrow if I can adapt the greedy automation to this

[Michael Bucko]

Turned it into a C++ script with Z3++.h. Attaching the script for the reference.
1323.cpp

The output is:

The conjecture is **not** entailed by the axioms (satisfiable).

Counterexample:

;; universe for Element:

;;   Element!val!3 Element!val!13 Element!val!18 Element!val!0 Element!val!2 Element!val!16 Element!val!1 Element!val!11 Element!val!15 Element!val!4 Element!val!17 Element!val!10 Element!val!12 Element!val!19 Element!val!5 Element!val!6 Element!val!7 Element!val!14 Element!val!8 Element!val!9

;; -----------

;; definitions for universe elements:

(declare-fun Element!val!3 () Element)

(declare-fun Element!val!13 () Element)

(declare-fun Element!val!18 () Element)

(declare-fun Element!val!0 () Element)

(declare-fun Element!val!2 () Element)

(declare-fun Element!val!16 () Element)

(declare-fun Element!val!1 () Element)

(declare-fun Element!val!11 () Element)

(declare-fun Element!val!15 () Element)

(declare-fun Element!val!4 () Element)

(declare-fun Element!val!17 () Element)

(declare-fun Element!val!10 () Element)

(declare-fun Element!val!12 () Element)

(declare-fun Element!val!19 () Element)

(declare-fun Element!val!5 () Element)

(declare-fun Element!val!6 () Element)

(declare-fun Element!val!7 () Element)

(declare-fun Element!val!14 () Element)

(declare-fun Element!val!8 () Element)

(declare-fun Element!val!9 () Element)

;; cardinality constraint:

(forall ((x Element))

        (or (= x Element!val!3)

            (= x Element!val!13)

            (= x Element!val!18)

            (= x Element!val!0)

            (= x Element!val!2)

            (= x Element!val!16)

            (= x Element!val!1)

            (= x Element!val!11)

            (= x Element!val!15)

            (= x Element!val!4)

            (= x Element!val!17)

            (= x Element!val!10)

            (= x Element!val!12)

            (= x Element!val!19)

            (= x Element!val!5)

            (= x Element!val!6)

            (= x Element!val!7)

            (= x Element!val!14)

            (= x Element!val!8)

            (= x Element!val!9)))

;; -----------

(define-fun W () Element

  Element!val!1)

(define-fun Y () Element

  Element!val!3)

(define-fun Z () Element

  Element!val!5)

(define-fun X () Element

  Element!val!0)

(define-fun b ((x!0 Element) (x!1 Element)) Element

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!1)) Element!val!8

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!3)) Element!val!9

  (ite (and (= x!0 Element!val!5) (= x!1 Element!val!0)) Element!val!12

  (ite (and (= x!0 Element!val!1) (= x!1 Element!val!3)) Element!val!15

    Element!val!0)))))

(define-fun c ((x!0 Element) (x!1 Element)) Element

  (ite (and (= x!0 Element!val!5) (= x!1 Element!val!0)) Element!val!10

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!1)) Element!val!13

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!3)) Element!val!16

  (ite (and (= x!0 Element!val!1) (= x!1 Element!val!3)) Element!val!17

    Element!val!0)))))

(define-fun a ((x!0 Element) (x!1 Element)) Element

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!1)) Element!val!2

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!3)) Element!val!4

  (ite (and (= x!0 Element!val!5) (= x!1 Element!val!0)) Element!val!6

  (ite (and (= x!0 Element!val!1) (= x!1 Element!val!3)) Element!val!7

    Element!val!0)))))

(define-fun d ((x!0 Element) (x!1 Element)) Element

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!1)) Element!val!11

  (ite (and (= x!0 Element!val!5) (= x!1 Element!val!0)) Element!val!14

  (ite (and (= x!0 Element!val!0) (= x!1 Element!val!3)) Element!val!18

  (ite (and (= x!0 Element!val!1) (= x!1 Element!val!3)) Element!val!19

    Element!val!0)))))

[Bernhard Reinke]

Is this a finite model? If so, then I probably did a mistake in the encoding, a finite counterexample shouldn't be possible

[Michael Bucko]

Bernhard Reinke schrieb:

Is this a finite model? If so, then I probably did a mistake in the encoding, a finite counterexample shouldn't be possible

Yes, I think so (the universe is defined with 20 distinct elements).

Perhaps I made a mistake in the code though. I'll have a look too.

[Terence Tao]

@Bernhard Reinke I like the emerging new strategy of constructing potential counterexample magmas by making them "extensions" of simple base magmas (where by "extension" I mean "has a surjective magma homomorphism to the base"). We have been experimenting with a similar strategy in 1485, although the order two base we used was a bit too simple to refute anything new. My "ad hoc" counterexample to 1437 (with a base of order 3) can also retroactively be considered as an instance of this method. Hopefully the method actually works in more cases, in any case I will add it to our list of techniques.

[Terence Tao]

Michael Bucko said:

Yes, I think so (the universe is defined with 20 distinct elements).

Perhaps I made a mistake in the code though. I'll have a look too.

An order 20 magma should be easily testable in Finite Magma Explorer.

[Amir Livne Bar-on]

I think I got it? Disclaimer: used a tool I'm not familiar with and I don't fully understand its results.

I've been thinking about how to make $L_y$ surjective and not injective. This means deleting some information, e.g. by working in the free semi-group and having $x \diamond y$ delete some portion of $y$ specified by $x$. I couldn't get this to work, and I wondered whether I'm going entirely the wrong way. A feature of this kind of construction is that $x \diamond x = e$. This is something we can write down as equations, so I tried it in Twee.

The following input file:

fof(eq1323, axiom,
    ![X, Y]: X = mul(Y, mul(mul(mul(Y, Y), X), Y))).

fof(diag, axiom,
    ![X, Y]: mul(X, X) = mul(Y, Y)).

fof(eq2744, conjecture,
    ![X, Y]: x = mul(mul(mul(Y, Y), mul(Y, X)), Y)).

results in CounterSatisfiable (the conjecture is false). The full output is attached.
out.txt

[Michael Bucko]

Amazing! Is Twee this one https://github.com/nick8325/twee ?

(I am still trying to learn how to convert the z3 format to the magma operator table)

[Bernhard Reinke]

Unfortunately, I think there is a typo in

fof(eq2744, conjecture,
    ![X, Y]: x = mul(mul(mul(Y, Y), mul(Y, X)), Y)).

you used lowercase xon the LHS. This would mean that there is a constant x such that the RHS is always equal to x. I also stumbled in this trap at some point :melting_face:

[Sebastian Flor]

If I understand you correctly, your construction fullfills the constant diagonal

$$x\diamond x = e$$

with constant e. But then 1323 becomes

$$x = y\diamond((e \diamond x)\diamond y).$$

for arbitrary y. And by inserting first

$$y = e\diamond x$$

we derive at

$$x=(e\diamond x)\diamond e$$

and by using this and setting y = e we get

$$x = e\diamond x$$

Therefore 1323 and 2744 just become the Putnam Laws,

$$x = y\diamond (x\diamond y)\\ x=(y\diamond x)\diamond y$$

which are equivalent. Did I misunderstand your counterexample?

[Amir Livne Bar-on]

No, you understood me perfectly. And it's a good argument. If $e$ is a neutral element then they immediately become the Putnam laws, and even if not, they are equivalent.

[Amir Livne Bar-on]

Michael Bucko said:

Amazing! Is Twee this one https://github.com/nick8325/twee ?

(I am still trying to learn how to convert the z3 format to the magma operator table)

Yes, that's the one

[Terence Tao]

Amazing to see a cameo role of the Putnam problems in this late stage of the project! [It really reinforces the observation that this project isn't just 4694 separate subprojects; they all synergize with each other, sometimes in unexpected ways. 1323 is also in some ways a "mirror image" of Ramanujan, so I expect a lot of the insights we gather here to have some analogues for Ramanujan as well.]

Anyway, we now know that squaring can't be either constant or surjective to create a counterexample; it has to be something in between. In that respect the F_2-extended model suggested by @Bernhard Reinke has some potential, since only half the model gets to be a square.

[Bernhard Reinke]

Michael Bucko said:

Bernhard Reinke schrieb:

Is this a finite model? If so, then I probably did a mistake in the encoding, a finite counterexample shouldn't be possible

Yes, I think so (the universe is defined with 20 distinct elements).

Perhaps I made a mistake in the code though. I'll have a look too.

Hm, could it be that in your code you consider X, Y, Z, W as constants? Probably you need to bound them by quantifiers in the axioms.

[Michael Bucko]

Bernhard Reinke schrieb:

Michael Bucko said:

Bernhard Reinke schrieb:

Is this a finite model? If so, then I probably did a mistake in the encoding, a finite counterexample shouldn't be possible

Yes, I think so (the universe is defined with 20 distinct elements).

Perhaps I made a mistake in the code though. I'll have a look too.

Hm, could it be that in your code you consider X, Y, Z, W as constants? Probably you need to bound them by quantifiers in the axioms.

I think you're right.
I only now started playing with the Z3 C++ API. It's perhaps fixed already. (it's running / not crashing / not stopping)

For reference, ver 2.0. 1323-2.cpp

[Bernhard Reinke]

Here is a sanity check, a lean proof that a tuple a,b,c,d satisfying my conditions would indeed give a counterexample (actually, b(x,x) = x and c(x,x) = x are not needed for this):

import Mathlib.Tactic

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

abbrev Equation1323 (G: Type _) [Magma G] := ∀ x y : G, x = y ◇ (((y ◇ y) ◇ x) ◇ y)

abbrev Equation2744 (G: Type _) [Magma G] := ∀ x y : G, x = ((y ◇ y) ◇ (y ◇ x)) ◇ y

theorem Construction_shows_Equation1323_not_implies_Equation2744 (X : Type) (a b c d : X → X → X)
(a_idem : ∀ x, a x x = x) (d_idem : ∀ x, d x x = x)
(r1 : ∀ x y z w, a y x = z ∧ a z y = w → a y w = x)
(r2 : ∀ x y z w, b y x = z ∧ c z y = w → b y w = x)
(r3 : ∀ x y z w, a y x = z ∧ b z y = w → d y w = x)
(r4 : ∀ x y z w, b y x = z ∧ d z y = w → c y w = x)
(d_not_cancellative : ∃ x y z w, d x y = z ∧ d x w = z ∧ y ≠ w) :
∃ (G: Type) (_: Magma G), Equation1323 G ∧ ¬ Equation2744 G := by
  let instMagma : Magma (X × Bool) := {
    op := fun x y => match x, y with
    | (x, false), (y, false) => (a x y, false)
    | (x, false), (y, true) => (b x y, true)
    | (x, true), (y, false) => (c x y, true)
    | (x, true), (y, true) => (d x y, false)
  }
  use X × Bool, instMagma
  constructor
  · intro
    | (x, false), (y, false) =>
      simp only [Magma.op, a_idem, Prod.mk.injEq, and_true]
      symm
      eapply r1
      tauto
    | (x, false), (y, true) =>
      simp only [Magma.op, d_idem, Prod.mk.injEq, and_true]
      symm
      eapply r3
      tauto
    | (x, true), (y, false) =>
      simp only [Magma.op, a_idem, Prod.mk.injEq, and_true]
      symm
      eapply r2
      tauto
    | (x, true), (y, true) =>
      simp only [Magma.op, d_idem, Prod.mk.injEq, and_true]
      symm
      eapply r4
      tauto
  · rcases d_not_cancellative with ⟨x, y, z, w, eq1, eq2, ineq⟩
    intro eq
    have s := eq (y,true) (x,true)
    have t := eq (w,true) (x,true)
    simp only [Magma.op, eq1, Prod.mk.injEq, and_true] at s
    simp only [Magma.op, eq2, Prod.mk.injEq, and_true] at t
    rw [s,t] at ineq
    exact ineq rfl

[Michael Bucko]

I tried to turn this into an mzn (for minizinc). It couldn't find the solution (result: UNSATISFIABLE).

Playground.mzn

[Bernhard Reinke]

Can minizinc produce infinite models? We know that there shouldn't be a finite counterexample.

[Michael Bucko]

Bernhard Reinke schrieb:

Can minizinc produce infinite models? We know that there shouldn't be a finite counterexample.

I checked the reference manual, and couldn't find anything related to infinite models. So maybe it doesn't support them.

But perhaps someone who knows minizinc better could help.

[Bernhard Reinke]

Daniel Weber said:

This looks interesting, I'll see tomorrow if I can adapt the greedy automation to this

That would be nice! One thing I noticed is that the Greedy Algorithm doesn't like the idempotent law yet, as it is a rule without any assumptions. Maybe a first step would be allowing the idempotent law in the classical algorithm

[Daniel Weber]

The problem with it is that it makes the notion of a "fresh variable" different, as it must have $R(c, c, c)$ already. However, one can use $R(a, b, c) \to (R(a, a, a) \land R(b, b, b) \land R(c, c, c))$ as a workaround

[Daniel Weber]

Is there an equation where the idempotent law is useful? Nvm, I just noticed you have it here

[Bernhard Reinke]

Hm, even without the idempotent law, something weird happens if I run the greedy algorithm for 125. I get something like this

[Rule([[0, 1, 2], [0, 1, 3]], [2, 3])
, Rule([[0, 1, 2], [2, 0, 3]], [0, 3, 1])
, Rule([[0, 1, 2], [0, 3, 2]], [3, 1])
, Rule([[0, 1, 2], [0, 3, 2], [4, 5, 6]], [3, 1])
, Rule([[0, 1, 2], [3, 1, 4], [3, 5, 4]], [5, 1])
, Rule([[0, 1, 2], [3, 2, 4], [3, 5, 4]], [2, 5])
, Rule([[0, 1, 1], [0, 2, 1]], [2, 1])
, Rule([[0, 1, 2], [0, 3, 2], [3, 4, 5]], [1, 3])
, Rule([[0, 1, 2], [0, 3, 2], [4, 2, 5]], [3, 1])
, Rule([[0, 1, 2], [3, 4, 5], [3, 6, 5], [7, 8, 9]], [4, 6])
, Rule([[0, 1, 2], [0, 3, 4], [0, 5, 2]], [1, 5])
, Rule([[0, 1, 2], [0, 3, 2], [4, 0, 5]], [1, 3])
, Rule([[0, 1, 2], [3, 4, 5], [3, 6, 5], [7, 3, 8]], [4, 6])
]

All rules produced so far are cancellativity, but some with extra junk. I am not sure why it is not removed

[Daniel Weber]

There was a bug with equality of rules, I have a fixed version on my computer, I'll try to run it

[Daniel Weber]

On 125, though? There are no open implications involving it

[Bernhard Reinke]

Yes, in my construction the squares (or equivalently, a) satisfy 125 (and the idempotent law)

[Bernhard Reinke]

So this is a sanity check that the method could work for the construction for 1323

[Daniel Weber]

It produced a conjectured rule set of size 87, but it can't prove any of it

[Bernhard Reinke]

Interesting! Could you please share the rule set?

[Bernhard Reinke]

Also, did you include the idempotent law? Does it change the size of the rule set drastically?

[Daniel Weber]

it includes the idempotent law, yes. I haven't tried without it

[Rule([[0, 1, 2], [0, 1, 3]], [2, 3]), Rule([[0, 1, 2], [2, 0, 3]], [0, 3, 1]), Rule([[0, 1, 2]], [0, 0, 0]), Rule([[0, 1, 2]], [1, 1, 1]), Rule([[0, 1, 2]], [2, 2, 2]), Rule([[0, 1, 1]], [1, 0, 1]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4]], [1, 4, 2]), Rule([[0, 1, 2], [3, 1, 4], [3, 2, 4], [3, 4, 1]], [3, 0]), Rule([[0, 1, 2], [3, 0, 4], [5, 1, 2], [5, 3, 3]], [3, 4]), Rule([[0, 1, 2], [0, 3, 2]], [3, 1]), Rule([[0, 1, 2], [0, 2, 3]], [3, 0, 1]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 0]], [2, 1, 3]), Rule([[0, 1, 2], [2, 3, 4], [3, 2, 0], [4, 2, 5]], [0, 5, 1]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3]], [2, 0, 4]), Rule([[0, 1, 2], [3, 0, 1]], [0, 2, 3]), Rule([[0, 1, 2], [3, 1, 2], [4, 3, 3]], [0, 4, 0]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 0]], [4, 2, 5]), Rule([[0, 1, 2], [1, 0, 3], [3, 4, 0], [4, 3, 0]], [3, 2]), Rule([[0, 1, 2], [2, 3, 0], [3, 2, 0]], [1, 0, 2]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 1, 3]], [2, 1, 0]), Rule([[0, 1, 2], [1, 0, 3], [3, 4, 5], [4, 3, 1], [5, 3, 6]], [1, 2, 6]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 0, 1], [4, 1, 3]], [3, 2, 1]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 1, 3], [5, 0, 1]], [2, 5, 1]), Rule([[0, 1, 2], [2, 3, 1], [3, 2, 1]], [1, 0, 2]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [5, 2, 0]], [2, 4, 5]), Rule([[0, 1, 2], [1, 3, 4], [2, 4, 0], [4, 1, 0], [4, 3, 1]], [2, 0]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 2], [2, 5, 0], [5, 2, 1]], [3, 4, 0]), Rule([[0, 1, 2], [0, 3, 4], [1, 3, 5], [2, 6, 7], [5, 1, 0], [6, 2, 0]], [7, 2, 4]), Rule([[0, 1, 2], [1, 0, 3], [3, 2, 4], [3, 5, 0], [5, 3, 4], [6, 2, 0], [6, 5, 5]], [3, 1]), Rule([[0, 1, 2], [1, 3, 2], [2, 4, 3], [4, 2, 0], [5, 3, 3]], [0, 5, 3]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 2], [2, 5, 0], [4, 0, 6], [5, 2, 1]], [4, 6, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 3, 0], [3, 5, 0]], [4, 5, 2]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 1, 3], [5, 0, 1]], [2, 3, 5]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [1, 5, 2], [2, 3, 0], [3, 5, 0]], [1, 4, 1]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 6], [5, 2, 0]], [6, 2, 4]), Rule([[0, 1, 2], [1, 0, 3], [2, 3, 4], [3, 2, 0], [4, 3, 2]], [2, 1, 0]), Rule([[0, 1, 2], [0, 3, 4], [2, 5, 3], [3, 0, 2], [5, 1, 3], [5, 2, 0]], [4, 3, 0]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 6], [5, 2, 0], [6, 7, 2]], [4, 6, 7]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 5, 6], [4, 7, 1], [7, 4, 6]], [2, 4, 5]), Rule([[0, 1, 2], [1, 0, 3], [2, 3, 0], [3, 5, 0], [4, 5, 2]], [0, 3, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 6], [5, 2, 0], [6, 0, 2]], [4, 1, 6]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 5, 1], [5, 4, 3]], [3, 2, 1]), Rule([[0, 1, 2], [1, 3, 4], [1, 5, 0], [5, 1, 4]], [2, 1, 3]), Rule([[0, 1, 2], [1, 0, 3], [1, 4, 2], [3, 4, 1]], [3, 1]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 4], [3, 0, 2], [4, 2, 0], [4, 4, 4]], [0, 4, 0]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [5, 1, 6], [5, 4, 3], [5, 6, 4]], [3, 0, 2]), Rule([[0, 1, 2], [1, 0, 3], [2, 4, 3], [3, 0, 4], [3, 4, 2]], [0, 3, 4]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 1, 5], [4, 6, 1], [6, 4, 5]], [2, 3, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 6], [2, 5, 1], [5, 5, 3], [6, 1, 0], [6, 2, 5]], [6, 4, 4]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 5, 1], [5, 4, 3]], [3, 0, 2]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [5, 0, 4], [5, 1, 0], [5, 4, 3]], [2, 3, 5]), Rule([[0, 1, 2], [0, 3, 4], [2, 0, 5], [3, 0, 2], [3, 1, 0], [3, 3, 3], [5, 0, 3]], [2, 4, 4]), Rule([[0, 1, 2], [1, 0, 3], [3, 0, 1], [4, 1, 5], [4, 5, 0]], [5, 2, 0]), Rule([[0, 1, 2], [0, 3, 4], [2, 0, 5], [3, 0, 2], [3, 1, 0], [3, 3, 3], [5, 0, 3]], [4, 2, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 1], [5, 2, 0]], [3, 1, 4]), Rule([[0, 1, 2], [2, 0, 3], [3, 0, 4], [4, 0, 2], [4, 1, 0]], [0, 4, 2]), Rule([[0, 1, 2], [1, 3, 0], [3, 1, 4], [4, 1, 5], [4, 6, 1], [6, 4, 5]], [2, 6, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 1], [5, 2, 0]], [1, 4, 0]), Rule([[0, 1, 2], [0, 2, 3], [2, 0, 4], [4, 0, 2], [5, 1, 0]], [3, 5, 0]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [4, 0, 5], [5, 6, 1], [6, 5, 4]], [5, 4, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 1], [3, 6, 1], [5, 2, 0]], [4, 3, 6]), Rule([[0, 1, 2], [1, 3, 4], [3, 0, 4], [3, 1, 5], [4, 0, 3], [5, 4, 3]], [4, 2, 0]), Rule([[0, 1, 2], [2, 3, 0], [3, 2, 5], [4, 5, 6], [5, 1, 6], [5, 4, 2]], [5, 0]), Rule([[0, 1, 2], [0, 2, 3], [2, 0, 4], [4, 0, 2], [5, 1, 0]], [3, 4, 5]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 3, 0], [3, 5, 0], [5, 2, 6]], [5, 6, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 1], [3, 2, 1], [5, 2, 0]], [4, 5, 3]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [4, 0, 5], [5, 6, 1], [6, 5, 4]], [4, 3, 0]), Rule([[0, 1, 2], [0, 2, 3], [2, 4, 0], [4, 2, 5], [5, 2, 4]], [1, 3, 2]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 0], [3, 2, 0]], [4, 5, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [1, 5, 2], [3, 6, 0], [6, 3, 1]], [4, 5, 0]), Rule([[0, 1, 2], [0, 2, 3], [2, 4, 0], [4, 2, 5], [5, 0, 2]], [3, 1, 5]), Rule([[0, 1, 2], [1, 3, 4], [3, 0, 4], [3, 1, 5], [4, 0, 3], [5, 4, 3]], [2, 3, 0]), Rule([[0, 1, 2], [1, 0, 4], [2, 4, 1], [3, 4, 5], [4, 2, 3], [4, 6, 1]], [5, 6, 2]), Rule([[0, 1, 2], [1, 0, 3], [4, 0, 2], [4, 2, 3], [4, 3, 1]], [0, 3, 2]), Rule([[0, 1, 2], [0, 3, 4], [0, 4, 5], [1, 0, 4], [2, 4, 0], [4, 3, 0]], [2, 5, 0]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 3], [2, 3, 1], [3, 2, 0], [5, 1, 0]], [1, 2, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 3], [2, 3, 1], [3, 2, 0], [5, 1, 0]], [2, 4, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 3], [2, 3, 1], [3, 2, 0], [5, 1, 0]], [2, 0, 4]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 4], [2, 4, 0], [4, 3, 0]], [2, 0]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [4, 0, 5], [5, 6, 1], [6, 5, 4]], [1, 5, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 3], [2, 3, 1], [3, 2, 0], [5, 1, 0]], [0, 4, 1]), Rule([[0, 1, 2], [1, 0, 4], [2, 6, 4], [3, 4, 5], [4, 0, 6], [6, 2, 0]], [3, 6, 5]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [4, 0, 5], [5, 6, 1], [6, 5, 4]], [5, 3, 6]), Rule([[0, 1, 2], [0, 3, 4], [1, 5, 2], [2, 6, 0], [5, 0, 2], [6, 2, 5]], [1, 3, 4]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [4, 0, 5], [5, 6, 1], [6, 5, 4]], [3, 1, 4]), Rule([[0, 1, 2], [0, 2, 3], [1, 4, 5], [2, 6, 0], [4, 0, 2], [6, 2, 4]], [1, 5, 3]), Rule([[0, 1, 2], [0, 3, 4], [1, 0, 3], [2, 5, 0], [3, 2, 0], [5, 3, 6]], [5, 6, 4])]

[Bernhard Reinke]

Daniel Weber said:

There was a bug with equality of rules, I have a fixed version on my computer, I'll try to run it

I would be interested in the fixed version, do you mind creating a PR for the fix?

[Sebastian Flor]

It looks like if the diagonal/squaring is not completely constant, but possesses exactly one exception, then no magma at all fullfills law 1323. It's admittedly a very small insight. I hope I made no mistakes:
Magma1323.pdf
Magma1323.tex

[Daniel Weber]

Bernhard Reinke said:

I would be interested in the fixed version, do you mind creating a PR for the fix?

I made equational#731

[Terence Tao]

@Sebastian Flor It's a long shot, but analyzing models in which squaring takes only two values (call them +1 and -1, say) might be a useful ansatz.

[Sebastian Flor]

Terence Tao schrieb:

Sebastian Flor It's a long shot, but analyzing models in which squaring takes only two values (call them +1 and -1, say) might be a useful ansatz.

Sorry for my late response, I'll check this out in the next few days! Interestingly it looks like the positive and negative units of certain well-known number systems follow magma 1323 and even possess only two different diagonal elements. For example entire numbers ([[0,1],[1,0]]), with the units 1,-1 or complex numbers ([[0,1,2,3],[1,0,3,2], [2,3,1,0], [3,2,0,1]]) with the units 1,-1,i,-i. On a quick first glance (but I didn't check fully, so please be cautious with this claim!), quaternions, oktonions and sedenions also follow this law if we take the relations between their positive and negative unit elements. I'll check this out too, maybe there's something useful to find there.

[Bernhard Reinke]

I thought a bit about a noncommutative linear appraoch to 1323 by doing an extension over $(\mathbb F_2^2, +)$. I think it might be possible, but not just with brute computation. Here is my line of attack: Let's identify $(\mathbb F_2^2, +)$ with bitwise xor (denoted $\oplus$) on $\{0,1,2,3\}$. I want to construct a (noncommutative) algebra R over a field $K$ with elements $a_{ij}, b_{ij}$ such that we have a magma structure on $R \times \{0,1,2,3\}$ via

$$(x, i) \diamond (y,j) = (a_{ij} x + b_{ij} y, i \oplus j)$$

It is possible to express 1323 in equations in the $a_{ij}, b_{ij}$, these are 16 equations (of degree 4). Under additional assumptions this can be simplified.

First, I want to impose that $(x, i) \diamond (x,j) = (x, i \oplus j)$. This is equivalent to $a_{ij} + b_{ij} = 1$. In particular, $a_{ij}$ and $b_{ij}$ commute.

From this we get that $b_{00}$ has to satisfy $z^3 - z^2 +1 = 0$. Suppose this factors in $K$ and us choose two roots of this polynomial $\zeta_0, \zeta_1$ (for example, if K has characteristic 59, then we can choose $\zeta_0 = 9, \zeta_1 = 7$.) Let us suppose that $b_{00}$ actually satisfies $(z - \zeta_0) (z -\zeta_1) = 0$

Let us now suppose that $b_{0i}, b_{i0}, b_{ii}$ all commute (also with different j). Each of the $b_{ii}$ satisfy a quadratic equation over $b_{00}$, and we can write $b_{i0}$ and $b_{0i}$ as polynomials in $b_{00}$ and $b_{ii}$. In particular, the commutative subalgebra of R generated by all these has dimension at most $16$. Let us suppose that this algebra actually has dimension 16, and is isomorphic to the direct product of 16 copies of $K$.

I managed to archive by replacing $R$ with the 16x16 matrix ring in a different ring $R'$ and letting $b_{0i}, b_{i0}, b_{ii}$ all be diagonal matrices with entries in $K$. One should think of the 16 indices as a bitvector $f_3f_2f_1f_0$, where $f_0$ decides whether $b_{00}$ acts as $\zeta_0$ or $\zeta_1$, and $f_i$ determines the choice of $b_{ii}$.

Now we have to deal with $b_{ij}, (i,j > 0)$, now a 16 x 16 matrix in $R'$. We can impose further symmetry conditions to only deal with $b_{12}$: If $p \in Sym(3)$, consider the 16 x 16 permutation P matrix associated to $f_3f_2f_1f_0 \mapsto f_{p(3)}f_{p(2)}f_{p(1)}f_0$. Then we impose that $b_{p(i)p(j)} = P b_{ij} P^{-1}$. I think the last remaining equation is then $P b_{12} P^{-1} (1 - b_{12}) b_{01} = 1$, where $P$ is associated to the shift $1 \mapsto 2 \mapsto 3 \mapsto 1$. We want a solution to this where $b_{12}$ is not right invertible, or equivalently, $(1 - b_{12}) b_{01} P b_{12} P^{-1} \not= 1$. Note that $P$ is a permutation matrix (of order three) that does not commute with $b_{01}$. I am curious to see whether one can construct a possible $b_{12}$ out of this.

I have explicit matrices for $K = \mathbf F_{59}$ if someone wants them, but I should probably clean up my code a little bit before.

I think the construction does not work if we impose $b_{00} = \zeta_0$, but I cannot give a conceptional reason for this yet. On the other hand, I believe one could remove the condition $(b_{00} - \zeta_0) (b_{00} -\zeta_1) = 0$ and instead work with some 24 x 24 matrices.

[Bernhard Reinke]

Hm, I did the condition $b_{00} = \zeta_0$ in a lower characteristic, maybe it could also work

[Bernhard Reinke]

I checked again, $b_{00} = \zeta_0$ does not work. But I do not fully understand it, I think we do not want that $b_{00}$ is in the center of $R$.

[Bernhard Reinke]

Hm, I think this construction with my symmetry constrains cannot work (at least for $K = \mathbf F_{59}$). At the moment, $b_{00}$ is fixed by the permutation action. This implies for $1 \leq i \leq 16$, the i-th diagonal entry of $P b_{01} P^{-1}$ takes only two values. So we have that $((P b_{01} P^{-1}) - b_{01}) ((P^{-1} b_{01} P) - b_{01}) ((P b_{01} P^{-1}) - (P^{-1} b_{01} P))$ vanishes. This seems to imply that $b_{12}$ is in fact right-invertible.

Maybe it makes sense to look at a base field $K$ where $x^3 - x^2 + 1$ doesn't split and impose symmetry on the $b_{ij}$ using the Galois action

[Bernhard Reinke]

Hm, I think it might be better not to assume that $b_{11}$ and $b_{22}$ commute.

I think the following algebra might be of interest: we take 8 generators p, q, i, a, b, s, t, x. We will later set b00 = x, b01 = s, b12 = b, a12 = a. We have the following relations

1. p^3 = p*q = q*p = 1. The conjugation by p should correspond to the index shift 1 -> 2 -> 3 -> 1.
2. x^3-x^2+1 = s^2-x^2*s+x*s-s-x^2+x-1 = s*x-x*s = 0. These relations make sure that the subalgebra generated by b00, b01 is commutative and we have the law 1323 satisfied on the submagma $R \times \{0,1\}$
3. s*t = t*s = 1: b01 is invertible with inverse t.
4. a + b = 1: This is the assumption that a12 + b12 = 1
5. p*b*q*a*s=1: This is the law b23 * a12 * b01 = 1.
6. p*x*q = x, i*x*i = x, i*i = 1, i*s*i = s, i*p*i=q. Conjugation by p should fix b00. we also introduce i that should correspond to the index swap 2 <-> 3. We want that i keeps b00 and b01 fixed, and we have (2,3)(1,2,3)(2,3) = (1,3,2).

We can define b10 and b11 in terms of b and s, and then define bij by the appropriate conjugations with p,q,i.

Attached is a Singular file using the letterplace subsystem, where this algebra is defined and the aij and bij are defined in terms of the algebra generators. We can check that this indeed satisfies 1323.

Edit: I forgot a relation in my enumeration (it was included in the file), it is a + b = 1.

Unfortunately, letterplace always works with a degree bound, so we cannot show directly with this computation that 2744 does not hold. But this algebra seems promising!
linear_1323_approach.sing

[Bernhard Reinke]

the algebra in the file works with characteristic 2, but I think every characteristic other than 5 should be more or less the same. In characteristic 5 my definition of b11 doesn't work

[Terence Tao]

Looks computationally tricky, but this may be the one approach that isn't blocked by all the "immunities" we know that the problem has. In particular do your models have non-surjective squaring? We know that is an essential ingredient for any counterexample.

[Bernhard Reinke]

Yes, all squares are in $R \times {0}$. I think the point is that if we use $\mathbf F_2^2$ instead of $\mathbf F_2$ as our base magma, we can have two different classes of non-squares interact with each other.

[Pace Nielsen]

@Bernhard Reinke For the past week I've been trying something similar. Here is what I've discovered so far.

First, let me set some notation (following ideas from you, Terry, and others). Let $(M,\ast)$ be an arbitrary magma (usually) satisfying some fixed identity/law, and fix some algebra $A$ with operations $\diamond_{m,n}$ indexed by pairs $(m,n)\in M$. We choose this algebra so that we believe we have some control/understanding of its behavior. We can attempt a decoupling procedure by defining a magma whose carrier set is $A\times M$ subject to the operation

$$(x,m)\diamond (y,n)=(x\diamond_{m,n}y,m\ast n).$$

Forcing this operation to also satisfy the fixed identity puts constraints on the $\diamond_{m,n}$ operations. But the hope is that the constraints are weak enough that we can avoid satisfying certain new identities.

The simplest kinds of algebras and operations seem to follow the linear ansatz over rings, so that's what I mainly worked with (as you are also doing!). So I took $x\diamond_{m,n}y:=a_{m,n}x+b_{m,n}y$, with the $a_{m,n},b_{m,n}$ in a ring.

I started with law 1485, using for $(M,\ast)$ the 2-element magma that does not satisfy the central groupoid law. I thought that in this way I could decouple the linearity from that law. Unfortunately, the new ring relations in the eight variables satisfy the laws we are trying to avoid.

Next I tried law 1516, using a 7-element linear magma for $(M,\ast)$, using Terry's projective ansatz. This led to 9 new functions, and so 18 new variables. After some Grobner basis type computations, it turned out that once again they always satisfied law 255. (It took about 40 steps of refining the reduction system to get the needed relation.)

If we consider your system in an arbitrary ring, there would be 32 variables. If you wish, I can run the check to see if the relations we want to avoid pop up quickly or not.

[Terence Tao]

Remarkable how tough these last few implications are, that they can defeat even quite sophisticated ansatzes!

[Bernhard Reinke]

@Pace Nielsen that sounds interesting! Are you doing your Gröbner basis computations in noncommutative rings or in commutative ones? I think if we do this construction with matrices over a commutative ring, we still have the rule that left multiplication being surjective implies that the left multiplication is injective. So we really need to use a noncommutative base ring for 1323, as 2744 is equivalent to left multiplication being injective.

[Bernhard Reinke]

Hm, it seems that it doesn't hurt too much to assume that $b_{00}$ commutes in fact with everything. We can even assume that $b_{00}$ belongs to our base field (for example $x = 7$ for $K = \mathbb F_{59}$. In this case $s$ is quadratic over the base field. If we only consider the relations in p, q, i, s, t, x, we get a nice finite Gröbner basis. So all the complexity is really in p*b*q*a*s=1

[Pace Nielsen]

The computations allow for noncommutativity. I've started the process and will run it over night and let you know what it finds.

So far the computations look much better than in the two cases I considered, because the target equation 2744 has so many of its own relations that need to hold.

I very much doubt that my process will terminate, so you should keep doing what you are doing!

[Pace Nielsen]

@Bernhard Reinke There are 32 relations that we want to avoid in order for 2744 to fail. After 170 steps so far, 14 of those 32 relations are now holding. Fortunately, they are all of a special form: when put in shortlex form, the leading variable has a zero in its subscript. The other 18 non-special forms have not been adjoined, such as the 2744 relation $a_{1,1}b_{0,1}b_{1,0}=1$.

Other than needing to invert 2 a couple times, the computations work in arbitrary characteristic. For example, the 19th step added the relation $a_{0,0}^2b_{0,0}=(-1/2)(b_{0,0}+a_{0,0}^3)$. Note that this is really the special 2744 relation $a_{0,0}b_{0,0}a_{0,0}=-b_{0,0}-a_{0,0}^{3}-a_{0,0}^2b_{0,0}$ after using the fact that $a_{0,0}$ and $b_{0,0}$ must commute (found at step 12).

The reason this process has only found 170 relations so far is to avoid an explosion of relations (there are literally hundreds of them found at every step, some of very large degree). The program just adjoins the one with the best shortlex considerations, and then reruns the computation to find new relations. I could definitely speed up this process by a significant amount; I've just never needed to worry too much about this issue previously in my own endeavors.

Other interesting observations: The first 15 relations adjoined were the only ones of degree 2 found so far, and were mostly commuting relations (such as the one mentioned above), but also some shift-commuting relations like $b_{2,1}a_{3,2}=a_{3,0}b_{0,0}$. At step 99, it adjoined a relation of the form $a_{0,0}^4=...$. On step 134 it started adjoining relations of degree 5, and so it may be a while before I see new short relations (if any).

[Bernhard Reinke]

Bernhard Reinke said:

Hm, it seems that it doesn't hurt too much to assume that $b_{00}$ commutes in fact with everything. We can even assume that $b_{00}$ belongs to our base field (for example $x = 7$ for $K = \mathbb F_{59}$. In this case $s$ is quadratic over the base field. If we only consider the relations in p, q, i, s, t, x, we get a nice finite Gröbner basis. So all the complexity is really in p*b*q*a*s=1

There is one more transformation I can do in this line of attack: We can write s as a linear combination of x and an idempotent e. We can think of the subalgebra generated by p,q,i,e as the monoid algebra for the monoid $\langle Sym(3), e | e^2 = e, (23)e = e(23) \rangle.$ This monoid is relatively nice, it has a complete rewriting system, I think it is related to the Coxeter Monoid of the $(2,3,\infty)$ triangle group, here we replace only one reflection by an idempotent.

With this, the additional equation for b reads like bqb - bq + c_1 * qe + c_2 * q = 0 for some constants depending on x. The Gröbner basis with b seems to be infinite, but the leading monomials seem to be a nice finite set together with 7 infinite families of the form v (pe)^n wor v (qe)^n w. The actual relations are rather large. But maybe one already try to argue that the standard monomials are indeed independent?

[Jose Brox]

I think we can use a Kisielewicz ansatz for 1323 (the kind Kisielewicz used to show that its identity is an Austin law)! Denote the product on Nat to be:

• $x*x = 2^x$
• $2^x*y = 2^x3^y$ except if $y=2^x$
• $x*2^{2^x}3^x = 2^x$ except if $x=2^y$
• $2^x3^y*x = 2^x3^y5^x$
• $x*2^x3^y5^x = y$
• $x*y = 7^x11^y$ otherwise.

Then, for Equation 1323 we have
$y*(((y*y)*x)*y) = y*((2^y*x)*y) = y*(2^y3^x*y) = y*2^y3^x5^y = x$
unless $x=2^y$, in which case
$y*(((y*y)*2^y)*y) = y*((2^y*2^y)*y) = y*(2^{2^y}*y) = y*2^{2^y}3^y = 2^y = x.$

On the other hand, for Equation 2744 in the generic case we have:
$((y*y)*(y*x))*y = (2^y*7^y11^x)*y = 2^y3^{7^y11^x}*y = 2^y3^{7^y11^x}5^y\neq x.$

Is this sound?

[Pace Nielsen]

@Jose Brox Your fifth rule needs an exception when $y$ is a power of 2 (to handle the second rule). But then the last equality in your first string of equalities fails when $y$ is a power of 2..

I like this thinking. Hopefully it can be fixed up.

[Pace Nielsen]

I have meetings for the next couple of hours, but I'll give it some thought.

[Bernhard Reinke]

@Jose Brox This is an interesting approach! One tricky thing is that left-multiplication with a x*x, so in your setting with $2^x$, has to be a bijection. I am not sure how easy it is to adjust your construction so that this holds

[Jose Brox]

After the important insights by @Pace Nielsen and @Bernhard Reinke , the idea needs improvement. Part of the problem can be solved by changing the operation precedence, so that $x\cdot 2^x3^y5^x = y$ even if $x$ is a power of 2, and then adding more rules, but an important blockade is the following: from 1323 we can get 2744 $(x,y^2)$, since by introducing
$((y^2y^2)(y^2 x))y^2$ instead of $x$, we arrive at
$((y^2y^2)(y^2x))y^2 = x.$
So we need a more complex set of operations, I will think about it when I have the time.
Perhaps this 2744 $(x,y^2)$ is useful for something? In particular, if squaring is surjective, then 1323 implies 2744.

Note that we also get
$y(xy) = ((y^2y^2)x)y^2,$
which may be useful too.

[Jose Brox]

After playing with Prover9, it seems that a 1323 magma which is unital does not necessarily satisfy 2744. This inspires the following simplification of the problem: the two equations
$(y^2x)y^2 = x \,\, (a), \quad xy^2 = y(xy) \,\, (b)$
together imply 1323 (and are implied by 1323 plus the identity element). We also get $x^2x^2=1$, etc.
Then I think we can build a 1323 unital Kisielewicz model which does not satisfy 2744, along the following lines:

• $1*x = x = x*1$
• $x*x = 2^x$
• $2^x*2^x = 1$
• $2^x*2^y = 5^x7^y$ (except if $x=y$)
• $2^x*y = 2^x3^y = y*2^x$ (except when y is a power of $2$)
• $2^x*(5^y7^x ) = 2^y$
• $(5^x7^y)*2^x = 2^y$
• $2^y*(2^y3^x) = x = (2^y3^x)*2^y$
• $x*y = 11^x13^y$ otherwise.
  I got without time today and haven't checked this much, but I prefer just to send it to you and see if you spot fixable mistakes or can build upon this to get the solution (@Pace Nielsen you may be interested!). :working_on_it: :grinning_face_with_smiling_eyes:

[Michael Bucko]

Tested Equation1323_implies_Equation2744 with Duper (it proved a bunch of other theorems already).

• Reached 1,000,000 heartbeats: no result.
• I'm going to run it with 10,000,000 heartbeats, and share the result here.

[Michael Bucko]

• Ran Duper with 10,000,000 heartbeats (ca 15 minutes). No result. It'd be great to run it with 1,000,000,000 heartbeats, but I guess we'd need a better infrastructure for that.

[Mario Carneiro]

if you raise the resource limits too much you can cause your computer to run out of memory or crash

[Daniel Weber]

Jose Brox said:

After playing with Prover9, it seems that a 1323 magma which is unital does not necessarily satisfy 2744. This inspires the following simplification of the problem: the two equations
$(y^2x)y^2 = x \,\, (a), \quad xy^2 = y(xy) \,\, (b)$
together imply 1323 (and are implied by 1323 plus the identity element). We also get $x^2x^2=1$, etc.
Then I think we can build a 1323 unital Kisielewicz model which does not satisfy 2744, along the following lines:

• $1*x = x = x*1$
• $x*x = 2^x$
• $2^x*2^x = 1$
• $2^x*2^y = 5^x7^y$ (except if $x=y$)
• $2^x*y = 2^x3^y = y*2^x$ (except when y is a power of $2$)
• $2^x*(5^y7^x ) = 2^y$
• $(5^x7^y)*2^x = 2^y$
• $2^y*(2^y3^x) = x = (2^y3^x)*2^y$
• $x*y = 11^x13^y$ otherwise.
  I got without time today and haven't checked this much, but I prefer just to send it to you and see if you spot fixable mistakes or can build upon this to get the solution (Pace Nielsen you may be interested!). :working_on_it: :grinning_face_with_smiling_eyes:

I'll try to run the greedy algorithm on that, it might work

[Michael Bucko]

(made a mistake, correcting the script)

[Michael Bucko]

I thought I solved it, but then I realized I had made an error in the script.

The current implication check is this:

fof(declare_operations, axiom,
    ! [X, Y] : ( f(X, Y) = f(Y, X) )
).

fof(unitality, axiom,
    ! [X] : ( f(1, X) = X & f(X, 1) = X )
).

fof(multiplication_rules, axiom,
    ! [X, Y] : (
        (X = Y => f(X, Y) = mul(2, X)) &
        (f(mul(2, X), mul(2, X)) = 1) &
        (X != Y => f(mul(2, X), mul(2, Y)) = mul(5, mul(X, 7))) &
        (Y != 2 => f(mul(2, X), Y) = mul(2, mul(X, 3))) &
        (f(mul(2, X), f(mul(5, Y), mul(7, X))) = mul(2, Y)) &
        (f(f(mul(5, X), mul(7, Y)), mul(2, X)) = mul(2, Y)) &
        (f(mul(2, Y), f(mul(2, Y), mul(3, X))) = X) &
        (f(f(mul(2, Y), mul(3, X)), mul(2, Y)) = X)
    )
).

fof(equation_1323, axiom,
    ! [X, Y] : (X = f(f(Y, f(f(Y, Y), X)), Y))
).

fof(equation_2744, axiom,
    ! [X, Y] : (X = f(f(f(Y, Y), f(Y, X)), Y))
).

fof(implication_check, conjecture,
    ~(
        ! [X, Y] : (
            (X = f(f(Y, f(f(Y, Y), X)), Y)) =>
            (X = f(f(f(Y, Y), f(Y, X)), Y))
        )
    )
).

[Michael Bucko]

Maybe it actually worked. If I read it correctly (and if the multiplication rule constraints are okay..), then 1323 should not imply 2744.
output1

[Bernhard Reinke]

Jose Brox said:

After playing with Prover9, it seems that a 1323 magma which is unital does not necessarily satisfy 2744. This inspires the following simplification of the problem: the two equations
$(y^2x)y^2 = x \,\, (a), \quad xy^2 = y(xy) \,\, (b)$
together imply 1323 (and are implied by 1323 plus the identity element). We also get $x^2x^2=1$, etc.
Then I think we can build a 1323 unital Kisielewicz model which does not satisfy 2744, along the following lines:

• $1*x = x = x*1$
• $x*x = 2^x$
• $2^x*2^x = 1$
• $2^x*2^y = 5^x7^y$ (except if $x=y$)
• $2^x*y = 2^x3^y = y*2^x$ (except when y is a power of $2$)
• $2^x*(5^y7^x ) = 2^y$
• $(5^x7^y)*2^x = 2^y$
• $2^y*(2^y3^x) = x = (2^y3^x)*2^y$
• $x*y = 11^x13^y$ otherwise.
  I got without time today and haven't checked this much, but I prefer just to send it to you and see if you spot fixable mistakes or can build upon this to get the solution (Pace Nielsen you may be interested!). :working_on_it: :grinning_face_with_smiling_eyes:

I like this approach! I think your formulas still run into the issue that left multiplication with 2^x has to be a bijection. I tried to see whether one can combine this approach with the matrix linear one, but it seems that this is not the case. There are "Matrix linear" models in characteristic 2, but for the ground magmas F_2and F^2_2, they all satisfy 2744 as well.

On the other hand, it seems that it is still possible to find an example that admits a magma homomorphism to $(\mathbf F_2, + )$, where squares are sent to 0. In particular, under these assumptions, the squares satisfy (y*x)*y = x, so a Putnam law.

[Bernhard Reinke]

Michael Bucko said:

Maybe it actually worked. If I read it correctly (and if the multiplication rule constraints are okay..), then 1323 should not imply 2744.
output1

I think you do not want your implication_check to be the conjecture, but you should remove it and have equation_2744 as the conjecture.

[Jose Brox]

Jose Brox ha dicho:

After playing with Prover9, it seems that a 1323 magma which is unital does not necessarily satisfy 2744. This inspires the following simplification of the problem: the two equations
$(y^2x)y^2 = x \,\, (a), \quad xy^2 = y(xy) \,\, (b)$
together imply 1323 (and are implied by 1323 plus the identity element). We also get $x^2x^2=1$, etc.
Then I think we can build a 1323 unital Kisielewicz model which does not satisfy 2744, along the following lines:

• $1*x = x = x*1$
• $x*x = 2^x$
• $2^x*2^x = 1$
• $2^x*2^y = 5^x7^y$ (except if $x=y$)
• $2^x*y = 2^x3^y = y*2^x$ (except when y is a power of $2$)
• $2^x*(5^y7^x ) = 2^y$
• $(5^x7^y)*2^x = 2^y$
• $2^y*(2^y3^x) = x = (2^y3^x)*2^y$
• $x*y = 11^x13^y$ otherwise.
  I got without time today and haven't checked this much, but I prefer just to send it to you and see if you spot fixable mistakes or can build upon this to get the solution (Pace Nielsen you may be interested!). :working_on_it: :grinning_face_with_smiling_eyes:

In my hurry I forgot to add the condition enforcing $y(xy) = xy^2$ in the generic case: we also need
$y*11^x13^y = 2^y3^x$ (there may be more conditions missing).

[Michael Bucko]

Bernhard Reinke schrieb:

I think you do not want your implication_check to be the conjecture, but you should remove it and have equation_2744 as the conjecture.

Made the adjustment and got a refutation from Vampire 4.9. Now equation_2744 is the conjecture.

fof(declare_operations, axiom,
    ! [X, Y] : ( f(X, Y) = f(Y, X) )
).

fof(unitality, axiom,
    ! [X] : ( f(1, X) = X & f(X, 1) = X )
).

fof(multiplication_rules, axiom,
    ! [X, Y] : (
        (X = Y => f(X, Y) = mul(2, X)) &
        (f(mul(2, X), mul(2, X)) = 1) &
        (X != Y => f(mul(2, X), mul(2, Y)) = mul(5, mul(X, 7))) &
        (Y != 2 => f(mul(2, X), Y) = mul(2, mul(X, 3))) &
        (f(mul(2, X), f(mul(5, Y), mul(7, X))) = mul(2, Y)) &
        (f(f(mul(5, X), mul(7, Y)), mul(2, X)) = mul(2, Y)) &
        (f(mul(2, Y), f(mul(2, Y), mul(3, X))) = X) &
        (f(f(mul(2, Y), mul(3, X)), mul(2, Y)) = X)
    )
).

fof(equation_1323, axiom,
    ! [X, Y] : (X = f(f(Y, f(f(Y, Y), X)), Y))
).

fof(equation_2744, conjecture,
    ! [X, Y] : (X = f(f(f(Y, Y), f(Y, X)), Y))
).

[Amir Livne Bar-on]

I think that if the operation is commutative, the multiplication maps $L_y$ are bijections, so 2744 follows from 1323. But commutativity isn't listed as one of the immunities, maybe I missed something?

[Bernhard Reinke]

I think you are right, should I edit the post at the beginning?

[Amir Livne Bar-on]

Yes, maybe we should. But this was triggered by Michael's result above, that has commutativity as an axiom.

[Jose Brox]

From my Prover9 playing, I think that one thing we can do is to impose "partial commutativity" $y^2x = xy^2$ without implying 2744. Other seemingly valid simplifications are x^4 = 1 for all the definitions of powers (but x^3 = 1 forces 2744).

[Bernhard Reinke]

I just had the same idea @Jose Brox :)

I think we then get on the squares a nice "design" structure: If we assume that the squares commute and satisfy 14, then we have for squares xy = z => yz = x. By commutativity we then get that xy = z, yx = z, xz = y, zx = y, yz = x, zy = x are all equivalent. If we further consider the impose that xx = 1for squares, we see that this implies (a) and (b) on squares.

So if we have a set Xtogether with a collection $E \subset P(X)$ of three element subsets, such that every pair $x \not= y$ is in a unique three element of $E$, then we can define a magma on $X \sqcup 1$ with 1 acting unital and $x \diamond y = z$ if $\{x,y,z\} \in E$ and $x \diamond x = 1$. This would nicely define the structure on the squares and I think the greedy algorithm easily can do this.

I am curious to extend this interpretation to the nonsquares. I think (a) can be again thought as a hypergraph condition, but in (b) we need to be more careful.

[Bernhard Reinke]

Also, I think we cannot impose that squaring is injective on nonsquares. xx = yy => x = y | xx = 1 together with the standing assumptions already implies 2744

[Bernhard Reinke]

(ups, I wanted to edit my original message)

[Daniel Weber]

The greedy construction gives a weird result, Vampire claims to find a counterexample but my code can't find a problem in it

[Bernhard Reinke]

Jose Brox said:

From my Prover9 playing, I think that one thing we can do is to impose "partial commutativity" $y^2x = xy^2$ without implying 2744. Other seemingly valid simplifications are x^4 = 1 for all the definitions of powers (but x^3 = 1 forces 2744).

I think it is possible to have a surjection onto $(\mathbf Z / 4 \mathbf Z, + )$ such that every one-generated submagma is is either trivial, or isomorphic to $(\mathbf Z / 2 \mathbf Z , + )$ or to $(\mathbf Z / 4 \mathbf Z , + )$. This is a little bit stronger than x^4 = 1 . I think we can also impose that x^3 is a magma automorphism.

[Bernhard Reinke]

I think this setting might be more approachable for the "Matrix Greedy" approach than this one.

My line of thought gives the following construction: We want to consider a set $X$ together with a base point $e \in X$. I want to define a magma on $X \times \mathbf Z / 4 \mathbf Z$ via $(x, i) \diamond (y, j) = (x \diamond_{i,j} y, i+j)$.
In this construction, the set of squares will be $(e,0) \sqcup X \times 2$, but $X \times 0$ will also share many properties of the squares.

I think we can impose the following:

1. $x \diamond_{i,j} y = y \diamond_{j,i} x$ unless $\{i,j\} = \{1,3\}$ (this is a stronger partial commutativity then just commutativity of squares.
2. $x \diamond_{i,j} y = x \diamond_{-i,-j} y$ (this will correspond to x^3 being an automorphism)
3. If $i$ is even, then $(y \diamond_{i,j} x) \diamond_{i+j,i} y = x$ (this is a rule (a) but now $X \times \{0, 2\}$ takes the role of the squares.
4. $e \diamond_{0,j} y = y \diamond_{j,0} e = y$: (e,0) is unital.
5. $x \diamond_{i,j} x = 1$ for $(i,j) = (0,0), (1,3), (2,2), (3,1)$ (this is basically x^4 = 1 in all ways)
6. $x \diamond_{i,j} x = x$ for $(i,j) = (1,1), (1,2), (2,1), (2,3), (3,3)$ (this is also x^4 = 1) (note that (0,1), (0,3) are in neither sets)
7. $e \diamond_{2,2} y = e \diamond_{0,2} y = y \diamond_{2,2} e = y \diamond_{0,2} e = y$: (1 + 3 implies that $e \diamond_{2,2} \bullet$ is a bijection, we fix the labeling on $X \times 0$ so that it is the identity.
8. For $j$ odd, we have $x \diamond_{i,2} y = y \diamond_{j,i+j} (x \diamond_{i,j} y)$ (this is rule (b). For even j, this already follows from (a) and 4+5.

Note that by commutativity and our automorphism we really only need to consider $\diamond_{i,j}$ for $(0,0),(0,1),(0,2),(1,1),(1,2),(1,3),(2,2),(3,1)$ so we only have 8 instead of 16 relations to worry about.

The reason I am more optimistic for this is that the even parts satisfy the commutative 14 Putnam law, that should have very simple greedy properties. Of course 8 relations is a bit more than 4, but I think there is a trade off over the control over the one-generated submagmas.

[Bernhard Reinke]

Hm, I managed to encode this into a tptp file, and it seems that if we take all these assumptions, we already have 2744. But now I can investigate what to drop. Here is the tptp for those who are interested:
1323_z4_functional.p

[Michael Bucko]

Bernhard Reinke schrieb:

Hm, I managed to encode this into a tptp file, and it seems that if we take all these assumptions, we already have 2744. But now I can investigate what to drop. Here is the tptp for those who are interested:
1323_z4_functional.p

Wow! And thank you for sharing the tptp file.

[Jose Brox]

Bernhard Reinke ha dicho:

But now I can investigate what to drop.

Possibly some of the commutativity is too strong. For example if we enforce y^2x = (yx)y we get 2744.

[Bernhard Reinke]

Apparently, already (3) + (a) + (b) implies 2744. So we shouldn't treat $X \times 0$ in the same way as squares. I have the fear that this approach has the same complexity as the original problem if we just consider the magma restricted on $X \times 0$.

[Bernhard Reinke]

I think it is possible (or at least vampire doesn't directly find a contradiction) to find a magma with a surjective magma homomorphism onto $(\mathbf F^2_2, +)$ such that the preimage of 0 (containing all squares) commutes with everything and satisfies the Putnam law (so if y is in the preimage of 0, then $L_y = R_y$ is an involution). Moreover, everything in the preimages of 0 squares to the unital element. This takes care of condition (a).

Also, it seems less clear whether it is possible to identify the different preimages somehow.

[Bernhard Reinke]

Also, it seams consistent to impose that if x and y map to different elements in $\mathbf F^2_2$, then xx != yy.

[Jose Brox]

Some more ideas and negative reports:

• Identities (a) and (b) already imply the existence of an identity element (namely, any element of the form $y^2y^2$).

• Identity (a) is close to saying that left multiplication by $y^2$ is an involution, although it is actually stronger. But if we impose the existence of an identity element, then (a) together with (b) is equivalent to (b) with
  $y^2(y^2x) = x$ (a').

• Also, it is too strong to ask for $y^2x = z^2x$ (it implies 2744), but apparently it may be enough that there are two kinds of square multiplications, with one of them being the identity. Therefore we can seemingly ask for
  $y^2x = x$ or $y^2x = x^*$, where $^*$ denotes some involution.

• Recall that we can also impose $y^2x = xy^2$.

• Therefore it may be interesting to look for a model (M) in which we have
  $1*x = x = x*1$, $y^2 = 0$ or $y^2 = 1$, $0*x = x^* = x*0$, and $y(xy) = y^2x$, which equals either $x$ or $x^*$, depending on the class of $y$. Note that we have $0*0=1$ since $0*0= y^2*y^2$ for some $y$.

Since we need involutions, which we can find by piecewise linear functions over the integers (e.g. $f(x):=x+1$ if $x$ is even and $f(x):=x-1$ if $x$ is odd), I have tried to find a magma over the integers with product $x*y:=ax+by+c$ where $a,b,c$ are functions of $x,y$ (mod N). But it turns out that this piecewise linear ansatz is impossible: the conditions $x = (x^*)^*$, $0*x = x^* = x*0$ and $y(xy)\in \{x,x^*\}$ give an incompatible system already for $x=y=0$ (mod N) for any N.

But perhaps we can find another ansatz giving an (M) model!

[Bernhard Reinke]

I did some experiments with vampire, I don't think that it is possible to have a magma satisfying (a) and (b) and only having 2 squares. As 1323 => 2744 for magmas that are left-cancellative, we can impose that we have an example of failure of left-cancellation. Then vampire quickly finds a contradiction under these assumptions.

[Bernhard Reinke]

this is the tptp file I ran:

fof(a, axiom,
m(m(m(Y, Y), X), m(Y, Y)) = X
).

fof(b, axiom,
m(X, m(Y, Y)) = m(Y, m(X, Y))
).

fof(few_squares, axiom,
m(X,X) = e | m(X,X) = f
).

fof(not_left_cancellative, axiom,
m(0,1) = 3 &
m(0,2) = 3 &
1 != 2
$true
).

[Bernhard Reinke]

In fact, I think even 1323 + at most two squares => 2744 holds

[Bruno Le Floch]

Relatedly I can prove that 1729 + one identity element + at most two squares (EDIT: + a finite-orbit condition) implies 917. I suppose this can be turned into a proof of 1323 + identity + at most two squares (EDIT: + a finite-orbit condition) implies 2744. Do you use the existence of the identity? I'll try to remove it from my proof.

[Bruno Le Floch]

(EDIT: I had confused my left and my right in many places. This is the drawback of thinking in parallel about 1323 and 1729.)
Proposition: Assume that a magma obeys 1323 ($x=y\diamond((y^2\diamond x)\diamond y)$), existence of identity ($I\diamond x=x\diamond I=x$), has at most two squares ($x^2\in\{I,T\}$), and that all orbits of $R_T$ are finite. Then the magma obeys 2744 ($x = (y^2\diamond(y\diamond x))\diamond y$).

The equation can be written $L_y\circ R_y\circ L_{y^2}=\mathrm{id}$ so $L_y$ is surjective, $R_y$ is injective, and they are bijective when $y$ is a square. The equation can also be written as $L_y\circ R_y = (L_{y^2})^{-1}$. The goal is to prove that all $L_y$ (equivalently $R_y$) are bijective.

Restricted injectivity property. If $y^2 = z^2$ and $L_x(y)=L_x(z)$ then $y\diamond(x\diamond y) = L_{y^2}^{-1}(x) = L_{z^2}^{-1}(x) = z\diamond(x\diamond z)$, so that $R_{x\diamond y}(y) = R_{x\diamond y}(z)$. By injectivity of all $R_w$ we get $y=z$. Therefore, all $L_x$ restricted to a given $\sqrt{u}=\{y\mid y^2=u\}$ are injective.

In particular, if all squares are equal, then all $L_x$ are injective and we are done proving 2744. We can thus assume that $T$ is a square, so that $L_I,R_I,L_T,R_T$ are all bijective. Since $T^2\in\{I,T\}$ and must differ from $I\diamond T=T$ we get $T^2=I$. As a consequence, $(x^2)^2=I$ for all $x$, and the equation for $x=y^2$ trivializes. Another consequence is that $(L_T)^{-1} = R_T$.

For $x=T\diamond y^2=y^2\diamond T$ (namely $T,I$ when $y^2=I,T$) we have $y^2\diamond x=T$ so the equation for this $(x,y)$ gives us $y \diamond L_T(y) = T\diamond y^2$. In particular, $\{y^2,y\diamond L_T(y)\}=\{I,T\}$.

Lemma. For any $w\in M$, one has $w^2=L_T(w)^2$.
Proof. The equation $L_{y^2}\circ L_y\circ R_y=\mathrm{id}$ for $y=L_T(w)$ and applied to $w$ is

$$w = L_{L_T(w)^2} \Bigl(L_T(w) \diamond \bigl(w\diamond L_T(w)\bigr)\Bigr) = L_{L_T(w)^2}\bigl(R_{T\diamond w^2}(L_T(w))\bigr) .$$

Either $L_T(w)^2=w^2$ and we are done, or $L_T(w)^2=T\diamond w^2\in\{I,T\}$ in which case the equation is $w=L_u(R_u(L_T(w)))=L_T(w)$ for some $u\in\{I,T\}$, which contradicts $L_T(w)^2=T\diamond w^2$.

Lemma. For any $v,w\in M$ consider the sequence $x_0 = v$, $x_1 = w$, $x_{i+2} = x_i \diamond x_{i+1}$. Then for all $p\geq 0$,

$$x_{3p} = (R_{x_1^2})^p(x_0) , \qquad x_{3p+1} = (R_{x_2^2})^p(x_1) , \qquad x_{3p+2} = (R_{x_0^2})^p(x_2) .$$

Proof. First a direct calculation $x_{i+3} = x_{i+1}\diamond (x_i\diamond x_{i+1}) = L_{x_{i+1}^2}^{-1}(x_i) = R_{x_{i+1}^2}(x_i)$, where in the last equality we used that $(L_I)^{-1} = R_I$ and $(L_T)^{-1}=R_T$. Since $x_i=L_{x_{i+1}^2}(x_{i+3})\in\{x_{i+3},L_T(x_{i+3})\}$ we get $x_{i+3}^2=x_i^2$ by the previous lemma. Then a trivial induction.

Proof of the proposition. For any $v,w$, the above sequence is periodic (with period given by the gcd of the relevant $R_{x_i^2}$ orbits) so it makes sense to talk about $x_{-2},x_{-1}$. Then $w = x_{-1}\diamond v = R_v(x_{-1})$. Since this can be done for all $v,w\in M$ we learn that $R_v$ is surjective, so we are done.

[Bruno Le Floch]

I also vaguely remember an obstruction to taking all $x^2=T$ for $x\not\in\{I,T\}$, but I can no longer find it. Ignoring this possible obstruction, an Ansatz for a counterexample would be $\{I,T\}\sqcup\mathbb{Z}$ with $n^2=T$ for all $n\in\mathbb{Z}$, with $L_I=R_I=\mathrm{id}$ and $R_T(n) = n-4$, $L_T(n)=n+4$, and $L_T(T)=R_T(T)=I$. Then the equation gives $n\diamond n=T$ and $n\diamond(n-4)=I$. Then there remains the equation for $(x,y)=(m,n)\in\mathbb{Z}^2$. We want to (not-quite-)partition all other pairs $(m,n)$ into sequences of the form $x_i,i\in\mathbb{Z}$ as defined in my previous post. I'll try on Friday.

[Bernhard Reinke]

Bruno Le Floch said:

Relatedly I can prove that 1729 + one identity element + at most two squares (EDIT: + a finite-orbit condition) implies 917. I suppose this can be turned into a proof of 1323 + identity + at most two squares (EDIT: + a finite-orbit condition) implies 2744. Do you use the existence of the identity? I'll try to remove it from my proof.

No, the vampire file I use is the following:

fof(eq1323,axiom,
X = m(Y,m(m(m(Y,Y),X),Y))
).

fof(few_squares, axiom,
m(X,X) = e | m(X,X) = f
).

fof(not_left_cancellative, axiom,
m(0,1) = 3 &
m(0,2) = 3 &
1 != 2
$true
).

I only assume 1323 + two squares + existence of a failure of left cancellation. We already now that 1323 + left cancellative => 2744, so these assumptions make sense. Vampire finds a proof in ~30 seconds that 1323 + two squares + existence of a failure of left cancellation leads to a contradiction, but by heavy SAT usage. In principle we could try to convert this to a machine generated Lean proof to be extra sure about the output.

[Bernhard Reinke]

Bruno Le Floch said:

I also vaguely remember an obstruction to taking all $x^2=T$ for $x\not\in\{I,T\}$, but I can no longer find it. Ignoring this possible obstruction, an Ansatz for a counterexample would be $\{I,T\}\sqcup\mathbb{Z}$ with $n^2=T$ for all $n\in\mathbb{Z}$, with $L_I=R_I=\mathrm{id}$ and $R_T(n) = n-4$, $L_T(n)=n+4$, and $L_T(T)=R_T(T)=I$. Then the equation gives $n\diamond n=T$ and $n\diamond(n-4)=I$. Then there remains the equation for $(x,y)=(m,n)\in\mathbb{Z}^2$. We want to (not-quite-)partition all other pairs $(m,n)$ into sequences of the form $x_i,i\in\mathbb{Z}$ as defined in my previous post. I'll try on Friday.

Unfortunately, a similar vampire script rules this out as well

[Jose Brox]

Bernhard Reinke ha dicho:

I did some experiments with vampire, I don't think that it is possible to have a magma satisfying (a) and (b) and only having 2 squares. As 1323 => 2744 for magmas that are left-cancellative, we can impose that we have an example of failure of left-cancellation. Then vampire quickly finds a contradiction under these assumptions.

In Prover9 I originally imposed the non-surjectivity of squarings, and it didn't find the contradiction! I have tried now with the failure of left-cancellation, and it still cannot find the contradiction after 20 minutes :grimacing: Perhaps I'm doing something wrong, but I don't think so (I'm leaving the goals section empty, but I have checked that this works for obvious contradicitions). I have tried two slightly different schemes, I copy them below. Btw, I have verified the Vampire computation on tptp.org and it also says unsatisfiable for me.

Option 1

((y*y)*x)*(y*y) = x.
x*(y*y) = y*(x*y).
x*x = 0 | x*x = 1.
exists a (exists b (exists c (a*b = a*c & b != c))).

Option 2

((y*y)*x)*(y*y) = x.
x*(y*y) = y*(x*y).
x*x = a | x*x = b.
0*1 = 0*2.
1 != 2.

[Jose Brox]

Btw, giving Vampire 999s (on TPTP.org) it cannot rule out the possibility of (a) plus (b) and the existence of 3 squares, nor does it prove the implication of 2744. Can you double check? The existence of 3 different squares can perhaps dissolve the contradiction in the piecewise affine model I was working with, I will check.

[Ibrahim Tencer]

Here is my current line of thinking: clearly the equations are equivalent given associativity, and an abelian group with exponent 4 will satisfy both of them. In fact, if it's a monoid it must be an abelian group.

This suggests taking an exponent 4 abelian group and tweaking the operation slightly (similar to other magmas used in the past that were of the form "xy = x + y + 1 if [parity condition], etc."). Let's write the abelian group operation as +. We know that left multiplication by a square should be bijective, so we can assume for example that $xy = x + y$ if $x = y$ or $x$ is a square (i.e. of the form $2k$) in the abelian group. So then it will be power-associative and have an identity. So 1323 becomes $x = y(((yy)x)y) = y(((2y)x)y) = y((2y + x)y)$, or rearranging, $p - 2y = y(py)$. Notice that taking it to have exponent 2 does not work here due to Sebastian's result because then there is only one square, 0. We might even be able to assume partial commutativity as Jose mentioned above. Anyways this equation seems a bit simpler -- can anyone show it has another solution where left-multiplication is not always injective, or that this is impossible?

In particular maybe we can define $xy = x + y + f(x, y)$ for some function and solve the resulting functional equation. There is in fact a model like this satisfying 1323 that isn't an abelian group: we fix some square element $u = 2k$ and define

$xy = x + y$ if $x$, $y$, or $x + y$ is a square

$xy = x + y + u$ otherwise.

So this model is unital, power-associative, and partially commutative. Unfortunately it is also commutative, so it satisfies 2744. If you don't include $y$ being a square in the first condition then 1323 won't hold anymore.

Some other observations: if left-multiplication is not injective then we have $py = py' = q$ for some values. Then let $x = p - 2y$ and x' = p - 2y'$$, so that $x = y((2y + x)y) = y(py) = yq$ and $x' = y'((2y' + x)y') = y'(py') = y'q$. So $p - 2y = yq$, and $p - 2y' = y'q$. Then $yq + 2y = y'q + 2y'$, so $y(py) + 2y = y'(py') + 2y'$. So $yq$ and $y'q$ have the same "parity" i.e. they differ by a square in the underlying abelian group.

[Bernhard Reinke]

Jose Brox said:

Btw, giving Vampire 999s (on TPTP.org) it cannot rule out the possibility of (a) plus (b) and the existence of 3 squares, nor does it prove the implication of 2744. Can you double check? The existence of 3 different squares can perhaps dissolve the contradiction in the piecewise affine model I was working with, I will check.

vampire reaches my memory limit, so maybe it is possible

[Bernhard Reinke]

I was thinking a bit about equations $(y^2x)y^2 = x \,\, (a), \quad xy^2 = y(xy) \,\, (b)$ in terms of rewriting. I think there is a nice confluent rewriting system for (a) + $y^2x = xy^2$, but (b) is tricker. (b) is equivalent to equation 4320. I tried to run the greedy algorithm for just (b) (so for eq 4320), but I get a strange error message, apparently the assumption a != b failed in normalize_eq.

[Terence Tao]

Just to summarize a bit of the 1323-relevant discussion over at the 1516 thread. It seems that 1323 has a number of "sporadic" laws of the shape $x \diamond y = z$ (where $z$ is somehow "simpler" than $x$ and $y$ concatenated), generated by the following laws, where $L_y, R_y$ are the usual left and right operators, $S$ is the squaring operator, and $T_y = R_{Sy} L_{S^2 y}$:

• Axiom 3 One has $y \diamond R_y L_{Sy} x = x$.
• Axiom 4 If $Sy \diamond x = z$, then $y \diamond R_y z = x$.
• Axiom 6' If $z \diamond y = w$, then $y \diamond w = T_y z$.
  (The numbering is explained over at the 1516 thread.)

Optimistically, applying Axiom 4 and Axiom 6' to Axiom 3 should generate a complete set of rules (this would require verifying Axioms 1, 2, 5 from the other post, and also showing that no other instance of Axiom 6 shows up not already covered by Axiom 6', after abstracting out the operators $S, L, R, T$ to involve pairing of trees (or words in a free magma) rather than 1516 magma operations.

Because there are two axioms, Axiom 4 and Axiom 6', that can propagate new rules in a non-commuting (and likely free) fashion, one has a potential exponential explosion (coming from the exponential growth in the free submonoid on two generators). However, one saving grace is that Axiom 4 is only triggered when the left argument is a perfect square. This is usually not the case for the laws generated by too many applications of Axiom 6', in particular after more than two such applications I don't think this situation should show up at all. We tried truncating the iteration by including all laws that could conceivably arise after enough applications of Axiom 6', e.g., $w \diamond T_y z = T_w T_y y$ which is the shape of the law formed from two applications of Axiom 6', but this unfortunately seems to imply 2744 for reasons that are currently unclear.

Anyway, this is all I have time for now. I'm hoping @Pace Nielsen 's new automated tool can help shed some light on the identities obeyed by 1323, and whether there is a chance of describing them well enough to resolve the implication to 2744.

[Jose Brox]

Terence Tao ha dicho:

• Axiom 6' If z⋄y=w, then y⋄w=Ty​z.

If we assume that the magma is unital, then we can replace 6' by the simpler

• Axiom 6b If $z⋄y=w$ then $y⋄w = Sy⋄z$
  (which is the identity (b) I introduced here).

[Terence Tao]

Ironically the approach I have may work best if one prevents as much simplification to occur as possible to make things "free" and avoid "collisions".

[Jose Brox]

My previous attempts had oversimplifications that I could remove, but here it is a proof that there is no unital 1323 magma $M$ carried by the integers whose product $x*y$ arises from piecewise affine functions parametrized by the equivalence classes of $(x,y) mod N$ for any $N$ (this is independent of the number of different squares):

Suppose that the product on $M$ is
$x*y := a_{\alpha\beta} x + b_{\alpha\beta} y + c_{\alpha\beta}$ with $x\equiv \alpha, y\equiv \beta (mod N)$
and that $u$ is the unit of $M$. Then
$u = u*u = a_{uu} u + b_{uu} u + c_{uu}$ (with abuse of notation) and also
$u+N = u*(u+N) = a_{uu}u + b_{uu}(u+N) + c_{uu},$
so substracting we find
$b_{uu}N = N$, hence $b_{uu} = 1$. Analogously, by working with $(u+N)*u$ we get that $a_{uu} = 1$. Then from $u = u*u$ we get
$c_{uu} = -u.$

Now, since $M$ is unital we have $x^2*x^2 = u$ for any $x$. Take $x\equiv u (mod N)$ with $x\neq u$. Then
$x*x = a_{uu}x + b_{uu}x + c_{uu} = 2x - u,$ with $2x-u\equiv u (mod N)$ again, so that
$u = x^2*x^2 = a_{uu}x^2 + b_{uu}x^2 + c_{uu} = 2(2x-u)-u = 4x-3u,$ what implies $x=u$, a contradiction.

[Bruno Le Floch]

I think the "reason" this approach fails is that the unit, and maybe all squares, should be kept away from the linear Ansatz. My (incomplete) attempt is to assume that the magma is unital and that the set $M_2=\{x\diamond x\mid x\in M\}$ of squares is closed under $\diamond$ so that it is a submagma obeying many conditions (for instance all its elements square to the unit). The simplest is $M_2=(\mathbb{Z}/2\mathbb{Z})^2$.

Then search for a solution of the form $M=M_2\sqcup N$ for some set $N$, equipped with:

• a squaring map $S\colon N\to M_2$,
• three bijections $L_A,L_B,L_C$ such that for each $y\in N$, the four elements $y,L_A(y),L_B(y),L_C(y)$ are pairwise distinct (we also denote $L_I=\mathrm{id}$),
• a function $f$ with domain $(N\times N)\setminus\{(x,L_t(x)), x\in N,t\in M_2\}$ and values in $N$, with the constraint that $f(x,y)\not\in\{y,L_A(y),L_B(y),L_C(y)\}$ for $x,y\in N$.

Then define $\diamond$ on $M$ by the operation on $M_2$, together with

$$\begin{aligned} I\diamond y = y\diamond I = y , \qquad A\diamond y = L_A(y) , \qquad y\diamond A = L_A^{-1}(y) , \\ y\diamond y = S(y) \in M_2 , \qquad y\diamond L_A(y) = A\diamond S(y) \in M_2 , \\ x\diamond y = f(x,y) \in N \setminus \bigl\{y,L_A(y),L_B(y),L_C(y)\bigr\} , \end{aligned}$$

where $A\diamond S(y)$ involves the operation in $M_2$. The equation to obey ends up being

$$f(y,f(x,y)) = x\diamond S(y) = L_{S(y)}^{-1}(x) .$$

For a given choice of $N,S,L_A,L_B,L_C$, we can hope to build $f$ a few entries at a time: at each step in the algorithm we pick a value $f(x,y)=z$, then we define $x_0=x,x_1=y,x_2=z$ and we see that we have to define $f(x_1,x_2) = L_{S(x_1)}^{-1}(x_0)$, which we call $x_3$, then we see that we have to define $f(x_2,x_3)$, and so on. In the cases that I had tried previously (with $M_2$ having only two elements, meaning a magma with only two squares, excluded by Bernhard), this sequence of $x_i$ ended up periodic and that led to some bijectivity, hence automatically obeying 2744. Now we have much more freedom because $S(x_i)$ can depend on $i$ and we have multiple $L_t$ bijections.

A rather simple case to try out is $N=\mathbb{Z}$ and $L_A(n)=n+1$, $L_B(n)=n+2$, $L_C(n)=n+3$, and $S$ either given by $n\bmod 4$, or chosen as we go.

[Jose Brox]

Bruno Le Floch ha dicho:

My (incomplete) attempt is to assume that the magma is unital and that the set M2​={x⋄x∣x∈M} of squares is closed under ⋄ so that it is a submagma

I have checked with Prover9 (20 minutes) and Vampire (999s), and from closure of squares plus identity element plus partial commutativity I couldn't get to 2744, so it seems a solid condition to impose!

I have checked that $x^2y^2$ can be neither $(xy)^2$ nor $(yx)^2$, though.

Perhaps an interesting observation is that under the square-closure hypothesis and all the others, the products $y(x(yx)) = x^2y^2 = x(y(xy))$ are a square for any $x,y$.

[Bruno Le Floch]

Thanks for checking that automated tools fail to find a contradiction! In your last statement, does $x^2y^2$ stand for $((x^2)y)y$ or $(x^2)(y^2)$? Is the proof human-understandable? If I understand correctly, it implies that $x(L_{y^2}^{-1}(x))$ is a square, which means it is equal to one of the $xL_t(x)$ for $t\in M_2$. This is especially interesting when the set of maps $\{L_t,t\in M_2\}$ is taken to not be invariant under inversion (for example my translations of $\mathbb{Z}$ by 0,1,2,3 are not invariant), because it automatically imposes non-injectivity of $L_x$.

[Jose Brox]

Bruno Le Floch ha dicho:

In your last statement, does x2y2 stand for ((x2)y)y or (x2)(y2)? Is the proof human-understandable? If I understand correctly, it implies that x(Ly2−1​(x)) is a square

I write $x^2y^2$ for $(x*x)*(y*y)$ (I give precedence to powers over products). But if the magma is unital, since it satisfies $y(xy) = xy^2$ (this is identity (b)), we also have $x^2y^2 = y(x^2y)$. If in addition we impose partial commutativity (i.e., $x^2y = yx^2$) then $x^2y^2 = y(yx^2)$ also. Then we can iterate and use (b) again to find $x^2y^2 = y(x(yx))$. Now, since $x^2y^2 = y^2x^2$, by symmetry we have $x(y(xy)) = x^2y^2$ too. They are squares since $x^2y^2$ is a square by your hypothesis.

[Bernhard Reinke]

@Daniel Weber Have you tried running the forcer script for equation 4320 (aka. condition (b))? I get a weird error message (an assertion fails in normalize_eq), but maybe I don't have the newest version of the forcer script

[Jose Brox]

Something that perhaps has not been stressed and is important for models: in a unital 1323 magma, any element has right inverses (this is already true if we impose $x(xx^2)) = 1$ for example, but it comes for free):
we know that $x^2x^2 = 1$, and by (b) we have $x^2x^2 = x(x^2x)$.

Moreover, by starting from $(x^2x^2)(y^2y^2) = 1$, if in addition we enforce partial commutativity, then by iteratively applying (b) and commutativity we can check that
$L_xR_xL_yR_yL_yL_xL_y x = 1$
(this has been verified by Prover9),
so we have potentially many right inverses.

Also, note that by (b), any right inverse satisfies $xx^{-2} = x^{-1}$ ($=x^{-2}x$ under partial commutativity).

[Terence Tao]

I (sadly) have to report a negative result: the axioms I proposed to generate simplifying rules for 1323 are inconsistent, specifically

• Axiom 1. If $x \diamond y = z$ and $x \diamond y = z'$, then $z = z'$
• Axiom 3. $y \diamond \tilde R_y \tilde L_{\tilde Sy} = x$
• Axiom 4. If $\tilde Sy \diamond x = z$, then $y \diamond \tilde R_y z = x$

where $\tilde L_y x = (y,x)$, $\tilde R_y x = (x,y)$, $\tilde S x = (x,x)$ are the pairing versions of $L_y,R_y,S$ respectively. Indeed from Axiom 3 we have $\tilde Sy \diamond \tilde R_{Sy} \tilde L_{\tilde S^2 y} x = x$ and hence by Axiom 4 $y \diamond \tilde R_y x = \tilde R_{Sy} \tilde L_{\tilde S^2 y} x$, hence $y \diamond \tilde R_y \tilde L_{\tilde S_y} x = \tilde R_{Sy} \tilde L_{\tilde S^2 y} \tilde L_{\tilde S_y} x$. But then from Axiom 3 and Axiom 1 we have $\tilde R_{Sy} \tilde L_{\tilde S^2 y} \tilde L_{\tilde S_y} x = x$, which is not the case.

Basically, the setup I had did not take into account known identities such as $R_{Sy} L_{S^2 y} L_{Sy} = 1$, and also $L_{Sy} L_y R_y = 1$. But actually the identity that concerns me the most is $L_y R_y = R_{Sy} L_{S^2 y}$, which comes from combining the previous two identities (left inverse equals right inverse). With all previous identities, e.g., $L_{Sy} L_y R_y x = x$ there was a sense that one side of the equation was definitely "simpler" than the other, and so one could try to build a set of sporadic rules accordingly; but with $L_y R_y x = R_{Sy} L_{S^2y} x$ , the left and right hand sides have comparable complexity, and it seems unlikely that one can model this either by $y \diamond R_y x = \tilde R_{\tilde Sy} \tilde L_{\tilde S^2 y} x$ or by $\tilde L_{\tilde S^2 y} x \diamond Sy = \tilde L_y \tilde R_y x$ in a consistent fashion.

So at this point I'm pessimistic on the idea of trying to build a model of 1323 out of modifying the free magma with only a few sporadic rules. Perhaps in the unital case one can find a more accurate initial model that already captures a lot of the known algebraic structure.

[Terence Tao]

I think I have created a unital, partially piecewise linear, partially greedy model for 1323 that refutes 2744, which came about by mashing together many ideas in this thread (particularly from @Jose Brox , @Ibrahim Tencer , @Bruno Le Floch , and @Joachim Breitner ), in particular trying to first nail down the squaring operation, then the operations of left and right multiplications of squares, and finally the multiplication table for non-squares, imposing simplifying assumptions such as $L_{Sy} = R_{Sy}$ to guide the ansatz. In the first two cases one can use a simple piecewise linear model that is also unital, but for the last case one needs to switch to a nonlinear model (and to use an infinite carrier) to break injectivity of $L_y$.

The carrier is the infinite abelian group of exponent two ${\mathbf F}_2^{\mathbb N} \times {\mathbf F}_2^{\mathbb N}$. We partially define the magma operation by setting
$(x,a) \diamond (y,b) = (x+y, a+b)$
if $a=0$ or $b=0$, and
$(x,a) \diamond (y,b) = (x+y+a, 0)$
if $a=b$ (note that this is consistent with the previous rule). The remaining operations $(x,a) \diamond (y,b)$ for $a,b,0$ distinct we leave undefined for now.

With these rules, $(0,0)$ is a unit, and the squaring operator is $S(x,a) = (a,0)$, so the set of squares is ${\mathbf F}_2^{\mathbb N} \times \{0\}$. We now have $L_{S(y,b)} (x,a) = R_{S(y,b)} (x,a) = (x+b, a)$, so axiom (a) (i.e., $L_{Sy}$ and $R_{Sy}$ invert each other) is satisfied since we are in characteristic 2.

[This is similar to @Bruno Le Floch 's ansatz except that we allow the submagma of squares to be much larger, being sort of like the "square root" of the entire carrier in size rather than just having cardinality 4. Having too few squares seems to generate a lot of constraints, for instance it triggers Bruno's property quite often. I arrived at the above ansatz by deciding I wanted squaring to be the shift map $(x,a) \mapsto (a,0)$, and then picking a commutative involution for the magma operation on the squares, which naturally suggested addition on an abelian group of exponent 2, and then trying to Sudoku the rest of the multiplication table.]

So it suffices to verify axiom (b), $R_{Sy} = L_y R_y$, or equivalently we have

Axiom: $(x,a) \diamond (y,b) = (z,c) \implies (y,b) \diamond (z,c) = R_{S(y,b)} (x,a) = (x+b,a).$

Several cases of this axiom are already verified:

• If $b=0$, then $(z,c) = (x,a) \diamond (y,0) = (x+y,a)$ and $(y,0) \diamond (z,c) = (y+x+y+a) = (x+b,a)$ as required.
• If $a=0$, then $(z,c) = (x,a) \diamond (y,b) = (x+y,b)$ and $(y,b) \diamond (z,c) = (y+x+y+b,0) = (x+b,a)$ as required.
• If $a=b$, then $(z,c) = (x,a) \diamond (y,b) = (x+y+a,0)$ and $(y,b) \diamond (z,c) = (y+x+y+a,b) = (x+b,a)$ as required.

So we just need to define $(x,a) \diamond (y,b)$ for $a,b,0$ distinct so that the Axiom is obeyed for such $a,b$.

Suppose we have $(x,a) \diamond (y,b) = (z,c)$ with $a,b,c,0$ distinct. Applying the Axiom repeatedly, we obtain a cycle of order 6:

1. $(x,a) \diamond (y,b) = (z,c)$
2. $(y,b) \diamond (z,c) = (x+b,a)$
3. $(z,c) \diamond (x+b,a) = (y+c,b)$
4. $(x+b,a) \diamond (y+c,b) = (z+a,c)$
5. $(y+c,b) \diamond (z+b,c) = (x,a)$
6. $(z+b,c) \diamond (x,a) = (y,b)$.

Note for $a,b,c,0$ distinct that there are no collisions between these six identities, or with the previously defined values of $\diamond$.

So now we can run a greedy algorithm! Start with some seed of finitely defined rules $(x,a) \diamond (y,b) = (z,c)$ for $a,b,c,0$ distinct that obey the Axiom. Then, pick an $(x,a) \diamond (y,b)$ that is not already defined, so in particular $a,b,0$ are distinct. Because of the infinite nature of both components of the carrier ${\mathbf F}_2^{\mathbb N} \times {\mathbf F}_2^{\mathbb N}$, we can then find $(z,c)$ with $a,b,c,0$ distinct such that none of the six laws above collide with any previously defined values of $\diamond$ (or with each other). Then add these six laws to the partially defined operation and iterate in the usual fashion to obtain a 1323 magma.

To contradict 2744, it suffices to refute the injectivity of $L_y$. So just pick $(x,a), (y,b), (y',b'), (z,c)$ with $a,b,b',c$ linearly independent (and $x,y,y',z$ arbitrary) and impose the six equations associated to both $(x,a) \diamond (y,b) = (z,c)$ and $(x,a) \diamond (y',b') = (z,c)$. One can check that no collisions occur and so we get a seed for the greedy algorithm for which $L_{(x,a)}$ is guaranteed to be non-injective.

[Bruno Le Floch]

Great! I think this same exact model should also give a proof that 1898 does not imply 2710, which is the dual of the 1729 implies 917 implication. I will double-check tonight.

[Michael Bucko]

Vampire says that'll work (assuming I don't have bugs, which can easily be the case). Could anyone help me review the TP file? (I tried to incorporate all the learnings)

% SZS status Theorem for 1323_2744

% SZS output start Proof for 1323_2744

8. ! [X0,X1,X2,X3,X4,X5,X6,X7] : (op(X0,X2,X1,X3,X4,X5) => (right_mult(X1,X3,X0,X2,X6,X7) & op(X1,X3,X4,X5,X6,X7))) [input]

9. ! [X0,X1] : ? [X6,X7,X10,X11] : (op(X0,0,X10,X11,X0,0) & op(X6,X7,X0,0,X10,X11) & op(X1,0,X1,0,X6,X7)) [input]

10. ! [X0,X1] : ? [X6,X7,X10,X11] : (op(X0,0,X10,X11,X0,0) & op(X6,X7,X1,0,X10,X11) & op(X1,0,X1,0,X6,X7)) [input]

11. ~! [X0,X1] : ? [X6,X7,X10,X11] : (op(X0,0,X10,X11,X0,0) & op(X6,X7,X1,0,X10,X11) & op(X1,0,X1,0,X6,X7)) [negated conjecture 10]

19. ! [X0,X1] : ? [X2,X3,X4,X5] : (op(X0,0,X4,X5,X0,0) & op(X2,X3,X0,0,X4,X5) & op(X1,0,X1,0,X2,X3)) [rectify 9]

20. ~! [X0,X1] : ? [X2,X3,X4,X5] : (op(X0,0,X4,X5,X0,0) & op(X2,X3,X1,0,X4,X5) & op(X1,0,X1,0,X2,X3)) [rectify 11]

27. ! [X0,X1,X2,X3,X4,X5,X6,X7] : ((right_mult(X1,X3,X0,X2,X6,X7) & op(X1,X3,X4,X5,X6,X7)) | ~op(X0,X2,X1,X3,X4,X5)) [ennf transformation 8]

28. ? [X0,X1] : ! [X2,X3,X4,X5] : (~op(X0,0,X4,X5,X0,0) | ~op(X2,X3,X1,0,X4,X5) | ~op(X1,0,X1,0,X2,X3)) [ennf transformation 20]

35. ! [X0,X1] : (? [X2,X3,X4,X5] : (op(X0,0,X4,X5,X0,0) & op(X2,X3,X0,0,X4,X5) & op(X1,0,X1,0,X2,X3)) => (op(X0,0,sK5(X0,X1),sK6(X0,X1),X0,0) & op(sK3(X0,X1),sK4(X0,X1),X0,0,sK5(X0,X1),sK6(X0,X1)) & op(X1,0,X1,0,sK3(X0,X1),sK4(X0,X1)))) [choice axiom]

36. ! [X0,X1] : (op(X0,0,sK5(X0,X1),sK6(X0,X1),X0,0) & op(sK3(X0,X1),sK4(X0,X1),X0,0,sK5(X0,X1),sK6(X0,X1)) & op(X1,0,X1,0,sK3(X0,X1),sK4(X0,X1))) [skolemisation 19,35]

37. ? [X0,X1] : ! [X2,X3,X4,X5] : (~op(X0,0,X4,X5,X0,0) | ~op(X2,X3,X1,0,X4,X5) | ~op(X1,0,X1,0,X2,X3)) => ! [X5,X4,X3,X2] : (~op(sK7,0,X4,X5,sK7,0) | ~op(X2,X3,sK8,0,X4,X5) | ~op(sK8,0,sK8,0,X2,X3)) [choice axiom]

38. ! [X2,X3,X4,X5] : (~op(sK7,0,X4,X5,sK7,0) | ~op(X2,X3,sK8,0,X4,X5) | ~op(sK8,0,sK8,0,X2,X3)) [skolemisation 28,37]

52. ~op(X0,X2,X1,X3,X4,X5) | op(X1,X3,X4,X5,X6,X7) [cnf transformation 27]

54. op(X1,0,X1,0,sK3(X0,X1),sK4(X0,X1)) [cnf transformation 36]

56. op(X0,0,sK5(X0,X1),sK6(X0,X1),X0,0) [cnf transformation 36]

57. ~op(sK8,0,sK8,0,X2,X3) | ~op(X2,X3,sK8,0,X4,X5) | ~op(sK7,0,X4,X5,sK7,0) [cnf transformation 38]

74. op(X0,0,sK3(X1,X0),sK4(X1,X0),X2,X3) [resolution 52,54]

75. op(sK5(X0,X1),sK6(X0,X1),X0,0,X2,X3) [resolution 52,56]

78. op(sK3(X0,X1),sK4(X0,X1),X2,X3,X4,X5) [resolution 74,52]

95. op(X0,0,X1,X2,X3,X4) [resolution 75,52]

96. ~op(sK3(X0,sK8),sK4(X0,sK8),sK8,0,X1,X2) | ~op(sK7,0,X1,X2,sK7,0) [resolution 57,54]

97. ~op(sK7,0,X1,X2,sK7,0) [subsumption resolution 96,78]

98. $false [subsumption resolution 97,95]

% SZS output end Proof for 1323_2744

% ------------------------------

% Version: Vampire 4.9 (commit cf529bc42 on 2024-07-12 16:29:36 +0100)

% Termination reason: Refutation

[Terence Tao]

Opened equational#811 to formalize this (and a blueprint update is en route at equational#810). If the same magma gives 1898->2710 then perhaps one can just update the blueprint accordingly (and I will also update the task). [EDIT: now updated.]

[Terence Tao]

I think you're right that it also refutes 1898 -> 2710, so it handles the easier of the two Ramanujan implications. I'll just go ahead and update the blueprint accordingly.

Sadly, this ansatz definitely obeys 2644, so the harder Ramanujan implication 1729 -> 817 remains open. But I guess @Shreyas Srinivas is still working on that one.

[Shreyas Srinivas]

Yeah I am still on it. Since I started using z3, I have found it easier to organise my thoughts and attempts in a jupyter notebook. I wish lean and ITPs were supported in them.

[Michael Bucko]

Shreyas Srinivas schrieb:

Yeah I am still on it. Since I started using z3, I have found it easier to organise my thoughts and attempts in a jupyter notebook. I wish lean and ITPs were supported in them.

Made Vampire and z3 available in a public notebook. Anyone who likes notebooks can now use it https://colab.research.google.com/drive/1M71WWJiy3Dnlt4oYbW51LJYzNc6Emawd?usp=sharing

[Michael Bucko]

(Longer sessions might require a Colab subscription)

[Shreyas Srinivas]

I am using it already on my local machine and for a different project as well

[Bruno Le Floch]

For the blueprint, are we interested in having the following results, especially the last one, which motivates the Ansatz a bit better?

Proposition: In an eq-1323 magma $M$ with unit $I$, the following properties hold:

• $x(yx)=y(x^2)$ for all $x,y\in M$,
• $(x^2)^2=I$ for all $x$,
• the bijections $L_{x^2},R_{x^2}$ are inverses of each other,
• the subset $\sqrt{I}=\{x\mid x^2=I\}$ is a (unital) submagma obeying equation 14 (Putnam law $x=y\diamond(x\diamond y)$).

[Terence Tao]

Sure, these would be great additions to the 1323 chapter, feel free to pr them if you have the time. Certainly these consequences (or at least suspected “friends”) of the unital hypothesis were very influential for me in trying this particular ansatz.

[Bruno Le Floch]

A few comments on your magma, in (a failed) hope to apply the same ideas to the remaining implications 1729⇒817 and 1516⇒255.

I notice that your choice of $(x,a)\diamond(y,b)$ for $\#\{a,b,0\}<3$ coincides with the operation $(x,a)\diamond(y,b)=(x+y+ab,a+b)$ which defines a (commutative, unital) magma obeying 1323 (here $ab$ denotes the component-wise product of the vectors). You use the same submagma $\sqrt{I}$, same left/right actions on $M$, and same squaring operation in $M$ so they are automatically consistent. Once these are fixed, the equation boils down to $y\diamond(x\diamond y)=\text{known}$. Crucially this only involves the operation twice, so that choosing a particular $x\diamond y=z$ forces the value of $y\diamond z$, which forces another one, and so on. The conditions to fulfill do not branch out. Periodicity is also helpful, but probably not crucial to keep control of things.

Since both 1729 and 1516 involve $L_{y^2}$, it is tempting to use the same approach: pick a rich enough base magma, then keep only the squaring operation, and the products of a square with anything (in both orders). The remaining equation only has two operations so we can try to fill in the rest of the table by a greedy algorithm. Sadly, the implications are immune to this approach because the RHS of the implications involve only squares and their products with other elements. For 1729⇒817, I got tempted to keep only $L_{x^2}$ and try to change $R_{x^2}$, but they have to be inverses of each other so that also fails.

[Terence Tao]

Thanks, this is a very clarifying interpretation. So in fact this is the "modified base magma" strategy, but with a very slightly nonlinear base. It suggests in fact that one could in fact replace the greedy step by a much more explicit modification of the magma that might have a very simple form (and be easy to formalize) - maybe just adding some extra polynomial corrections to the base law $(x,a) \diamond (y,b) = (x+y+ab, a+b)$ that vanishes when $a,b,0$ are not distinct. (This can't be done at the pointwise level over $F_2$, but maybe over a finite field $F_{2^k}$? Though somehow the infinite nature of the carrier has to come into play due to the immunity to finite counterexamples. Maybe a shift map needs to be employed?)

The broader strategy of finding simplifying assumptions that are ATP-checked (with reasonable confidence) to not accidentally prove the implication, but break down the problem into smaller pieces (in this case, this meant that the problem of determining the multiplication table for squares and non-squares was largely "decoupled"), seems promising still. Perhaps we should pursue it further in 1516, in simplifying the somewhat large number of identities involving squares, cubes, and fourth powers.

[Terence Tao]

It is ironic that I had dismissed @Jose Brox 's previous suggestion to the unital assumption to simplify the Axiom 6 propagation rule $z \diamond y = w \implies y \diamond w = R_{Sy} L_{S^2 y} z$ to $z \diamond y = w \implies y \diamond w = L_{Sy} z$ on the grounds that I wanted the propagation to be as complicated as possible to avoid collisions. But now I realize that the other gains from simplifying the ansatz (in particular, removing all the difficulties I was having with "Axiom 4", and also the other component of Axiom 6) greatly outweigh this cost.

[Bruno Le Floch]

It might be good to phrase the counterexample as living on the direct sum $\bigoplus_{n\in\mathbb{N}}\mathbb{F}_2$ (squared), which is countable, rather than on the product $\mathbb{F}_2^{\mathbb{N}}$ (squared), which is uncountable. Otherwise the countable version of the implication graph would technically be left incomplete.

[Alex Meiburg]

Surely the countable version of the implication graph and the uncountable version are isomorphic, because if there is a countermodel, it can always be reduced to a countable countermodel?

[Mario Carneiro]

I don't know if there are any implications which only have finite counterexamples

[Mario Carneiro]

I guess it's not possible because you can take direct products of magmas to make finite counterexamples infinite, unless it is the singleton magma

[Jose Brox]

Bruno Le Floch ha dicho:

Otherwise the countable version of the implication graph would technically be left incomplete.

By the Löwenheim-Skolem theorem, any first-order theory (in a countable language) which has an infinite model $M$ of some cardinal, has infinite models $M_\alpha$ for all infinite cardinals $\alpha$, which are elementarily equivalent to $M$ (i.e., "isomorphic" from the first-order-logic point of view, satisfy exactly the same first-order statements). [When I learnt about this, for me it was mind-blowing! Imagine, there are uncountable models of the natural numbers, countable models of set theory... !!]

In addition, since equational theories are closed under arbitrary cartesian products, once an equational theory has a nontrivial finite model, it has also a nontrivial infinite model, and then one for each infinite cardinal. Hence for equational theories there are only two cardinality questions in the coarse sense: 1) Is there a nontrivial finite model? And, if there is not, then 2) Is there an infinite model? (If the answer is also no then the theory is trivial). Ofc there is also the finer question of the spectrum of the theory, i.e., 3) For which finite cardinals does the theory have models? These matters are distinguishable because there exist first-order sentences $\phi_n$ which state "This set has at most $n$ elements" (but by Löwenheim-Skolem, the same cannot be done with "This set is finite", "This set is infinite", "This set is countable", and so on...).

[Bruno Le Floch]

Terence Tao said:

Suppose we have $(x,a) \diamond (y,b) = (z,c)$ with $a,b,c,0$ distinct. Applying the Axiom repeatedly, we obtain a cycle of order 6:

1. $(x,a) \diamond (y,b) = (z,c)$
2. $(y,b) \diamond (z,c) = (x+b,a)$
3. $(z,c) \diamond (x+b,a) = (y+c,b)$
4. $(x+b,a) \diamond (y+c,b) = (z+a,c)$
5. $(y+c,b) \diamond (z+b,c) = (x,a)$
6. $(z+b,c) \diamond (x,a) = (y,b)$.

[...] To contradict 2744, it suffices to refute the injectivity of $L_y$. So just pick $(x,a), (y,b), (y',b'), (z,c)$ with $a,b,b',c$ linearly independent (and $x,y,y',z$ arbitrary) and impose the six equations associated to both $(x,a) \diamond (y,b) = (z,c)$ and $(x,a) \diamond (y',b') = (z,c)$. One can check that no collisions occur and so we get a seed for the greedy algorithm for which $L_{(x,a)}$ is guaranteed to be non-injective.

Trying and failing to make an explicit construction here, I find that there is a typo in equations 5,6: $z+b$ should be $z+a$ I think. If I am right, then equation 6 implies $(y,b) = (z+a,c) \diamond(x,a)$ so that $(y,b)$ is entirely determined in terms of $(x,a)$ and $(z,c)$, hence $L_y$ is injective. In other words the twelve equations associated to $(y,b)$ and $(y',b')$ do have collisions. The "counterexample" no longer violates 2744. Can someone confirm that I got this right?

The key problem is the periodicity of equations 1-6 here (the periodicity of the sequence $x_i$ that I had defined in an earlier message as $x_{i+1} = x_{i-1}\diamond x_i$). It arises from the facts that multiplication by a square is an involution (more generally is periodic) and that it preserves the square, namely $(L_{w\diamond w}(x))^2 = x^2$. I'm not sure which one is easiest to break while keeping the base consistent.

[Terence Tao]

Ugh, you're right, the model currently does not break 2744, and we will need to tweak it to make the right multiplication by squares non-periodic. I'll play around with it and see if there is a reasonably painless fix.

[Jose Brox]

Bruno Le Floch ha dicho:

Trying and failing to make an explicit construction here

Heh, I have also been trying to build an explicit model, but just starting from your base magma and trying to modify it.

My idea was to change the product to
$(x,a)*(y,b) :=$
$(x+y+ab, a+b +S(x,a,y,b)z_b),$
where $z_b$ is orthogonal to $b$ and $S(x,a,y,b)$ is a "switch" (or indicator function) which is $0$ for "problematic" pairs and $1$ for "tame" pairs.

Imposing that $(x,a)^2 = (a,0)$ and $(0,0)$ is the identity element we get $S(x,a,x,a) = S(0,0,x,a) = S(x,a,0,0) = 0.$

Now imposing identities (a') and (b) we find relations between different switches and orthogonal elements:
$S(b,0,x,a)z_a = S(b,0,b,+x,a)z_{a+S(b,0,x,a)z_a}$
$S(b,0,x,a)z_a = S(x,a,y,b)z_b + S(y,b,x+y+ab,a+b+S(x,a,y,b)z_b)z_{a+b+S(x,a,y,b)z_b}.$

My original idea was to define $z_b$ as having only one $1$ at the position of the first $0$ of $b$ and then open some switches for good $a$ (like $a$ having the first $0$ at the same position as $b$, or being complementary to $b$ up to that position), but just working with the second identity proves this idea to be impossible (one opening leads to another and in the end to an unsatisfiable condition).

Does anyone see some easy way to circumvent this and save the model? I didn't even get to think about the first condition, perhaps it makes things even "more impossible".

[Jose Brox]

I guess more or less the same idea can be applied in an analogous context: Pick an infinite field $F$ of characteristic two, a vector space $V$ over $F$, and a symmetric bilinear form $q$. Now define the base magma to be $F\oplus V$ with product
$(\lambda,v)*(\mu,w) := (\lambda + \mu + q(v,w), v+w)$
and modify it with $z_w$ being orthogonal to $w$ with respect to $q$.

[Bruno Le Floch]

In a 1323 magma with left/right identity $I$ we have $(x^2)^2=I$ and $y(xy)=x(y^2)$ for all $x,y$. One can show that $\sqrt{I}=\{x,x^2=I\}$ is a submagma obeying equation 14 (Putnam) and having squares constant equal to $I$. Terry's construction (and Jose's modification I think) starts by taking $\sqrt{I}$ an abelian group of exponent $2$, and the set of squares to be all of $\sqrt{I}$, and additionally to take the bijections $L_{x^2}$ and $R_{x^2}$ (always inverses of each other) to be equal and given by the action of that abelian group on some auxiliary set $M\setminus\sqrt{I}$.

This already implies 2744. More generally, taking the set of squares to be a group and $x^2\mapsto L_{x^2}$ to be a group action on $M$ implies 2744. Note that

$$R_{(xy)^2} y = y (xy)^2 = (xy) (y(xy)) = (xy) (x(y^2)) = R_{x(y^2)} L_x y$$

for any $x,y\in M$. Then take $x=z^2$ so that subscripts in this formula are all squares. Since $L=R$ for squares, and since we have an abelian group action, we find $L_{(z^2 y)^2} y = L_{(z^2 y^2) z^2} y$. The LHS reduces to $L_{y^2}$. By injectivity of $R_y$, we learn that $(z^2 y)^2 = y^2$. In words, multiplication by a square does not change the squares. This is enough to get the periodicity of the $x_i$ sequence defined by $x_{i+2}=x_ix_{i+1}$, hence 2744.

[Terence Tao]

I implemented a (slightly messy) fix in the blueprint argument at equational#841. In the end, I gave up the assumption that $L_{Sx}$ and $R_{Sx}$ are equal, to allow the $R_{Sx}$ to act non-periodically. In order to do this, I had to introduce some artificial bijections between the countable exponent 2 group $G$, and the nearly torsion-free group ${\mathbb Q}^\times$ (non-zero rationals, with $+1,-1$ the only torsion elements), and now on each square root set $\sqrt{a} = \{ x: Sx = a \}$ with $a$ non-unital (which I now identify with ${\mathbb Q}^\times$), the operators $R_b$ and $L_a$ act by multiplication in ${\mathbb Q}^\times$, rather than by addition in $G$, to ensure non-periodicity. This is definitely not aesthetically pleasing (for instance it now uses the axiom of choice!), but it was the quickest patch I could come up with. I still hope there should be a simpler construction that does not use the greedy algorithm or choice.

[Bruno Le Floch]

I haven't fully checked, but this looks like a solution! I think you need to "arrange matters so that" $\phi_b(c)$ and $\phi_c(a)$ both have new primes (note that you cannot ask that of $\phi_a(b)$ since $a,b$ are already fixed). Otherwise the third relation $(\phi_c(a)^n z,c)\diamond(\phi_a(b)^{n+1} x,a) = \dots$ may collide with previous assignments.

(A few $b$ should be $b'$ in the corollary, but that's trivial for the reader to correct.)

The axiom of choice can be avoided by constructing the $\phi$ as they show up in the greedy algorithm I think, but that makes the story less readable.

[Jose Brox]

Bruno Le Floch ha dicho:

By injectivity of Ry​, we learn that (z2y)2=y2. In words, multiplication by a square does not change the squares.

Didn't have time yet to read all, but this conclusion seems false in my model: The square of $(x,a)$ is $(a,0)$, while the product with a square is
$(b,0)(x,a) = (b+x, a+S(b,0,x,a)z_a)$;
so, unless the rest of the argument actually forces $S(b,0,x,a)=0$ for all $b,x,a$, the square of $(b,0)(x,a)$ is not always $(a,0)$, there would be some $(a+z_a,0)$.

[Terence Tao]

@Bruno Le Floch Thanks for the corrections! But I think $\phi_c(a)$ does not need new primes (it just needs to avoid $\pm 1$, which it does) because $(\phi_c(a)^n z, c)$ would not have been used by any previous step of the algorithm as $c$ is novel.

I still view this construction as an inelegant hack though - it feels so "wrong" to force an exponent two group to behave like a torsion-free group via an axiom of choice (or greedy algorithm)-constructed bijection! I very much encourage the ongoing efforts to find a more "natural" construction for this problem.

[Bruno Le Floch]

@Terence Tao Correct. My mistake, thanks.

[Ibrahim Tencer]

I went back to the approach I mentioned above and it turns out it's straightforward to show that it will always produce a model satisfying 2744. To recap, we start with an exponent 4 abelian group and take $x \diamond y := x + y + f(x, y)$ with $f$ always giving a square, and $f(x, y) = 0$ if $x = y$ or if $x$ is even.

Then we have
$z + 2y = y \diamond (z \diamond y)$ and
$y \diamond (z \diamond y) = y \diamond (z + y + f(z, y)) = y + z + y + f(z, y) + f(y, z + y + f(z, y))$
So the functional equation for 1323 is (noting that $-f(z, y) = f(z, y)$ because it only gives squares)
$f(z, y) = f(y, z + y + f(z, y))$

Now let $v = f(z, y)$. Then we can repeatedly apply the functional equation to get:

$f(z, y) = f(y, z + y + v) = f(z + y + v, z + 2y) = f(z + 2y, 2z + 3y) = f(2z + 3y, 3z + y + v) = f(3z + y + v, z) = f(z, y)$

Then with $f(y, x) = w$, the RHS of 2744 becomes
$((y \diamond y) \diamond (y \diamond x)) \diamond y = (2y \diamond (y \diamond x)) \diamond y = (2y + (y + x + w)) \diamond y = (3y + x + w) \diamond y = (3y + x + w) + y + w = x + 2w = x$

So much for a more natural approach! I wonder if there is some explanation for why it has so many immunities or why "most" models of 1323 should also satisfy 2744.

[Ibrahim Tencer]

Actually this may be a special case of Bruno's argument above, hmm.

[Bruno Le Floch]

Ibrahim Tencer said:

I wonder if there is some explanation for why it has so many immunities or why "most" models of 1323 should also satisfy 2744.

Equation 1323 is of the form $W=f_1\circ\dots\circ f_k(W)$ for $W$ a word in some variables, with $f_i$ being left/right multiplication by some other variables (not in $W$).

In finite magmas this implies that $f_i$ are bijections (on the image of $W$) hence $W=f_{j+1}\circ\dots\circ f_k\circ f_1\circ\dots\circ f_j(W)$ for each $j$. These implications have no particular reason to be true in the infinite realm, so they tend to form Austin pairs. For instance the simplest Austin pair in the tour, (3588,3994), is of this form with $W=x\diamond y$, and (1323,2744) is of this form. If some $f_i$ are left/right multiplication by a single variable (and in some more general cases) we get that they are bijections, which is a very strong condition. For instance, the conjectural Austin law 5093 is of this form and can be shown in this way to imply equation 2 in finite magmas. In some exceptional cases such as Putnam laws 14 $x=y\diamond(x\diamond y)$ and 29 $x=(y\diamond x)\diamond y$, the implication also holds in infinite magmas.

Note also that immunity to finite magmas implies immunity to linear magmas because any linear expression contradicting the target law will still contradict it on a large $\mathbb{Z}/n\mathbb{Z}$.

Equation 1323 is peculiar in that $f_1$ and $f_k$ are two left-multiplications, so that any left-multiplication that matches both expressions (here $L_{y^2}$ and $L_{y'}$ for some $y,y'$, but we can have more general situations) is bijective. We can then "move" some left-multiplications around the cycle $f_1\circ\dots\circ f_k$ and get information about right multiplication. By tuning the variables other than $x$ (here taking $y$ to be a square), one can hope to make all left multiplications involved in the equation be bijective, and get bijectivity of some right multiplications (here, right-multiplication by squares).

The final nail in the coffin for 1323 is that once we treat these bijective multiplications (here, by squares) as being "understood", equation 1323 can be thought of as a "twist" of the Putnam equation 14, which is equivalent (even in the infinite case) to 29. So we really need the twist to be non-trivial to get a counterexample. By the way, in a vague sense, 1323 is 14 twisted by 14, but I cannot make this precise.

All this is informed by vague impressions coming from the remaining equations in the Higman-Neumann thread.