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

This is the case of the Hadamard conjecture reachable by combining Paley's 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 3 \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 construction (Paley_construction_I, applied to the finite field $\mathbb Z/q\mathbb Z$) gives a Hadamard matrix of order $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 $(q+1)\cdot 2^{t} = 4k$.

This theorem, together with the case $k = 2^m$ (settled unconditionally by Sylvester's construction alone in the Hadamard_Conjecture proof-sketch) and a further residual case, is intended as one branch of a finer case split refining Hadamard_Conjecture_nonpoweroftwo; it does not by itself close the Hadamard conjecture, since infinitely many $k$ satisfy neither hypothesis (e.g. $k$ for which $4k$ has no divisor of the form $q+1$ with $q$ prime, $q \equiv 3 \pmod 4$).

Formalization Note Since every Hadamard matrix of order $4k$ has an underlying orthogonality identity $MM^{\mathsf T} = 4kI_{4k}$, the determinant bound $|\det M| = (4k)^{4k/2}$ follows from $(\det M)^2 = \det(MM^{\mathsf T}) = (4k)^{4k}$ and evenness of $4k$; this conversion is internal to the proof and not part of the statement.