AIM + Nuclear Squares

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Last updated: May 13, 2026

Background

Which subsets of the 3 Nuclear Squares properties suffice to prove the 7 goals of the strong AIM conjecture?

The 7 goals are as follows.

   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").
   K(a(x,y,z),u) = 1              # label("Ka").

   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").

From previous results, it suffices to prove any one of the single-a goals {aK1,aK2,aK3,Ka} plus any one of the double-a goals {aa1,aa2,aa3}.

Results

Case 1: Assume all 3 properties

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 2: NucSq_l + NucSq_m

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 3: NucSq_m + NucSq_r

   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 4: NucSq_l + NucSq_r

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Proof of aK1 assuming aa1: (in, out, pf, xml)

Proof of aa1 assuming aK1: (in, out, pf, xml)

Case 5: NucSq_l alone

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").

Here is a proof that assuming the single-a goals suffices to prove the double-a goals.

Case 6: NucSq_m alone

   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").

Here is a proof that assuming the double-a goals suffices to prove the single-a goals.

Case 7: NucSq_r alone

   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Proof of aK3: proof

Proof of aK1 assuming aa1: (in, out, pf, xml)

Proof of aa1 assuming aK1: (in, out, pf, xml)

This, together with the proof of aK3, suffices to complete the proof of all 7 goals of strong AIM conjecture.