An old new idea

Stream: Equational

[Pace Nielsen]

Someone previously mentioned constructing a monoid on the complex numbers, where the monoid map is linear of the form x*y=ax+by for some a,b\in \C. (Apologies for forgetting who it was who had this great idea.) I believe that this shows that Eqn1286 =/> Eqn3, which is one of the open questions.

In that case, this turns into finding a,b such that a+b\neq 1, yet b^2=-a/(a^2+1) and b=(2a^2+1)/(a^5+a^3). Taking any root of a^5+2a^4+3a^3+3a^2+a+1 should do the trick.

[Terence Tao]

I guess it's some Grobner basis calculation for any given implication Equation X => Equation Y whether this construction furnishes a counterexample or not. I have no idea whether this is already implemented within Lean but I could imagine it is well within the capability of e.g., SAGE to enumerate through the 20,000 remaining implications to see if any further examples of this type exist.

[Cody Roux]

I feel dumb not being able to articulate this correctly, but it's not necessary to go all the way to Grobner bases since we are looking at quadratic forms, the "duality trick" should suffice (and reduce it to a linear problem). But still might not be easy to formalize.

[Terence Tao]

One can also model these infinite magmas through a finite field model (replace C by F_p for a sufficiently large prime p), by the Lefschetz principle. So one could just do a numerical search with random p, a, b and one has a reasonably high likelihood to get a hit. For instance in the example above, for typical medium size p one should be able to get a working a,b about 1/p^2 of the time. It may thus be faster to simply do random brute force across all equations than a Grobner basis for each pair of equations. (Though we should now be able to cut down the number of equations to look at a fair bit, as many equations now have 0 incoming or outgoing open implications, and of course we only need to study one representative from each equivalence class.)

[Terence Tao]

One has to try a couple p, e.g. p = 5, 7, 11, just because some of the polynomial equations to solve won't have roots in F_p. (One could also work in fields of prime power order, e.g., F_8 or F_9.)

[Terence Tao]

In this model all words evaluate to linear maps, so one can check equational laws just by comparing two coefficients; one does not need to check all inputs. So this is actually quite a fast verification and should be quite doable numerically, with very concrete finite magmas (associated to triples (p,a,b)) output as a consequence.

[Terence Tao]

Created equational#346 to propose testing out this idea on the remaining set of equations.

[Heather Macbeth]

I did one non-implication of this form (3116 does not imply 513) to show how the proof style can be expressed in Lean. (Proofs generated by polyrith).

import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.Tactic.Polyrith

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

infix:65 " ◇ " => Magma.op

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

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

def G : Type := AlgebraicClosure ℚ

open Polynomial

noncomputable def foo : Polynomial (AlgebraicClosure ℚ) := X ^ 4 - X ^ 3 + 1

theorem foo_degree : foo.degree = 4 := by
  unfold foo
  compute_degree
  · norm_num
  · decide
  · decide

theorem foo_degree_ne_zero : foo.degree ≠ 0 := by
  rw [foo_degree]
  norm_num

noncomputable def α : AlgebraicClosure ℚ := (IsAlgClosed.exists_root foo foo_degree_ne_zero).choose
theorem spec_α : foo.IsRoot α := (IsAlgClosed.exists_root foo foo_degree_ne_zero).choose_spec
theorem spec_α_eq : α ^ 4 - α ^ 3 + 1 = 0 := by simpa [foo] using spec_α

noncomputable instance instG : Magma G where
  op x y := α * (id x : AlgebraicClosure ℚ) + (1 - α) * (id y : AlgebraicClosure ℚ)

