1648 !=> 206

Stream: Equational

[Bernhard Reinke]

Hello, I think I have a counterexample that shows that 1648 does not imply 206. The magma is supported on the integers and defined as follows

$$x ◇ y = x - sign(y - x)$$

In other words, x ◇ x = x, and x ◇ y = x + 1 if x > y, and x ◇ y = x - 1 if x < y.

Now this satisfies 1648: it is clear if x = y, otherwise consider the case x > y, then

$$(x ◇ y) ◇ ((x ◇ y) ◇ y) = (x + 1) ◇ ((x + 1) ◇ y) = (x + 1) ◇ (x + 2) = x$$

the case x < y is analogous. But this magma does not satisfy 206:

indeed, for x = 0, y = -1 we have

$$(x ◇ (x ◇ y)) ◇ y = (0 ◇ 1) ◇ -1 = -1 ◇ -1 = -1 \not= 0 = x$$

[Shreyas Srinivas]

can you formalise this in Lean?

[Shreyas Srinivas]

Btw, I assume you are picking a field

[Bernhard Reinke]

I am not sure what you mean, maybe I should make it more clear that I mean that it's defined on the integers

[Shreyas Srinivas]

Oh right. I should have read more carefully

[Bernhard Reinke]

Shreyas Srinivas said:

can you formalise this in Lean?

I don't have a working lean version installed, so probably it would be easier for someone else to formalize this. I could try to do a sketch with an online tool

[Shreyas Srinivas]

You can fork the repository, create a branch on your fork and open it on gitpod

[Shreyas Srinivas]

No installation is needed, just a free tier gitpod account and four clicks

[Shreyas Srinivas]

You can also try it out here opening this code sample in the online editor:

import Mathlib.Tactic

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

infix:65 " ◇ " => Magma.op

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

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

theorem Equation1648_implies_Equation206 (G: Type _) [Magma G] (h: Equation1648 G) : Equation206 G := by
  sorry
theorem Equation1648_not_implies_Equation206 : ∃ (G: Type) (_: Magma G), Equation1648 G ∧ ¬ Equation206 G := by
  sorry

[Shreyas Srinivas]

If you hover over that example you will see two icons on the top right corner. The second icon takes you to the lean playground

[Vlad Tsyrklevich]

(Deleted, I've made a whole host of mistakes in this calculation)

[Shreyas Srinivas]

Here's a long flow-of-thought proof. I think this can be golfed down significantly if split allowed naming the hypothesis and I used more mathlib defs:

import Mathlib.Tactic

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

infix:65 " ◇ " => Magma.op

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

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


def sign (x : ℤ) :=
  if x = 0 then 0 else if x < 0 then -1 else 1

theorem Equation1648_not_implies_Equation206 : ∃ (G: Type) (_: Magma G), Equation1648 G ∧ ¬ Equation206 G := by
  let instMagmaInt : Magma ℤ := {
    op := fun x y => x - sign (y -x)
  }
  use ℤ, instMagmaInt
  simp [Equation1648, Equation206]
  constructor
  · intro x y
    simp [instMagmaInt, sign]
    by_cases hyx : y = x
    case pos =>
      observe h_y_minus_x: y - x = 0
      simp[h_y_minus_x]
    case neg =>
      observe hy_neq_x : y - x ≠ 0
      simp [hyx, hy_neq_x]
      by_cases hy_lt_x : y < x <;> simp [hy_lt_x]
      case neg =>
        by_cases hyx_prec : y - (x - 1) = 0 <;> simp[hyx_prec]
        case pos =>
          linarith
        case neg =>
          by_cases hyx : y < x - 1 <;> simp [hyx]
          case pos =>
            linarith
      case pos =>
        by_cases hy_x_succ : y - (x + 1) = 0 <;> simp [hy_x_succ]
        case pos =>
          linarith
        case neg =>
          by_cases hy_lt_x_succ : (y < x + 1) <;> simp [hy_lt_x_succ]
          linarith
  · use 0,-1
    simp [instMagmaInt, sign]

[Shreyas Srinivas]

Feel free to use it

[Shreyas Srinivas]

One issue I noticed was that split doesn't throw only those goals there aren't closed when one uses split <;> split <;>... . It throws all of them

[Shreyas Srinivas]

@Mario Carneiro : is this expected behaviour? Seems suboptimal

[Mario Carneiro]

what is "this"? Your code doesn't have split in it

[Shreyas Srinivas]

No it doesn't, but in quite a few instances of by_cases a large number of subgoals were being closed by split <;> split <;> .. but because of the aforementioned issue, I just went ahead with by_cases instead of split

[Mario Carneiro]

Can you show me the code you want to write instead of the workaround?

[Shreyas Srinivas]

sure I'll need a few minutes

[Mario Carneiro]

I don't understand your references to "it" and "the aforementioned issue"

[Mario Carneiro]

split produces subgoals just like by_cases, I don't understand what you are asking for

[Shreyas Srinivas]

While trying to reproduce the issue with split, I found a shorter proof (CC : @Bernhard Reinke ) :

import Mathlib.Tactic

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

infix:65 " ◇ " => Magma.op

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

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


def sign (x : ℤ) :=
  if x = 0 then 0 else if x < 0 then -1 else 1

theorem Equation1648_not_implies_Equation206 : ∃ (G: Type) (_: Magma G), Equation1648 G ∧ ¬ Equation206 G := by
  let instMagmaInt : Magma ℤ := {
    op := fun x y => x - sign (y -x)
  }
  use ℤ, instMagmaInt
  simp [Equation1648, Equation206]
  constructor
  · intro x y
    simp [instMagmaInt, sign]
    by_cases hyx : y - x = 0 <;> simp[hyx]
    case neg =>
      split <;> simp_all <;> split <;> split <;> simp_all <;> linarith
  · use 0,-1
    simp [instMagmaInt, sign]

[Zoltan A. Kocsis (Z.A.K.)]

Excellent observation. The resulting model is also potentially a good candidate for "modified base model" proofs - very much comparable to the ones I used to settle 1661 => ... and 1701 => ...)!

