Parity obstruction for Miyamoto C2 ingredients

Hadamard constructions seek square ±1 matrices with pairwise orthogonal rows. The scoped targets are eight explicit orders—2884, 4532, 7004, 7172, 7828, 8476, 9476 and 11948—via Cooper–Wallis ingredients, and the validity of Miyamoto’s displayed C2 ingredient outside block orders 1 mod 4.

Why it matters and what counts as progress

Why it matters: It combines exact existence questions with identifying where a proposed construction ingredient cannot work.

What counts as progress: New exact Hadamard constructions from valid ingredients, or a proof identifying impossible C2 block orders; an invalid ingredient cannot establish a matrix order.

How the problem developed

1991 · Construction [1]
Miyamoto Published a construction of Hadamard matrices using a C₂-matrix ingredient; later work asks which block orders can realize the displayed ingredient.
18 Oct 2026 · Formalized result [2]
JD Jones Reported a parity argument excluding Miyamoto’s displayed C₂ ingredient at positive block orders not congruent to 1 modulo 4, alongside formalized Cooper–Wallis constructions at eight orders.

AI contribution

AI-assisted Hadamard constructions cover eight orders

Using periodic T-matrix quadruples of orders 103 and 163 and symmetric-circulant Williamson quadruples of orders 7, 11, 13, 17, 19, 23 and 29, a formalized Cooper–Wallis construction gives Hadamard matrices at orders 2884, 4532, 7004, 7172, 7828, 8476, 9476 and 11948. A separate parity result rules out Miyamoto’s displayed C2-matrix ingredient at positive block orders not congruent to 1 mod 4.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4/Mathlib kernel with finite decide checks, transitive axiom audit and Comparator statement matching)

Human understandingFew