Tagewerk XXXII

Kernel-attested complex Hadamard matrix of order 94 (Szöllősi 2026)

A 2026 existence resolution in a domain new to the ledger — complex Hadamard matrices — independently reconstructed and kernel-attested. A complex Hadamard matrix of order n is an n x n matrix with entries in {1,-1,i,-i} and H H* = n I; whether one exists in order 94 was open. Szollosi (arXiv:2603.09572) settles it (Theorem 1) by a Goethals-Seidel-style construction: four circulant {-1,1}-matrices A,B,C,D of order 47, with A,B symmetric and A A^T+B B^T+C C^T+D D^T = 188 I, assemble (with R the back-diagonal) into a complex Hadamard matrix of order 94. The hard part is the computer search for the four sequences; verification is exact and self-certifying (the search is not part of the certificate). Leibniz reconstructs A,B,C,D from the length-47 rows printed in the paper — both Example 1 and, independently, Example 2 — and verifies by exact integer arithmetic: the published anchors (row sums 3,7,7,9 / -1,-5,9,9 and summed autocorrelation norm 796 / 1116, peaks 14 / 18), that A,B are symmetric, that A A^T+B B^T+C C^T+D D^T = 188 I, and that the assembled 94x94 matrix is unimodular in {1,-1,i,-i} and satisfies H H* = 94 I — i.e. a complex Hadamard matrix of order 94 (both examples). The Lean 4.31 kernel re-decides the finite structural core by plain decide: eq (1) written as the vanishing of the summed periodic autocorrelations at every nonzero shift (equivalent, since the four Gram matrices are circulant, and far cheaper than the dense 188x188 product) plus the symmetry of A,B — exactly the hypotheses Theorem 4 turns into the order-94 matrix — for both examples, with a negative control (one flipped sign breaks eq (1)); every theorem depends on at most [propext]. The dense 94x94 H H* = 94 I is carried by the exact integer procedure. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact integer arithmetic and the kernel decide.