[Shreyas Srinivas]

Mario Carneiro said:

I don't understand your references to "it" and "the aforementioned issue"

naming the split hypothesis like in by_cases, and being able to use them

[Shreyas Srinivas]

when split <;> <some_tactics> fails, split throws all the subgoals, including the ones it appears to have solved when the cursor is on <;>

[Shreyas Srinivas]

I'll try to reproduce this behaviour though it seems harder to reproduce a wrong proof that I had a few iterations ago.

[Bernhard Reinke]

Thanks @Shreyas Srinivas , your formalization looks nice! I don't think I will be able to help with the Lean formalization any further, feel free to take over!

[Zoltan A. Kocsis (Z.A.K.)]

The resulting model is also potentially a good candidate for "modified base model" proofs - very much comparable to the ones I used to settle 1661 => ... and 1701 => ...)!

I've just tested this construction, and unfortunately it's not a model of any other unknown antecedent. But it's still a good candidate for modification if it does not refute all other implications starting from 1648.

[Shreyas Srinivas]

PR coming up.

[Bernhard Reinke]

By the way, I think the following magma might be interesting: let x◇y = x + 1 if x >= y and x ◇ y = x - 1 if x < y. I think this still satisfies 1648, but not 151

[Shreyas Srinivas]

equational#569

[Shreyas Srinivas]

I have created a separate folder called "ManuallyProved" for these one-off proofs

[Bernhard Reinke]

Looks good to me (apart from the spelling of my surname :sweat_smile: )

[Shreyas Srinivas]

Oh sorry. Will fix

[Shreyas Srinivas]

I'll see if I can also prove that anti-implication of 151 in this PR

[Terence Tao]

These are great examples of the translation-invariant magma approach!

[Shreyas Srinivas]

Done.

[Shreyas Srinivas]

The proof is basically

import Mathlib.Tactic

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

infix:65 " ◇ " => Magma.op

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

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


theorem Equation1648_not_implies_Equation151 : ∃ (G: Type) (_: Magma G),
  Equation1648 G ∧ ¬ Equation151 G := by
  let instMagmaInt : Magma ℤ := {
    op := fun x y => if x > y then x + 1 else x - 1
  }
  use ℤ, instMagmaInt
  simp [Equation1648, Equation151]

  constructor
  · intro x y
    simp [instMagmaInt]
    split <;> simp <;> split <;> simp_all <;> linarith
  · simp [instMagmaInt]
    use 0
    simp

[Bernhard Reinke]

Nice! Probably there are even more anti-implications shown by the second example, I think 23 and 307 are also ruled out. The other equations in only one variable should be also easy to check.

[Shreyas Srinivas]

Would you like to contribute this one as a PR?

[Shreyas Srinivas]

If yes, then:

