Nonexistence of (243,121,60) difference sets in C3 × C9 × C9

We prove, by exhaustive computation, that no $(243,121,60)$ difference set exists in $C_3\times C_9\times C_9$. Keita Baba settled this case first on October 4, 2026, by a SAT computation with a certificate accepted by a formally verified checker. We give an independent proof by a different method: a lifting search with the reduction checked in Lean. A difference set with these parameters is a 121-element subset whose ordered differences represent every nonzero group element exactly 60 times. Vera López and García Sánchez recorded this group-specific case as unresolved, and Gordon singled it out in his presentation on the La Jolla Difference Set Repository. The reduction builds on the classical multiplier and character methods of Hall, Menon and Turyn and the multiplier searches of Vera López and García Sánchez. A multiplier-fixed translate has thirteen points in the subgroup of elements annihilated by three. Moment identities, singleton congruences and affine normalizations reduce the problem to eight quotient multiplicity arrays. Complete ternary lifting searches exclude all eight. Lean proves the algebraic reduction, normalization, lifting coverage and pruning lemmas; the final formal nonexistence theorem assumes the search assertions established by the external integer computations.

Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.