Hadamard conjecture: the Paley-II-times-power-of-two case

This is the case of the Hadamard conjecture reachable by combining Paley's second construction with Sylvester's doubling construction via the Kronecker-product multiplicativity theorem.

Suppose $k$ is a natural number for which there exist a prime $q \equiv 1 \pmod 4$ and a natural number $t$ with

Then there exists a $4k \times 4k$ matrix $M$ with every entry $1$ or $-1$ attaining Hadamard's determinant bound $|\det M| = (4k)^{4k/2}$.

Proof idea. Paley's second construction (Paley_construction_II, applied to the finite field $\mathbb Z/q\mathbb Z$) gives a Hadamard matrix of order $2(q+1)$; Sylvester's doubling construction gives one of order $2^{t}$. The Kronecker-product multiplicativity theorem (Hadamard_matrix_kronecker_product) combines them into one of order $2(q+1)\cdot2^{t} = 4k$.

This theorem is the Paley-II analogue of Hadamard_Conjecture_paley_sylvester_case (which uses Paley's first construction, $q\equiv3\pmod4$, order $q+1$). Together they cover further $k$ not reachable by either construction alone — for instance $q=5,13,17,29$ (each $\equiv1\pmod4$) give base orders $12,28,36,60$, i.e. $k=3,7,9,15$ and all their doublings.

As with the Paley-I case, this theorem is intended as one branch of a finer case split refining Hadamard_Conjecture_residual; it does not by itself close the Hadamard conjecture.

Formalization Note The determinant bound $|\det M|=(4k)^{4k/2}$ follows internally from the orthogonality identity $MM^{\mathsf T}=4kI_{4k}$ via $(\det M)^2=\det(MM^{\mathsf T})=(4k)^{4k}$ and evenness of $4k$.