1. Create a file named Equation307.lean under the ManuallyGenerated folder
2. Add the import to ManuallyGenerated.lean.
3. Add the proof to Equation307.lean created in step 1.

[Vlad Tsyrklevich]

op := fun x y => if x > y then x + 1 else x - 1 appears to solve almost all outstanding unknowns for 1648. I was able to generate disproofs for all but 3253 (which is a dual of 4065 which is also disproved)

[Shreyas Srinivas]

Okay. Give me a few minutes to tidy up equational#569 and feel free to create a PR for the rest of them in the same file.

[Vlad Tsyrklevich]

151 and 206 are special cases of the general class, it may be worth it to just have a fact that covers all of them, though I'm not sure how that works with specializing in either 1 or 2 variables.

[Bernhard Reinke]

I am still struggling with setting up Lean again, so please go ahead @Vlad Tsyrklevich !

[Shreyas Srinivas]

206 came from a different example,

[Shreyas Srinivas]

We can have both of these separately if you put the generated proofs in the generated folder.

[Vlad Tsyrklevich]

That's true, I just mean to say the second formula covers 206 as well, it seems to be more general

[Vlad Tsyrklevich]

(I double checked the run, the second is more general)

[Shreyas Srinivas]

The pattern for the positive part of the proof seems to be "repeat split<;> simp_all until no conditionals remain and then try linarith"

[Vlad Tsyrklevich]

  @[equational_result]
  theorem Equation1648_facts : ∃ (G : Type) (_ : Magma G), Facts G [1648] [23, 151, 203, 206, 307, 1426, 1832, 2238, 2441, 3050, 3456, 3522, 4065, 4118] := by
    let hG : Magma ℤ := { op := fun x y => if x > y then x + 1 else x - 1 }
    use ℤ, hG

    constructor
    . intro x y
      dsimp [hG]
      split_ifs
      repeat simp_all
      repeat linarith
    . repeat' apply And.intro
      all_goals {
        by_contra h
        try {
          specialize h 0
          simp [hG] at h
        }
        try {
          specialize h 0 1
          simp [hG] at h
        }
        try {
          specialize h 1 0
          simp [hG] at h
        }
      }

[Vlad Tsyrklevich]

my ugly local working code. The try{}s seem like they're not desirable upstream, but I'm really an absolute lean beginner so I'm not sure what's is idiomatic

[Shreyas Srinivas]

Tbh, seems good.

[Vlad Tsyrklevich]

I wish there was a better way to express a try{} that then applied the value to the parent context if it succeeded. Then you could simplify it to:

try { specialize h 0 }
try { specialize h 0 1 }
try { specialize h 1 0 }
simp [hG] at h

but I'm just not sure if that's possible.

[Shreyas Srinivas]

I think you should push ahead and make a task and PR

[Shreyas Srinivas]

Here: the task is yours to claim: https://github.com/users/teorth/projects/1/views/8?pane=issue&itemId=83328189

[Vlad Tsyrklevich]

claimed, will submit momentarily

[Shreyas Srinivas]

I have not added the equational_result attribute in my PR, so I think it won't be counted on the dashboard. So your PR should be hassle-free

[Mario Carneiro]

Vlad Tsyrklevich said:

I wish there was a better way to express a try{} that then applied the value to the parent context if it succeeded. Then you could simplify it to:

try { specialize h 0 }
try { specialize h 0 1 }
try { specialize h 1 0 }
simp [hG] at h

but I'm just not sure if that's possible.

you can actually just drop the braces, those are two separate bits of syntax and the braces force the goal to be closed

[Vlad Tsyrklevich]

Wow! I wish I knew that 2 weeks ago

[Mario Carneiro]

the braces are alternative syntax for what is usually written · tac

[Shreyas Srinivas]

@Vlad Tsyrklevich : I suggest appending your proof to equational_theories/ManuallyProved/Equation1648.lean

[Shreyas Srinivas]

Let the other proofs be as they are. We do want to retain the other example, even if they don't add to the stats.

[Vlad Tsyrklevich]

equational#574

[Shreyas Srinivas]

I'll merge that as soon as CI is done

[Zoltan A. Kocsis (Z.A.K.)]

If you merge #573 as well, we should have a substantial reduction in unknown count today.

[Shreyas Srinivas]

@Zoltan A. Kocsis (Z.A.K.) : Could you shorten the proofs of all the anti-implications like @Vlad?

[Shreyas Srinivas]

All the proofs seem to follow a common pattern

[Zoltan A. Kocsis (Z.A.K.)]

