Family Bauer–Furuta invariant, Exotic Surfaces and Smale conjecture

We establish the existence of a pair of exotic surfaces in a punctured K3 which remains exotic after one external stabilization and have diffeomorphic complements. A key ingredient in the proof is a vanishing theorem of the family Bauer–Furuta invariant for diffeomorphisms on a large family of spin 4-manifolds, which is proved using the tom Dieck splitting theorem in equivariant stable homotopy theory. In particular, we prove that the S^1-equivariant family Bauer–Furuta invariant of any orientation-preserving diffeomorphism on S^4 is trivial and that the Pin(2)-equivariant family Bauer–Furuta invariant for a diffeomorphism on S^2 × S^2 is trivial if the diffeomorphism acts trivially on the homology. Therefore, these invariants do not detect exotic self-diffeomorphisms on S^4 or S^2 × S^2. Furthermore, our theorem also applies to certain exotic loops of diffeomorphisms on S^4 (as recently discovered by Watanabe) and show that these loops have trivial family Bauer–Furuta invariants. En route, we observe a curious element in the Pin(2)-equivariant stable homotopy group of spheres which could potentially be used to detect an exotic diffeomorphism on S^4.