theorem Equation3116_not_implies_Equation513 :
    ∃ (G: Type) (_: Magma G), Equation3116 G ∧ ¬ Equation513 G := by
  use G, instG
  constructor
  · simp [Equation3116, instG, G]
    intro x y
    linear_combination (x - 1 * y) * spec_α_eq
  · simp [Equation513, instG, G]
    use 1, 0
    intro H
    apply one_ne_zero (α := AlgebraicClosure ℚ)
    linear_combination
      (-(19 / 45 * α ^ 3) + 17 / 45 * α ^ 2 + 16 / 45 * α + 23 / 45) * H +
        (-(19 / 45 * α ^ 3) + 74 / 45 * α ^ 2 - 92 / 45 * α + 1) * spec_α_eq

[David Renshaw]

For @Pace Nielsen's initial example above (Eqn1286 =/> Eqn3), (p,a,b) = (11, 1, 7) works as a finite refutation.
PR incoming.

[David Renshaw]

equational#349

[Terence Tao]

It's amusing that when restricting to these linear magma operations, magma varieties basically become algebraic varieties.

[David Renshaw]

@Zoltan A. Kocsis (Z.A.K.) can you add the above 11x11 magma to your list and generate all consequences? I'm noticing that it proves a bunch more anti-implications involving Eqn1286.

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

Certainly @David Renshaw will do in a bit!

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

@David Renshaw - a bit behind with other stuff, so this'll have to be on hold until tomorrow. Sorry :(

[Will Sawin]

In fact examples are relatively likely to exist over finite fields (not necessarily F_p) even when they don't exist over C, particularly for 3-variable equations. 3-variable equations become triples of polynomial equations in two variables, and a generic such triple doesn't have solutions over C but does have solutions over a few finite fields.

[Daniel Weber]

Are there any ways to generalize this approach which could refute implications which hold on finite models?

[David Renshaw]

@Heather Macbeth a finite refutation for your implication above is given by (p,a,b) = (11, 3, 9). See equational#360.

[Will Sawin]

Daniel Weber said:

Are there any ways to generalize this approach which could refute implications which hold on finite models?

Going to higher-degree polynomials doesn't fix the problem that any tuple of equations and negations of equations that can be satisfied over C can be satisfied over a large finite field. The general idea of "take some understood algebraic structure and define a magma operation using operations of that structure" could potentially produce further examples, for example considering nonabelian groups with magmas defined using the group operation, but most structures I can think of that are easy to compute in also have this kind of reduction to finite examples property (e.g. residually finite groups).

[Leo Shine]

I'm sure it doesn't matter as I didn't get this idea to go anywhere as I found it hard to find a real example of where this was useful for an implication that wasn't already generated but I mentioned this idea before this thread. I don't really know how to do this but I imagine you can use field extensions on other finite fields to generate more magmas like this.

I couldn't work out how you'd get useful magmas out of this ideas for equations that don't have 2 variables and have at least 2 instances of each variable in them.

[Leo Shine]

The other problem I found is that there had to be some sort of reason such a counter example would not have already been found by #Equational19 which brute forced small polynomials in Z/n

[Will Sawin]

Leo Shine said:

The other problem I found is that there had to be some sort of reason such a counter example would not have already been found by #Equational19 which brute forced small polynomials in Z/n

Do you know why the examples people found on this thread weren't found by equational#19?

[Will Sawin]

Maybe something to do with magmas with 6 or more elements being excluded from the PR

[Leo Shine]

No I have not really looked into it very much sorry.

[Leo Shine]

Looking at code it only goes up to n=12 so could easily be missing bigger examples

[Leo Shine]

Also there were like 6 different variables so finding the Z/11 example above is going to be less than a 1/100000 chance. So maybe not run enough to find.

[Nicholas Carlini]

Will Sawin said:

Do you know why the examples people found on this thread weren't found by equational#19?

That search wasn't a complete brute force, I just ran it on python for a few hours and stopped it when it seemed like it had ran "long enough". At that point in the project it refuted 60% of the unknown implications (up from 0%). I never went back to it because I'd assumed that after we did enumeration over the 3x3 and 4x4s, and then the theorem provers, there wouldn't be any low hanging fruit for such a simple method to find.