I can try @Shreyas Srinivas, but it's probably best left to somebody else. As you'll recall, I've hit fun issues before, and while I took your suggestion to use split as much as possible, large simps with the mod_two_... strategies still didn't work too well. I'm primarily an Agda and Isabelle/HOL person, and so far haven't mastered how to do these modular-arithmetic case analyses well.

(these two comments should probably be moved to a more suitable thread, maybe the linked one)

[Shreyas Srinivas]

I can add them to your PR

[Vlad Tsyrklevich]

There is now one remaining open anti-implication from 1648, 3253, the dual of 4065. Transposing x/y in the given magma formula no longer satisfies 1648.

[Vlad Tsyrklevich]

One tool that would be really nice is a finite magma generator, plug in an equation number and get a random example magma, fields whose value can be anything are marked by a '?'. Sometimes it helps to just try to 'see' the structure of an example, or maybe a tool to build them step-by-step to see what the relationships between their constraints are.

[Terence Tao]

So maybe a Sudoku type interface where one can enter in different values of a multiplication table, and on the side it can show whether various laws are contradicted or not? Perhaps there are online Sudoku interfaces out there that could serve as a model (I haven't actually played around with Sudoku for years though, so I don't know what people use nowadays).

[Vlad Tsyrklevich]

oh sudoku is a great analogy, I've often thought about the constraints on a square when trying to solve one

[Shreyas Srinivas]

Check out the proofwidgets library

[Shreyas Srinivas]

You might be able to build such an interface yourself

[Vlad Tsyrklevich]

Maybe even something like, you get a 5x5 board and fill in an equation number, you fill in a square and the tool fills in whatever other squares are determined by that choice.

[Mario Carneiro]

Sounds like a job for a sat solver

[Shreyas Srinivas]

I think there was a project recently which in fact built sudoku into lean.

[Shreyas Srinivas]

You might be able to get z3 to fill in the values.

[Mario Carneiro]

lean ships with a sat solver these days, so maybe it's not even that hard to use sat solver queries to do the hints and propagation

[Shreyas Srinivas]

Oh yes, cadical

[Vlad Tsyrklevich]

I was thinking a webapp for ease-of-use, but there are transpilers as well of course

[Shreyas Srinivas]

For the interface check out the proofwidgets

[Shreyas Srinivas]

You will get something that works in-editoe

[Mario Carneiro]

lean's infoview is basically a webapp

[Terence Tao]

Opened equational#576 for this. I could imagine this being a fun project for someone who is good at this sort of interface design and has some time on their hands.

[Shreyas Srinivas]

See : https://github.com/TwoFX/sudoku

[Shreyas Srinivas]

It might give you a nice template to work with

[Vlad Tsyrklevich]

Yeah I saw it, but it uses typescript and I know so little about the web environment that just using plain JS sometimes seems easier, but maybe I should just try it. I guess another problem is I've only been using nvim but I should probably also give VS a try since everyone else uses it.

[Shreyas Srinivas]

Vanilla Javascript is valid typescript

[Shreyas Srinivas]

@Zoltan A. Kocsis (Z.A.K.) : I'll merge your PR for now. We can make a separate task for usingFactsSyntax

[Zoltan A. Kocsis (Z.A.K.)]

I was just about to push with the changes you requested.

[Zoltan A. Kocsis (Z.A.K.)]

(I.e. combined Facts and files moved to ManuallyProved)

[Zoltan A. Kocsis (Z.A.K.)]

So I'll make another PR shortly (just running tests to make sure there are no regressions)

[Shreyas Srinivas]

Oh okay I'll merge that one too when the new PR is ready

[Zoltan A. Kocsis (Z.A.K.)]

@Shreyas Srinivas This is now equational#579. Thanks!

[Shreyas Srinivas]

Interesting. In the mobile app the linkifier takes me to mathlib. On the desktop it takes me to equational_theories

[Shreyas Srinivas]

equational#579

[Shreyas Srinivas]

Merged. The webpage should be updated once the CI finishes its job

[Shreyas Srinivas]

Btw the no proof counter is already down to 364

[Zoltan A. Kocsis (Z.A.K.)]

we're down to 364! :tada:

[Shreyas Srinivas]

This is before the CI finishes on your PR I think

[Shreyas Srinivas]

We should check it again in 15-20 minutes

[Zoltan A. Kocsis (Z.A.K.)]

My last PR adds no implications (it just moves files) so it shouldn't make a difference, right?
Equation Explorer and Finite Magma Explorer are all updated to my previous PR (which actually refuted the 1659->... implications)

