February 2022

AIM Loops (clause representation)

formulas(assumptions).

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x \ (x * y) = y.
   x * (x \ y) = y.
   (x * y) / y = x.
   (x / y) * y = x.

   % associator (right associated * a = left associated)
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

   % commutator ( (x * y) * K(y,x) = y * x )
   (x * y) \ (y * x) = K(y,x) # label("commutator").

   % inner mappings
   (y * x) \ (y * (x * u)) = L(u,x,y).
   ((u * x) * y) / (x * y) = R(u,x,y).
   x \ (u * x) = T(u,x).

   % abelian inner mapping group
   T(T(u,x),y) = T(T(u,y),x).
   T(L(u,x,y),z) = L(T(u,z),x,y).
   T(R(u,x,y),z) = R(T(u,z),x,y).
   L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
   L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
   R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.

Weak AIM Conjecture

AIM loops are nilpotent of class 3.

Status:

• Proved with a high-level mathematical argument.

• Challenge: Prove with Prover9.

• Status of 32 goals sufficient to prove that AIM loops are nilpotent of class 3.

• the 8 having > 1 occurrence of K are lemmas

  (in, out, pf, xml)

• nil3 15 => the remaining 14 of 15 having exactly 1 occurrence of K

  (in, out, pf, xml)

• aK1 + nil3 24 => the remaining 8/32 nil3 clauses having 0 occurrences of K.

  (in, out, pf, xml)

• Since aK1 trivially => nil3 15, it follows that aK1 + nil3 24 => nilpotency class 3.

Strong AIM Conjecture

formulas(goals).

   % aK (or "single-a") goals
   K(a(x,y,z),u) = 1     # label("Ka").
   a(K(x,y),z,u) = 1     # label("aK1").
   a(x,K(y,z),u) = 1     # label("aK2").
   a(x,y,K(z,u)) = 1     # label("aK3").

   % aa (or "double-a") goals
   a(a(x,y,z),u,w) = 1   # label("aa1").
   a(x,a(y,z,u),w) = 1   # label("aa2").
   a(x,y,a(z,u,w)) = 1   # label("aa3").

end_of_list.

Single-a Goals

• The 4 goals are equivalent.

• Proved for several special cases.

• Equality relationships between the single-a goal terms

Double-a Goals

• The 3 goals are equivalent.

• Proved for several special cases.

• Example next step challenge: middle Bol + KK => aa1.

     x * ((y * z) \ x) = (x / z) * (y \ x)    # label("middle Bol").
     K(K(x,y),z) = 1                          # label("KK").
  

• Another example challenge: AIM => any aai_eq_aaj.

• Results assuming middle Bol as an extra assumption