But I guess clearly that was wrong: I can resume a bigger brute force and see if there's anything more new that's found.

[Terence Tao]

Yeah it seems that restricting attention to linear operations instead of quadratic ones has a much higher "yield" because many fewer equations have to be satisfied for things to go right. In particular, in order for a law x ◇ y = a * x + b * yto obey a law of k variables, the coefficients a and b need to satisfy k polynomial equations with integer coefficients (I believe the fancy name for this is "planar affine scheme over $\mathrm{Spec}({\mathbb Z})$", but I'm not 100% sure). In order for one law to imply (resp. be equivalent to) another, the corresponding scheme must contain (resp. be equal to) the other scheme, which in principle should recover a large fraction of the entire set of anti-implication (it might be nice to actually compute this coarser implication graph of linear magma implication and see how it compares with the full implication graph - I've set up equational#364 for this in case someone is interested).

This comports well with the previous intuition that the number of variables k determines a lot of the behavior. Indeed:

• If k=1, then we have one equation and the scheme is a (possibly reducible) curve (except when dealing with the trivial equation x = x, in which case the scheme is the entire plane).
• If k=2, then except in some degenerate circumstances (such as the commutative law x ◇ y = y ◇ xthe scheme is 0-dimensional - basically a finite set of points, with some ramification at small primes due to some discriminant or resultant having all coefficients divisible by the a non-trivial greatest common divisor.
• If k>2, then one expects the scheme to be empty, suggesting (but not proving conclusively) that the law is equivalent to the singleton law.

Some simple examples of schemes associated to laws:

• The constant law x ◇ y = z ◇ w is associated to the origin a=b=0 (degenerate behavior).
• The idempotent law x = x ◇ x is associated to the line a+b=1.
• The commutative law x ◇ y = y ◇ x is associated to the line a=b (degenerate behavior).
• The associative law (x ◇ y) ◇ z = x ◇ (y ◇ z) is associated to the four-point set a(a-1)=b(b-1)=0 (degenerate behavior).
• The left absorption law x = x ◇ y is associated to the line b=0.

I think that one should be able to describe these schemes and identify the linear implication graph using the classical theory of resultants (so the full power of Groebner bases is not required). In any case we now have a way to assign a geometric object (a planar affine scheme) to each law that serves as a first approximation as to where that law should be located in the implication graph. (One could eventually update the equation explorer to add this geometric object to the web page associated to each equation... I'll add that to the previous task.)

[Will Sawin]

Terence Tao said:

• If k>2, then one expects the scheme to be empty, suggesting (but not proving conclusively) that the law is equivalent to the singleton law.
  

This seems not quite right. If k=3 we have three equations in two variables. The theory of resultants lets us compute from the coefficients of the equations a number such that if p divides that number then (at least generically) the equations have a common solution mod p. If I write a complicated expression in three variables than we should get high-degree polynomials so that this number is probably large and thus a solution mod p for some large-ish p should exist.

[Will Sawin]

Do there exist three-variable equations not currently known to be satisfied by any nontrivial 3-variable magma where one can test this approach?

[Terence Tao]

Ah, right, I forget how weird algebraic geometry gets at low characteristic. So even the "asymptotically empty" schemes have some interesting structure to them that continues to make them a useful invariant of a law.

By the way, I wanted to add one more example of a scheme attached to a law: the law x ◇ (y ◇ z) = (x ◇ y) ◇ w that inspired this whole project is associated to the two-point scheme a(a-1)=b=0, which helps explain why it lies between the constant law (associated to the scheme a=b=0) and the associative law (associated to the scheme a(a-1)=b(b-1)=0).

[David Renshaw]

equational#371 resolves 4 more implications with Z/11 models

[Nicholas Carlini]

I'll have a brute force run started shortly that should be able to go up fairly high. What other meta-data would be saved along with the run? The smallest (p, a, b) that satisfy each equation? Other things?

[Leo Shine]

Not sure how you're doing the brute force so not sure if it's obvious but you only need to check x=1 and y =0 and y=1 and x=0 in order to check an equation is satisfied I think(at least for primes)

[Will Sawin]

Terence Tao said:

Ah, right, I forget how weird algebraic geometry gets at low characteristic. So even the "asymptotically empty" schemes have some interesting structure to them that continues to make them a useful invariant of a law.

However, this might not be so relevant for this project: Unless each variable appears twice in the equation, we are forced to have a=0 or b=0 for the coefficient of that variable to cancel. This forces the magma to have a very simple form - the operation ignores one variable and viewed as a function on the other variable it's periodic. Presumably everything with a counterexample of this form was found already. The size limit of the project means if each variable appears at least twice then it appears exactly twice and there might not be so many remaining such examples that are undetermined.

[Will Sawin]

One can consider more general rings where a,b may be nilpotent or zero divisors without being zero. In none of the examples I tried did this help but maybe there are some where it does.

[Nicholas Carlini]

Leo Shine said:

Not sure how you're doing the brute force so not sure if it's obvious but you only need to check x=1 and y =0 and y=1 and x=0 in order to check an equation is satisfied I think(at least for primes)

Just to clarify notation, you're saying that the constants "x" and "y" in operator op(a, b) = x*a + y*b mod p. Not the variables we've called x and y (and z,w,u,v)

[Terence Tao]

I believe he actually meant the variables: to check whether two linear forms ax+by, cx+dy agree, it suffices to check them at generators (x,y) = (1,0), (0,1). This is probably about as fast as just computing the coefficients directly.

[Nicholas Carlini]

OK. That makes more sense. I'm starting with a brute force over everything for now and can revisit this later

[Terence Tao]

Will Sawin said:

One can consider more general rings where a,b may be nilpotent or zero divisors without being zero. In none of the examples I tried did this help but maybe there are some where it does.

For the central groupoid law https://teorth.github.io/equational_theories/implications/?168 the scheme is a^2 = b^2 = 0; 2ab = 1 which unfortunately collapses to the uninteresting empty set (multiply the last equation by a or b), but it did at least have a chance of containing nilpotents. EDIT: but maybe the non-commutative scheme a^2 = b^2 = 0; ab+ba = 1 is more interesting?

[Terence Tao]

By the way I just wanted to point out that we have recovered an old result of Austin https://www.jstor.org/stable/2035753?seq=1 that any law with at most 2 variables has non-trivial finite models (in fact infinitely many such), with basically the same proof.

[Nicholas Carlini]

I haven't pulled since yesterday, but linear equations solves >443 unknowns since what we had last time I pulled. Rebuilding now and will let this run a while longer to see how it goes

[Nicholas Carlini]

Okay, so updating to the latest and it's down to 30 new ones. I've created #380 which introduces these. I think my counting may be wrong, I know it's at least 30, but it may be more. I'll be back later today and can both report status on the more complete run and diagnose what's going on here with counting.

[David Renshaw]

equational#380

[David Renshaw]

including one at ZMod 43. Nice!

[Nicholas Carlini]

It completed its search for all p^k <= 47

[Will Sawin]

which equation is ZMod 43 for?

[Leo Shine]

1076 according to PR

[Will Sawin]

I was trying to figure out "why 43 is necessary." I didn't quite figure it out. If I calculated right the equations are a^2b+a^2b^2=1 and a+ab^3+b^2=0 whose interesting solutions have b a root of b^4-b^3-b^2+b-1 which is an irreducible polynomial of degree 4, so writing down a solution over C is tricky, but it has solutions over smaller finite fields.

[Nicholas Carlini]

Ah okay so I'm not entirely sure that this is the first one that's necessary. I try to do some kind of set-cover like thing and that 43 is there might mean that it covers a larger set of things and that's why it's there

[Nicholas Carlini]

I'm running into a problem now though if one of you lean experts have an idea. I've sped up my algorithm by quite a bit and have brute forced up to Z/199Z but now Lean is taking forever to prove just saying "by decide!" which I read to mean "I give up just brute force it or something". Is there some faster way to show lean some of these are true/false? It's been building for 10 minutes with no end in sight

[David Renshaw]

I wonder if the memoFinOp thing would help?

[David Renshaw]

Switch from ZMod n to Fin n and put memoFinOp in front of your fun

[Joachim Breitner]

That can help if the operation itself is slow to reduce. But deciding an equation over Fin 43 requires 43^n tests, where n is the number of variables. I would not expect the kernel to be up for that.

Did you also try by native_decide?

[Will Sawin]

Joachim Breitner said:

That can help if the operation itself is slow to reduce. But deciding an equation over Fin 43 requires 43^n tests, where n is the number of variables. I would not expect the kernel to be up for that.

If that's the problem then couldn't Leo Shine's idea be the solution? https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/An.20old.20new.20idea/near/475110536 Checking only for the standard basis vectors reduces the 43^n tests to n.

[Joachim Breitner]

Sorry, not following closely. If there is a certain structure and you can prove the theorem that checking only certain values suffices, then you should be able to apply that theorem before using decide.

[Joachim Breitner]

Also, is there a reason this file uses decid!e and not decideFin!? Ah,the latter probably needs to learn about ZMod n in addition to Fin. This might help a bit with theorems with very many facts (but less so with theorems with a small number of facts)

[Joachim Breitner]

I won't be able to have a look today, but if no one beats me to it I should be able to make a tactic somewhen next week that recognizes and efficiently checks linear equations over ZMod n. Maybe near the end of the week, though.

[Nicholas Carlini]

I had a bug. (I overflowed int64 trying to be tricky). I don't have anything past Z/47Z but that's still rather slow to compile in lean. I have it running and will check back in a few hours if it's found anything else

[Nicholas Carlini]

Okay, going up to Z/169Z exclusively searching for new implications (restricting only to the ~300 equations that aren't solved) doesn't find anything new.

[Nicholas Carlini]

If I'm counting right, 13.3m implications are resolved with this approach

[Terence Tao]

That's pretty close to the 13.8m anti-implications that actually exist. So the linear implications are reasonably good at clearing out most anti-implications.

[Joachim Breitner]

Had a brief look, maybe the proof can be algebraic rather than calculational, and thus scale to large magmas easily.

It seems that ring can almost solve the positive facts, but it needs a little help reducing the constants. Here is a quick hack:

-- The following three lemmas help simp reduce constants in `ZMod n`, which together with
-- `ring` can solve positive facts.
-- The proofs are just quick ugly hacks. And the whole thing is maybe better
-- implemented as a simproc

theorem ZMod_reduce_constant0 (n : ℕ) [NeZero n] (x : Nat) (h : n = x + 2)  :
    @OfNat.ofNat (ZMod n) (x + 2) _ = 0 := by
  simp [OfNat.ofNat]
  apply ZMod.val_injective
  norm_num
  conv_lhs => equals ((x + 2 : Nat) : ZMod n) => simp
  conv_rhs => equals ((0 : Nat) : ZMod n) => simp
  apply (ZMod.natCast_eq_natCast_iff' _ _ _).mpr
  rw [h]
  simp

theorem ZMod_reduce_constant1 (n : ℕ) [NeZero n] (x : Nat) (h : n = x + 1)  :
  @OfNat.ofNat (ZMod n) (x + 2) _ = 1 := by
  simp [OfNat.ofNat]
  conv_lhs => equals ((x + 2 : Nat) : ZMod n) => simp
  conv_rhs => equals ((1 : Nat) : ZMod n) => norm_num
  apply (ZMod.natCast_eq_natCast_iff' _ _ _).mpr
  rw [h]
  cases x
  · simp
  · rw [Nat.mod_eq_sub_mod]
    simp
    omega

theorem ZMod_reduce_constant2 (n : ℕ) (x : Nat) (_h : n < x + 1)  :
  @OfNat.ofNat (ZMod n) (x + 2) _ = @OfNat.ofNat (ZMod n) (x % n + 2) _ := by
  simp only [OfNat.ofNat, Nat.cast_add, ZMod.natCast_mod]


@[equational_result]
theorem LinearInvariance0 : ∃ (G : Type) (_ : Magma G), Facts G [1076] [26, 65, 73, 102, 117, 125, 160, 167, 212, 229, 258, 263, 335, 362, 429, 437, 464, 473, 504, 513, 546, 562, 617, 632, 640, 679, 704, 826, 833, 872, 879, 910, 917, 949, 962, 1029, 1046, 1085, 1110, 1119, 1226, 1231, 1278, 1323, 1455, 1482, 1491, 1518, 1526, 1632, 1654, 1658, 1662, 1682, 1721, 1729, 1790, 1838, 1850, 1861, 1873, 1885, 1897, 1925, 1967, 2044, 2053, 2060, 2100, 2125, 2267, 2300, 2328, 2330, 2449, 2457, 2470, 2485, 2503, 2533, 2541, 2586, 2653, 2663, 2672, 2699, 2744, 2850, 2863, 2875, 2910, 2939, 3053, 3058, 3066, 3075, 3079, 3083, 3094, 3113, 3271, 3279, 3343, 3352, 3459, 3474, 3482, 3518, 3526, 3558, 3607, 3668, 3675, 3761, 3871, 3888, 3924, 3954, 4068, 4073, 4127, 4131, 4135, 4146, 4157, 4290, 4321, 4369, 4383, 4408, 4443, 4585, 4636, 4656] := by
  refine ⟨ZMod 43, { op := fun x y => 17 * x + 27 * y }, ?_⟩
  constructor
  · unfold Equation1076
    simp [Magma.op]
    ring_nf
    simp [ZMod_reduce_constant0, ZMod_reduce_constant1, ZMod_reduce_constant2]
  repeat' apply And.intro
  · intro h; have this := h 0 1; revert this; decide
  sorry

For the negative facts I guess the easiest plan is to write a tactic that detects the number of variables, and then just tries 0,1 and then 1,0 etc.

Or alternatively this could proceeds algebraically as in the positive case, yielding

⊢ ∃ x x_1, ¬x = x_1 * 26 + x * 18

which could be processed further, solving for x_1 (if this is in a finite field), and then eliminating the existential.

But maybe that’s not actually worth it, and a simple tactic that just plugs in the basis vectors and uses decide suffices.

Anyways, this plan should allow us to us rather large magmas with linear operators very efficiently.

[Joachim Breitner]

And it seems that simp already knows how to reduce Fin n constants, just not ZMod n constants, so presumably that’s just something that mathlib can fix:

import Mathlib

example (n : Fin 42) (P : Fin 42 → Prop): P (44 * n) := by
  simp
  guard_target = P (2 * n)
  sorry

example (n : ZMod 42) (P : ZMod 42 → Prop): P (44 * n) := by
  fail_if_success simp
  guard_target = P (44 * n)

[Joachim Breitner]

In particular this means that if you use Fin rather than ZMod then ring_nf; simp can solve the positive facts easily:

@[equational_result]
theorem LinearInvariance0 : ∃ (G : Type) (_ : Magma G), Facts G [1076] [26, 65, 73, 102, 117, 125, 160, 167, 212, 229, 258, 263, 335, 362, 429, 437, 464, 473, 504, 513, 546, 562, 617, 632, 640, 679, 704, 826, 833, 872, 879, 910, 917, 949, 962, 1029, 1046, 1085, 1110, 1119, 1226, 1231, 1278, 1323, 1455, 1482, 1491, 1518, 1526, 1632, 1654, 1658, 1662, 1682, 1721, 1729, 1790, 1838, 1850, 1861, 1873, 1885, 1897, 1925, 1967, 2044, 2053, 2060, 2100, 2125, 2267, 2300, 2328, 2330, 2449, 2457, 2470, 2485, 2503, 2533, 2541, 2586, 2653, 2663, 2672, 2699, 2744, 2850, 2863, 2875, 2910, 2939, 3053, 3058, 3066, 3075, 3079, 3083, 3094, 3113, 3271, 3279, 3343, 3352, 3459, 3474, 3482, 3518, 3526, 3558, 3607, 3668, 3675, 3761, 3871, 3888, 3924, 3954, 4068, 4073, 4127, 4131, 4135, 4146, 4157, 4290, 4321, 4369, 4383, 4408, 4443, 4585, 4636, 4656] := by
  refine ⟨Fin 43, { op := fun x y => 17 * x + 27 * y }, ?_⟩
  constructor
  · unfold Equation1076
    simp [Magma.op]
    ring_nf
    simp

[David Renshaw]

does the reduce_mod_char tactic help?

[Joachim Breitner]

https://github.com/teorth/equational_theories/pull/402 switches to Fin n so that simp reduces literals and that we can use decideFin!, packages the above into a little macro, and uses that to solve positive facts for larger magmas. 26→9s speed up building this file.
I hope this unblocks larger magmas from being included by @Nicholas Carlini .

[Pace Nielsen]

Doesn't taking (p,a,b)=(11,4,6) show 1076=/> 3?

[Nicholas Carlini]

My tool says 1076 fails (11,4,6) on (x,y)=(0,1)

[Nicholas Carlini]

Let me make sure it's right.

[David Renshaw]

x = y ◇ ((x ◇ (x ◇ y)) ◇ y)
x = ay + b(a(ax + b(ax + by)) + by)
x = ay + a²bx + a²b²x + ab³y + b²y

1 = a²b + a²b²  (coefficients of x)
0 = a + ab³ + b² (coefficients of y)

It looks to me like the coefficients of y fail to line up.

[Nicholas Carlini]

class Number:
    def __init__(self, number):
        self.number = number
    def __add__(self, other):
        return Number((4*self.number + 6*other.number)%11)
    def __str__(self):
        return str(self.number)

x = Number(0)
y = Number(1)
print(eval('y ◇ ((x ◇ (x ◇ y)) ◇ y)'.replace("◇", "+")))

[Nicholas Carlini]

(Gives 2, and 2 != 0)

[Pace Nielsen]

Oops, I made a miscalculation on this. Back to the drawing board.

[Nicholas Carlini]

As long as my code is correct (and double checking it today) there will exist no new linear solutions up to Z/200Z.

[Franklin Pezzuti Dyer]

Maybe this has already been said here - but I wonder if any new counterexamples can be found by considering x ◇ y = Ax + By for A, B arbitrary (possibly non-commuting) matrices

[Franklin Pezzuti Dyer]

I have been puzzling over the unresolved implication 63 <--> 1692 and thought to try this approach when the I didn't find any linear counterexamples over C. Sadly it didn't work for this specific pair of laws (the exact same pairs of matrices A, B make x ◇ y = Ax + By satisfy 63 as 1692) but I wonder whether this could be applied to any other implications...

[Will Sawin]

Franklin Pezzuti Dyer said:

I have been puzzling over the unresolved implication 63 <--> 1692 and thought to try this approach when the I didn't find any linear counterexamples over C. Sadly it didn't work for this specific pair of laws (the exact same pairs of matrices A, B make x ◇ y = Ax + By satisfy 63 as 1692) but I wonder whether this could be applied to any other implications...

The laws can be expressed as polynomial equations in the coefficients of A and B, so general nonsense means that if any pair of matrices over any field works to establish a non-implication between two magma laws then a pair of matrices over a finite field works to establish a non-implication which means there will be counterexamples for finite magmas. So this can't work for any implication known to hold for finite magmas. But other than that this potentially works.

[Will Sawin]

The dimension-counting arguments Terry was thinking about earlier still suggest that there will likely be interesting solutions for laws in two variables but not for more than two variables. Here the choice of finite field doesn't save you and give expected solutions in the three variable case. But are there any unknown implications left, not known to hold for finite magmas, where the source of the implication has two variables?

[Franklin Pezzuti Dyer]

No idea. I was finding implications to work on from the Equation Explorer - is there a way to filter out (in EE or elsewhere) the implications that are known/not known for finite magmas?

[Terence Tao]

I think in principle we might get some equations that are only solvable with infinite dimensional matrices and so not subject to the Lefschetz principle objection. A classical example is AB-BA=1 which is solvable in infinite dimensions (Heisenberg relations) but not finite ones (left-hand side has trace zero, right-hand side doesn't). I don't know if the noncommutative 63 equations have some exotic infinite dimensional solutions of this form though.

[Terence Tao]

Franklin Pezzuti Dyer said:

No idea. I was finding implications to work on from the Equation Explorer - is there a way to filter out (in EE or elsewhere) the implications that are known/not known for finite magmas?

We have a file https://github.com/teorth/equational_theories/blob/main/data/smallest_magma.txt that stores the size of the smallest nontrivial finite magma solving a given equation, so it implicitly will answer your question (up to numerical evidence), but it is not integrated into EE (maybe we should add it...)

[Terence Tao]

Wait this doesn't fully answer your question, it only lists whether an equation has a finite magma model, not whether an implication holds for finite models. We don't have systematic data on that, only isolated human generated results

[Terence Tao]

In principle we do have data on which of the anti-implications arise from finite models, and perhaps we could remove this from the set of all anti-implications and get a relatively small set of anti-implications (a couple thousand perhaps) that are only known via infinitary techniques such as saturation, or a small number of human-coded infinite models. But we don't have tooling to easily recover this.

In the medium term, we could develop an enriched version of the transitive closure tooling that lists, for a given implied implication, the specific explicit implications that were used to establish it, and also their locations in te Lean files where they live. Then one could manually see, for any given implication, whether for instance it was disproven using a finite magma. The list of issues is getting a bit long, but perhaps I will list this as a medium term issue.

[Pace Nielsen]

I've run through a bunch of the equations involved in open implications, plugging in ax+by+c for the operation, and then finding a reduction system for the resulting relations over noncommutative rings (using Bergman's diamond lemma from ring theory). Each time, the relations have resulted in a,b commuting, occasionally with a+b=1. I'm not sure why the current batch of equations leads to commuting coefficients. (On the other hand, c doesn't commute with a,b, it is often a zero-divisor, but so far also hasn't provided any useful leverage.) The reduction systems are very simple to find and describe. So if anyone has a favorite equation # where they want me to give the full reduction system in terms of a,b,c, just post the number here and I'll get to it.

[Terence Tao]

Even if it is a largely negative result, this is a useful empirical data point to have - it's not intuitively obvious that the noncommutative linear models aren't significantly more powerful as anti-implication generation machines than the commutative linear models, so this is worth knowing.

[Will Sawin]

and the situation may totally flip applying similar ideas to a variant problem, for example the version where the equations are allowed to have five multiplications. Maybe in that case the noncommutative algebra method will resolve a lot of cases other methods don't.

[Will Sawin]

Terence Tao said:

In the medium term, we could develop an enriched version of the transitive closure tooling that lists, for a given implied implication, the specific explicit implications that were used to establish it, and also their locations in te Lean files where they live. Then one could manually see, for any given implication, whether for instance it was disproven using a finite magma. The list of issues is getting a bit long, but perhaps I will list this as a medium term issue.

A possibly more pressing issue is the reverse of what you are discussing, which is to know which of the implications that are currently unknown can be proven relatively easily for finite magmas. This would require generalizing and systematizing some of the arguments people have already made.