[Shreyas Srinivas]

Wait that only counts implications?

[Shreyas Srinivas]

I thought it counted all unknown implications and anti-implications

[Vlad Tsyrklevich]

I think he means that it didn't add refutations, and that he just moved things around

[Shreyas Srinivas]

Oh yeah right. I was thinking of the other PR

[Zoltan A. Kocsis (Z.A.K.)]

Sorry, I think I wasn't clear.
equational#579 didn't pass through CI yet, but it didn't add new results.
equational#573 is already through CI and the dashboard is updated with its results.

[Shreyas Srinivas]

Btw, I love the facts syntax. Kudos for coming up with that.

[Zoltan A. Kocsis (Z.A.K.)]

Hear hear, it's really helpful here but All4x4Tables would have been impossible without it!

[Terence Tao]

I just made a note to mention it in the plan of paper. Good notation is important for a project at this scale!

One minor observation: if a single law, EquationX has many anti-implications (to EquationY1, EquationY2, etc.) then it is possible to find a single magma G with Facts G [X] [Y1, Y2, ...] by taking the direct product of individual counterexamples. So one can always, if desired, merge a whole bunch of anti-implications coming from a single law EquationX into a single Facts statement if one wanted (though this might be a somewhat artificial magma G).

[Zoltan A. Kocsis (Z.A.K.)]

@Terence Tao Indeed. For finite magmas, doing the opposite is a good idea, since checking that the equation holds in the product is going to be strictly more expensive than checking it in the factors.

[Vlad Tsyrklevich]

(Deleted)

[Vlad Tsyrklevich]

Well, nevermind my previous enthusiasm, I proved the converse of an unknown.

[Terence Tao]

Yeah, the model you gave looked like it should work even when specialized to say a 4 x 4 magma, in which case it should have already been picked up in previous sweeps.

[Bernhard Reinke]

A small observation in the opposite direction: I think for finite magmas we have that 206 => 1648: A finite magma satisfying 206 has to be right cancellative. But then we can substitute x ◇ y for x in 206 and obtain

$$x ◇ y = ((x ◇ y)◇((x ◇ y)◇y))◇y$$

so by cancelling ◇ y we get 1648. So a counterexample for 206 !=> 1648 has to be infinite.

[Bernhard Reinke]

Not sure if there is a finite counterexample for 1648 !=> 206

[Vlad Tsyrklevich]

Bernhard Reinke said:

A finite magma satisfying 206 has to be right cancellative.

I don't understand, why is that the case?

[Terence Tao]

206 implies that the maps z ↦ z ◇ y are surjective, hence injective on a finite magma.

[Shreyas Srinivas]

Btw, we ought to add a blueprint chapter on these anti-implication proofs from special counterexamples.

[Shreyas Srinivas]

Any volunteers?

[Terence Tao]

I think @Zoltan A. Kocsis (Z.A.K.) already is going to write something on modifying base models such as translation invariant magmas

[Vlad Tsyrklevich]

Bernhard Reinke said:

A small observation in the opposite direction: I think for finite magmas we have that 206 => 1648: A finite magma satisfying 206 has to be right cancellative. But then we can substitute x ◇ y for x in 206 and obtain

$$x ◇ y = ((x ◇ y)◇((x ◇ y)◇y))◇y$$

so by cancelling ◇ y we get 1648. So a counterexample for 206 !=> 1648 has to be infinite.

Managed to formalize this with help from Daniel's previous formalization for 3588/3994. I think this is an interesting case because 3558/3994 had 3 variables/4 operations each while 206/1648 have 2 variables and 3/4 operations. That said, 206=>1648 is still open, so until it's proven it's just a conjecture that this doesn't apply in the infinite case as well.

  theorem Finite.Equation206_implies_Equation1648 (G : Type*) [Magma G] [Finite G] (h : Equation206 G) : Equation1648 G := by
    intro x y
    let S := {x | x : G}

    have m1 : S.MapsTo (· ◇ y) S := by
      intro
      simp [S]
    have t : S.SurjOn (· ◇ y) S := by
      intro x _
      let z := x ◇ (x ◇ y)
      use z
      simp [S, z]
      apply Eq.symm (h x y)

    rw [Set.Finite.surjOn_iff_bijOn_of_mapsTo (Set.toFinite _) m1] at t
    apply t.injOn (by simp [S]) (by simp [S])
    simp
    apply h (x ◇ y)

