A complex Hadamard matrix of order 94 exists (Szöllősi 2026) — kernel-attested structural core: the Example-1 circulant quadruple (A,B,C,D, order 47, {−1,1}) satisfies A A^T+B B^T+C C^T+D D^T = 188·I with A,B symmetric (Theorem 4)

Enuntiatio — the claim

A complex Hadamard matrix of order 94 exists (Szöllősi 2026) — kernel-attested structural core: the Example-1 circulant quadruple (A,B,C,D, order 47, {−1,1}) satisfies A A^T+B B^T+C C^T+D D^T = 188·I with A,B symmetric (Theorem 4)

Refuted by a nonzero shift s∈[1,47) at which the summed periodic autocorrelations of A,B,C,D are nonzero (or ≠188 at s=0), or an asymmetry in A or B — breaking the Theorem-4 construction hypothesis

Expressio — the formal statement

set_option maxHeartbeats 0
set_option maxRecDepth 1000000

def rot (x : List Int) (s : Nat) : List Int := x.drop s ++ x.take s
def dotf (u v : List Int) : Int := (List.zipWith (fun a b => a * b) u v).foldl (fun t a => t + a) 0
def autocorr (x : List Int) (s : Nat) : Int := dotf x (rot x s)

def eq1 (a b c d : List Int) : Bool :=
  (List.range 47).all (fun s => autocorr a s + autocorr b s + autocorr c s + autocorr d s == (if s == 0 then 188 else 0))

def symrow (x : List Int) : Bool := (List.range 47).all (fun k => x.getD k 0 == x.getD ((47 - k) % 47) 0)

def a1 : List Int := [1, 1, 1, 1, -1, 1, -1, 1, 1, -1, -1, -1, 1, -1, 1, 1, -1, -1, -1, -1, -1, 1, 1, 1, 1, 1, 1, -1, -1, -1, -1, -1, 1, 1, -1, 1, -1, -1, -1, 1, 1, -1, 1, -1, 1, 1, 1]
def b1 : List Int := [1, 1, -1, 1, -1, 1, 1, 1, -1, 1, -1, 1, 1, -1, -1, -1, 1, 1, -1, -1, 1, -1, 1, 1, 1, 1, -1, 1, -1, -1, 1, 1, -1, -1, -1, 1, 1, -1, 1, -1, 1, 1, 1, -1, 1, -1, 1]
def c1 : List Int := [1, 1, 1, 1, 1, 1, 1, 1, 1, -1, -1, -1, 1, 1, -1, 1, -1, 1, 1, -1, -1, 1, -1, -1, -1, -1, -1, 1, -1, -1, 1, 1, -1, 1, 1, 1, 1, -1, 1, 1, 1, -1, -1, 1, -1, 1, -1]
def d1 : List Int := [1, 1, 1, 1, 1, 1, -1, -1, 1, 1, 1, 1, -1, 1, 1, -1, 1, -1, 1, -1, -1, 1, 1, -1, 1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, 1, 1, -1, -1, -1, 1, 1, -1, 1, 1, -1, -1]

theorem had94_witness1 : (eq1 a1 b1 c1 d1 && symrow a1 && symrow b1) = true

Demonstratio — the kernel-checked proof

by decide