[Vlad Tsyrklevich]

I'll submit a draft PR for it tomorrow that can sit until a refutation comes in to verify that it's actually an interesting case. Makes me curious what the stats are on finite magma refutations for lower bounds on such cases.

[Pietro Monticone]

Shreyas Srinivas said:

See : https://github.com/TwoFX/sudoku

That is written in Lean 3. Here is the WIP port to Lean 4 https://github.com/avigad/LeanSudoku

[Bernhard Reinke]

I tried to come up with an example for 206 !=> 1648, but I made a silly computational mistake

[Bernhard Reinke]

Probably I can fix it, but my first attempt was wrong

[Shreyas Srinivas]

The 9-10 anti-implications here can also be shortened to one using FactsSyntax : https://github.com/teorth/equational_theories/blob/6fa72b34a6ec989e2f91589b4d133ae8663f300c/equational_theories/ManuallyProved/Equation1701.lean#L132

[Shreyas Srinivas]

Here's the task up for claiming : https://github.com/users/teorth/projects/1/views/8?pane=issue&itemId=83458223

[Bernhard Reinke]

I think I have a sketch for an example of a magma satisfying 206 but not 1648. I use the translation invariant approach, but for a non-commutative group: let $G$ the free product of three cyclic groups of order 2. If we have the alphabet $A = \{a,b,c\}$ then we can identify $G$ with the reduced words in $A$ that have no subwords of the form $aa, bb, cc$.

Our magma will be defined on G and will satisfy

$$x ◇ y = x f(x^{-1}y)$$

where $f \colon G \rightarrow \{1, a, b, c\}$.

Then the RHS of 206 is

$$(x ◇ (x ◇ y)) ◇ y = (x ◇ (x f(x^{-1}y)) ◇ y = (x f(f(x^{-1} y))) ◇ y = x f(f(x^{-1} y)) f( (f(f(x^{-1} y))^{-1} x^{-1} y)$$

Setting $z = x^{-1} y$, we get that 206 is equivalent to
$f(f(z)) f ( f(f(z))^{-1} z) = 1$. Under the assumption that $f$ maps to $\{1, a, b, c\}$ (so $f(z) = f(z)^{-1}$), this simplifies to

$$f(f(z)) = f( f(f(z)) z)$$

I claim the following f satisfies this: we set

$$f(1) = 1, f(a) = b, f(b) = c, f(c) = a$$

now, if $w$ is a nonempty reduced word not starting in $a$, we set $f(aw) = a$, cyclically symmetric for reduced words starting in b and and c. Let us check that this satisfies $f(f(z)) = f( f(f(z)) z)$:

It is clear that $f(f(1)) = f( f(f(1)) 1) = 1$.

We have $f(f(a)) = f(b) = c$, and $f(f(f(a))a) = f(ca) = c$.

For $w$ is a nonempty reduced word not starting in $a$, we have
$f(f(aw)) = f(a) = b, so f( f(f(aw)) aw) = f(baw) = b$. The rest follows by symmetry.

I think 1648 translates to
$f(z)f(f((f(z))^{-1} z)) = 1$
this is not satisfied, as $f(a) f(f( (f(a))^{-1} a) = b f(f(ba)) = b f(b) = bc \not= 1$.

I hope I haven't made any computational mistakes (this is in fact my second try, :sweat_smile: ), would someone like to check whether this makes sense? I don't think I would be able to formalize this in Lean myself.

[Bernhard Reinke]

I think this magma has the following geometric interpretation: consider a planar 3-regular tree (every vertex has 3 edges, and we can talk about the cyclic ordering of edges at a vertex). Our magma will be defined on the vertices of this graph. We define x ◇ y as follows: if $x =y$, then $x ◇ y = x$. If x and y have distance at least 2, then x ◇ y is the neighbor of x that is the closest to y. If x and y have distance 1 (so that they are neighbors), then x ◇ y is the next neighbor of x after y in the cyclic ordering. Now 206 holds: for x = y there is nothing to show. For $x \not= y$, the geometric insight is that x ◇ (x ◇ y) is always a neighbor of x that is away from y. This is clear if x and y had distance at least 2, but it also works if they are neighbors. So (x ◇ (x ◇ y)) has always distance at least 2 from y, and we get (x ◇ (x ◇ y)) ◇ y = x. I think this construction should in fact work for any (infinite) planar tree where every vertex has at least degree 3.

[Bernhard Reinke]

I am curious what the best way to implement this is. I think the generalized construction should work on a "rooted 3-regular tree", i.e. List (Fin 3). Probably is it possible to write down an explicit magma there (losing translation invariance), but this might be tedious. On the other hand, the group description uses some things I cannot find easily in mathlib

[Daniel Weber]

Just a note that https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1076.20!.3D.3E.203 also has (the dual of) this non-implication (in another way), and I'm planning to write code to automatically formalize it

[Bernhard Reinke]

Ah, thanks for the heads up! Probably it makes sense to use the more general approach then

[Terence Tao]

Well, this tree construction is quite novel (I don't think anyone has previously considered a non-abelian translation-invariant model before), and the geometric nature of this construction could suggest similar constructions for future work on other implications. I'll take a closer look at the construction later when I have time, but for now I have updated the commentary for 206 on equation explorer to indicate that we now have a provisional construction.

[Zoltan A. Kocsis (Z.A.K.)]

Terence Tao said:

I think Zoltan A. Kocsis (Z.A.K.) already is going to write something on modifying base models such as translation invariant magmas

This is one of the few things I still intend to work on, piece by piece this week when I get a a bit of time here and there. But I'll post this here; feel free to make it a Github issue if you think it's a good plan too.

The idea is the following:

Unify the Asterix and Greedy chapters into a chapter provisionally titled "Infinite magma constructions" , with the following sections.

1. Translation-invariant magmas: A section defining translation-invariant magmas and giving an example.
2. The Asterix equation: The bulk of the current Asterix chapter.
3. Greedy constructions: The current Greedy chapter.
4. A survey of examples: This would consist of brief explanations of the following simple examples. I tried to pick simple-but-nontrivial ones, rather than showcasing the most "powerful" approaches. A translation-invariant magma played straight, by Reinke to refute 1648->206; an example of my modified translation-invariant magmas, as written here: 1659->45; an elegant greedy construction, Pace Nielsen's one refuting 1076->3.

[Terence Tao]

Sounds great! I have created equational#591 for this.

[Terence Tao]

Bernhard Reinke said:

I think this magma has the following geometric interpretation: consider a planar 3-regular tree (every vertex has 3 edges, and we can talk about the cyclic ordering of edges at a vertex). Our magma will be defined on the vertices of this graph. We define x ◇ y as follows: if $x =y$, then $x ◇ y = x$. If x and y have distance at least 2, then x ◇ y is the neighbor of x that is the closest to y. If x and y have distance 1 (so that they are neighbors), then x ◇ y is the next neighbor of x after y in the cyclic ordering. Now 206 holds ...

This is a beautiful construction! A good example of a proof which is easy to see visually once one draws the right pictures, but involves a lot of opaque case checking if done algebraically. (I have this mental image of x sucking in y by "gravitational attraction" until y borders x (at x ◇ y), at which point it "orbits" x (moving to x ◇ (x ◇ y)). If one then exerts a gravitational force from this new location x ◇ (x ◇ y) on the original locationy, that location will now crash into x.) This type of geometric construction could be a useful paradigm to find human-generated solutions to any outstanding equations that survive our greedy algorithm run. I have opened equational#596 for anyone who wishes to try formalizing it.

I'm curious how you were led to these constructions. I can understand how you would experiment with a translation-invariant non-abelian group, but how were you led to this specific group and this specific choice of f?

[Joachim Breitner]

Terence Tao said:

Sounds great! I have created equational#591 for this.

Nice little exercise. I proved it, up to a bunch of sorried lemmas about reduction of such words. Maybe I’ll pull in mathlib for that, or just prove them directly (which may be more fun). But my bus is arriving at the destination, so maybe later tonight or tomorrow.

[Bernhard Reinke]

Terence Tao said:

I'm curious how you were led to these constructions. I can understand how you would experiment with a translation-invariant non-abelian group, but how were you led to this specific group and this specific choice of f?

I am not sure I can give you a complete answer to this. One thing that led to the consideration of this group is the fact that 206 has a model on $C_2$ via $x ◇ y = x + 1$. I had the hope I can glue these kind of models together, so this group was a natural candidate. I used also a kind of greedy approach, trying to define fby increasing word length. The restriction that f only maps into the generating set was posed to limit my search space. I spend some time trying to find an interesting f with f(1) = f(a) = a, but this ruled out the assignments f(b) = c, f(c) = b or f(b) = b, f(c) = c, so I was less optimistic for this variant. I noted that it would be a nice property of we always have that f(f(z))z doesn't cancel, i.e., the letter f(f(z)) shouldn't be the starting letter of z. In this way we could use the greedy approach, defining new values on the RHS. Then I tried around with the starting conditions f(1) = 1, f(a) = b, f(b) = c, f(c) = a and got consequences f(ca) = c , f(aca) = a, f(baca) = b, so the choice of f seems natural from there.

[Joe McCann]

Slightly off topic question, but is this the de-facto thread now for 1648? From when I was experimenting with it I was able to find some oddities of the finite magmas that it holds for (which turn out to be not very many, only 82 of the 5^25 5-element magmas satisfy it!) Was going to type it up into the commentary.md but also wanted to put it here to laugh about with yall

[Joachim Breitner]

Joachim Breitner said:

Terence Tao said:

Sounds great! I have created equational#591 for this.

Nice little exercise. I proved it, up to a bunch of sorried lemmas about reduction of such words. Maybe I’ll pull in mathlib for that, or just prove them directly (which may be more fun). But my bus is arriving at the destination, so maybe later tonight or tomorrow.

https://github.com/teorth/equational_theories/pull/599

I really shouldn't start working on fun little things at the evening. It’s 3am now…

I chose to made it self-contained, so there is 300 lines to develop the reduction function to construct the free product of three cyclic groups of order 2, and then 30 lines for the construction of the magma. Probably could have saved work by searching through mathlib… but where is the fun in that.

Will clean up tomorrow.

:zzz:

[Terence Tao]

By the way, 1648 => 3253 is still open, if anyone wants to work on that.

[Joachim Breitner]

https://github.com/teorth/equational_theories/pull/599 is now in a presentable, somewhat documented form and contains a self-contained development of reducing words over copies of the simple group of order two :musical_notes:

[Vlad Tsyrklevich]

equational#606 has the 'Austin pair' result now that the non-implication is proven.

[Bernhard Reinke]

Here is an attempt for 1648 !=> 3253 using again the noncommutative translation invariant approach.

Consider $G = F_3$ the free group on three elements $\{a, b, c\}$. We construct $x◇y = xf(x^{-1}y)$ where the image of $f$ is contained in $\{a,b,c, a^{-1}, b^{-1}, c^{-1} \}$.
Equation 1648 can be written as
$(x ◇ y) ◇ ((x ◇ y) ◇ y) = (xf(x^{-1}y)) ◇ (xf(x^{-1}y) ◇ y) = (xf(x^{-1}y)) ◇ (x f(x^{-1}y) f(f(x^{-1}y)^{-1} x^{-1} y) = x f(x^{-1}y) f(f(f(x^{-1}y)^{-1} x^{-1} y))$, or (using again $z = x^{-1} y$)

$$f(z)^{-1} = f(f( f(z)^{-1} z)$$

Equation 3253 is equivalent to $f(1) = f(f(f(1)))$.

We let $f(1) = a, f(a) = b, f(b) = c, f(c) = b^{-1}, f(b^{-1}) = a, f(a^{-1}) = c^{-1}, f(c^{-1}) = a^{-1}$. Note that f restricts to a derangement on $\{a,b,c, a^{-1}, b^{-1}, c^{-1} \}$, let us denote by $g$ the inverse of $f$ on this set. Finally, if $w$ is a reduced word of length at least 2 starting in the letter $l$, we set $f(w) = g(l)$.

Let us check that this satisfies the equation: for $z = 1$ we have $f(1)^{-1} = a^{-1} = f(f(a^{-1})) = f(f( f(1)^{-1} 1))$. If $w$ is a nonempty reduced word, we see that $(f(w))^{-1} w$ is still reduced (basically because f(for length 1) and g (for length > 1) are derangements on the generating set). Hence $f(f( f(w)^{-1} w)) = f(g ( f(w)^{-1})) = f(w)^{-1}$.
On the other hand, $f(f(f(1))) = c \not= a = f(1)$, so 3253 does not hold.

[Joachim Breitner]

I assume you can’t adjust this construction to use the product of three copies of the cyclic group of order two, which we already have constructed for the other example? :)

[Bernhard Reinke]

Not really, if $f(1)$ has order 2, then 3253 holds. But I think free groups are already in mathlib

[Joachim Breitner]

Right, still more work than just extending the existing file with maybe a different f :-)

[Bernhard Reinke]

Apparently it is also solved using greedy techniques

[Bernhard Reinke]

see here

[Joachim Breitner]

Ok, so no need to pounce onto that one yet?