Lemmas on circulant Hadamard matrices

This file contains preliminary lemmas used in the theory of circulant Hadamard matrices.

Main results

• isRootOfUnity_of_isIntegral_of_norm_eq_one: Lemma 8. If θ is an algebraic integer in a number field K such that every conjugate of θ (i.e., every image under an embedding K →+* ℂ) has absolute value 1, then θ is a root of unity.

• kronecker_isRootOfUnity_of_cyclotomic: Theorem 9 (Kronecker). If K is a cyclotomic extension of ℚ and α ∈ K is an algebraic integer with |α| = 1 (under some embedding), then α is a root of unity.

• CirculantHadamard.cyclotomic_two_pow_succ_eq : The 2^(k+1)-th cyclotomic polynomial equals X^(2^k) + 1.

• CirculantHadamard.irreducible_cyclotomic_two_pow : The polynomial cyclotomic (2^k) ℚ is irreducible.

• CirculantHadamard.irreducible_X_pow_two_pow_add_one : The polynomial X^(2^k) + 1 is irreducible over ℚ.

• no_circulant_hadamard_pow_two: Theorem 1. There is no circulant Hadamard matrix of order 2^k for k ≥ 3.

Proof dependency chain for Theorem 1

The main theorem no_circulant_hadamard_pow_two uses exists_sum_eq_diff, which instantiates a cyclotomic field and applies:

• Corollary 7 (circulantHadamard_eigenvalue_ratio_integral): eigenvalue divisibility
• coeff_extraction_from_eigenvalue_divisibility: power-basis extraction

Corollary 7 transitively depends on:

• Lemma 6 (circulantHadamard_eigenvalue_factorization)
• Equation (3) (eigenvalue_product_eq)
• Lemma 4 (two_eq_zeta_sub_one_pow_mul_unit, zeta_sub_one_prime_two_pow)
• Lemma 5 (card_quotient_zeta_sub_one_eq_two)
• Equations (1)+(2) (prod_eigenvalueOI_eq_pm_pow via prod_eigenvalueOI_eq_algebraMap_det)

References

This corresponds to Lemmas 2–8, Theorem 9, and Theorem 1 in the textbook (Chapter 16).

theorem isRootOfUnity_of_isIntegral_of_norm_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : K} (hθ_int : IsIntegral ℤ θ) (hθ_norm : ∀ (φ : K →+* ℂ), ‖φ θ‖ = 1) : ∃ (n : ℕ) (_ : 0 < n), θ ^ n = 1

Lemma 8. If θ is an algebraic integer in a number field K such that all its conjugates (images under embeddings K →+* ℂ) have absolute value 1, then θ is a root of unity: there exists a positive integer n with θ ^ n = 1.

The proof uses a pigeonhole argument: since θ^m is an algebraic integer whose conjugates are all on the unit circle for every m, its minimal polynomial has integer coefficients bounded by a function of the degree. Hence there are finitely many possibilities for minimal polynomials, so θ^m = θ^{m'} for some m ≠ m', giving θ^{m-m'} = 1.

theorem CirculantHadamard.cyclotomic_two_pow_succ_eq {R : Type u_1} [CommRing R] (k : ℕ) : Polynomial.cyclotomic (2 ^ (k + 1)) R = Polynomial.X ^ 2 ^ k + 1

The 2^(k+1)-th cyclotomic polynomial equals X^(2^k) + 1. This is the specialization of cyclotomic_prime_pow_eq_geom_sum to p = 2.

theorem CirculantHadamard.irreducible_cyclotomic_two_pow (k : ℕ) : Irreducible (Polynomial.cyclotomic (2 ^ k) ℚ)

Lemma 2. The polynomial cyclotomic (2^k) ℚ is irreducible.

The book states: p_k(x) = x^{2^{k-1}} + 1 = Φ_{2^k}(x) is irreducible over ℚ. This follows from the general fact that all cyclotomic polynomials are irreducible over ℚ.

theorem CirculantHadamard.irreducible_X_pow_two_pow_add_one (k : ℕ) : Irreducible (Polynomial.X ^ 2 ^ k + 1)

The polynomial X^(2^k) + 1 is irreducible over ℚ. This is Lemma 2 stated directly in terms of the polynomial X^(2^k) + 1.

Lemma 4: Factorization of 2 in ℤ[ζ_{2^k}]

The book states (Lemma 4): Let n = 2^k (k ≥ 3) and ζ = e^{2πi/n}, a primitive n-th root of unity. Then 2 = (1-ζ)^{n/2} · u for some unit u in ℤ[ζ]. Moreover, (1-ζ) generates a prime ideal.

We formalize this using Mathlib's cyclotomic field machinery. The cyclotomic extension {2^(k+1)} corresponds to the book's n = 2^(k+1). The key results are:

• (ζ-1) is a prime element in 𝓞 K
• The ideal (2) equals (ζ-1)^{2^k} (i.e., totally ramified)
• As elements: 2 = (1-ζ)^{2^k} · u for a unit u

theorem CirculantHadamard.isPrime_span_zeta_sub_one_two_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : (Ideal.span {hζ.toInteger - 1}).IsPrime

Lemma 4 (Primality, ideal version). The ideal generated by (ζ - 1) is a prime ideal in the ring of integers 𝓞 K. This says that (1-ζ) generates a prime ideal above 2.

theorem CirculantHadamard.zeta_sub_one_prime_two_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Prime (hζ.toInteger - 1)

Lemma 4 (Primality, element version). In a 2^(k+1)-th cyclotomic field K, the element (ζ - 1) is prime in the ring of integers 𝓞 K.

theorem CirculantHadamard.finrank_cyclotomic_two_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] : Module.finrank ℚ K = 2 ^ k

The degree [K : ℚ] of a 2^(k+1)-th cyclotomic field equals 2^k. This follows from φ(2^(k+1)) = 2^k.

theorem CirculantHadamard.ideal_span_two_eq_span_zeta_sub_one_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {2}) = Ideal.span {hζ.toInteger - 1} ^ 2 ^ k

Lemma 4 (Ideal factorization). The ideal (2) in 𝓞 K equals ⟨ζ - 1⟩^{2^k}. This says 2 is totally ramified in the 2^(k+1)-th cyclotomic field: the ideal generated by 2 factors as the 2^k-th power of the prime ideal ⟨ζ - 1⟩.

In the book's notation with n = 2^(k+1): the ideal (2) = (1-ζ)^{n/2}.

theorem CirculantHadamard.associated_two_zeta_sub_one_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Associated ((algebraMap ℤ (NumberField.RingOfIntegers K)) 2) ((hζ.toInteger - 1) ^ 2 ^ k)

Lemma 4 (Element factorization, Associated form). In 𝓞 K, the element 2 is associated to (ζ - 1)^{2^k}. This is the element-level version of the ideal factorization.

theorem CirculantHadamard.two_eq_zeta_sub_one_pow_mul_unit (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : ∃ (u : (NumberField.RingOfIntegers K)ˣ), (algebraMap ℤ (NumberField.RingOfIntegers K)) 2 = (hζ.toInteger - 1) ^ 2 ^ k * ↑u

Lemma 4 (Element factorization, Unit form). There exists a unit u in 𝓞 K such that (2 : 𝓞 K) = (ζ - 1)^{2^k} * u.

This is the book's equation (4): 2 = (1-ζ)^{n/2} · u, where n = 2^(k+1) and u is a unit.

theorem CirculantHadamard.card_quotient_zeta_sub_one_eq_two (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Nat.card (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1}) = 2

Lemma 5 (Residue field). The quotient ring 𝓞 K / ⟨ζ - 1⟩ has cardinality 2, i.e., the residue field at the prime (1-ζ) is F₂.

Since 2 is totally ramified in the cyclotomic field K = ℚ(ζ_{2^{k+1}}), the ramification index e = 2^k = [K : ℚ], which forces the residual degree f = 1. Hence the residue field has p^f = 2^1 = 2 elements.

theorem kronecker_isRootOfUnity_of_cyclotomic {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {α : K} (hα_int : IsIntegral ℤ α) (φ₀ : K →+* ℂ) (hα_norm : ‖φ₀ α‖ = 1) : ∃ (m : ℕ) (_ : 0 < m), α ^ m = 1

Theorem 9 (Kronecker). Let τ be any root of unity and α ∈ ℚ(τ) with |α| = 1. Then α is a root of unity.

More precisely, if K is a cyclotomic extension of ℚ (hence a number field with abelian Galois group), and α ∈ K is an algebraic integer with |α| = 1 under some embedding φ₀ : K →+* ℂ, then α is a root of unity.

The proof uses the fact that the Galois group Gal(K/ℚ) is abelian (isomorphic to (ℤ/nℤ)ˣ), so complex conjugation commutes with all automorphisms. From |α| = 1 under one embedding, we deduce |φ α| = 1 for all embeddings φ, and then apply Lemma 8 (isRootOfUnity_of_isIntegral_of_norm_eq_one).

Lemma 3: Eigenvalue absolute value

A circulant Hadamard matrix of order n has all eigenvalues of absolute value √n.

structure CirculantHadamardMatrix (n : ℕ) [NeZero n] : Type

A circulant Hadamard matrix of order n is specified by a function a : ZMod n → ℤ whose entries are ±1 and whose rows are pairwise orthogonal (the Hadamard condition).

• a : ZMod n → ℤ
• entries_sq (i : ZMod n) : self.a i ^ 2 = 1
• orthogonality (j : ZMod n) : ∑ i : ZMod n, self.a i * self.a (i + j) = if j = 0 then ↑n else 0

noncomputable def CirculantHadamardMatrix.eigenvalue {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) (ζ : ℂ) (j : ZMod n) : ℂ

The eigenvalue of a circulant Hadamard matrix H at index j, given a primitive n-th root of unity ζ, is γ_j = ∑ᵢ a_i · ζ^(ij).

theorem pow_zmod_val_add {n : ℕ} [NeZero n] (ζ : ℂ) (hζn : ζ ^ n = 1) (a b : ZMod n) : ζ ^ (a + b).val = ζ ^ a.val * ζ ^ b.val

Key lemma: if ζ^n = 1 then ζ^(a + b : ZMod n).val = ζ^a.val * ζ^b.val.

theorem circulantHadamard_eigenvalue_conj_mul {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) (ζ : ℂ) (hζ : IsPrimitiveRoot ζ n) (j : ZMod n) : (starRingEnd ℂ) (H.eigenvalue ζ j) * H.eigenvalue ζ j = ↑↑n

Core computation: conj(γ) * γ = n in ℂ.

The proof: γ_j * conj(γ_j) = (∑_i a_i ζ^{ij})(∑_k a_k ζ^{-kj}) = ∑_i ∑k a_i a_k ζ^{(i-k)j} = ∑d (∑i a_i a{i+d}) ζ^{dj} = n · δ{d,0} · ζ^0 + ∑{d≠0} 0 · ζ^{dj} = n.

theorem circulantHadamard_eigenvalue_abs {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) (ζ : ℂ) (hζ : IsPrimitiveRoot ζ n) (j : ZMod n) : ‖H.eigenvalue ζ j‖ = √↑n

Lemma 3. The eigenvalues of a circulant Hadamard matrix of order n have absolute value √n. Stated as: for any primitive n-th root of unity ζ and any j, |γ_j| = √n, i.e., ‖∑ a_i ζ^{ij}‖ = √n.

Proof. We compute |γ_j|² = n using the orthogonality condition, then take √.

def CirculantHadamardMatrix.toMatrix {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) : Matrix (ZMod n) (ZMod n) ℤ

The circulant matrix associated to a circulant Hadamard matrix H. The (i, j) entry is H.a (i - j), so row i is a cyclic shift of the first row.

theorem CirculantHadamardMatrix.toMatrix_mul_transpose {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) : H.toMatrix * H.toMatrix.transpose = ↑n • 1

The product of the circulant matrix with its transpose equals n • I. This follows directly from the orthogonality condition HH^T = nI.

theorem circulant_hadamard_det_sq {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) : H.toMatrix.det ^ 2 = ↑n ^ n

The square of the determinant of a circulant Hadamard matrix equals n^n. Proof: det(H)² = det(H) · det(Hᵀ) = det(H · Hᵀ) = det(n · I) = n^n.

Equation (2): Determinant of a circulant matrix equals the product of eigenvalues

The book states (Section 1, after defining the circulant matrix): "It is straightforward to compute that for 0 ≤ j < n the column vector [1, ζ^j, ζ^{2j}, ..., ζ^{(n-1)j}]^t is an eigenvector of A with eigenvalue a_0 + ζ^j a_1 + ζ^{2j} a_2 + ... + ζ^{(n-1)j} a_{n-1}."

"Hence det(A) = ∏{j=0}^{n-1} (a_0 + ζ^j a_1 + ... + ζ^{(n-1)j} a{n-1})."

The proof, while described as "straightforward", involves:

1. Verifying that the DFT columns are eigenvectors (a computation).
2. The DFT matrix (with entries ζ^{ij}) is invertible when ζ is a primitive n-th root of unity.
3. Therefore the circulant matrix is diagonalizable with eigenvalues γ_j, and det(circulant) = ∏ γ_j.

We prove the eigenvector property (step 1) and state the determinant formula.

noncomputable def CirculantHadamardMatrix.toMatrixℂ {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) : Matrix (ZMod n) (ZMod n) ℂ

The circulant matrix of a CirculantHadamardMatrix, viewed as a matrix over ℂ. Entry (i,j) = ↑(a(j - i)), matching the book's convention where the first row is [a_0, a_1, ..., a_{n-1}]. This is the cast of the ℤ-valued toMatrix composed with negation, since toMatrix uses entry a(i - j).

noncomputable def CirculantHadamard.dftCol {n : ℕ} (ζ : ℂ) (j : ZMod n) : ZMod n → ℂ

The DFT column vector: the j-th column of the DFT matrix is [1, ζ^j, ζ^{2j}, ...].

theorem CirculantHadamard.circulant_mulVec_dft_col {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) (ζ : ℂ) (hζ : ζ ^ n = 1) (j : ZMod n) : H.toMatrixℂ.mulVec (dftCol ζ j) = H.eigenvalue ζ j • dftCol ζ j

Eigenvector property. The DFT column vector [1, ζ^j, ζ^{2j}, ...] is an eigenvector of the circulant matrix H.toMatrixℂ with eigenvalue γ_j = H.eigenvalue ζ j.

This is the "straightforward computation" mentioned in the book.

Lemma 6: Eigenvalue factorization in ℤ[ζ]

The book states (Lemma 6): Each eigenvalue γ_j of a circulant Hadamard matrix of order n = 2^k can be written as γ_j = v_j · (1-ζ)^{h_j} where v_j is a unit in ℤ[ζ] and h_j ≥ 0.

The proof relies on:

• Equation (3): the product ∏ γ_j = ± n^{n/2} = ± 2^{2^{k-1}}
• Lemma 4: 2 = (1-ζ)^{n/2} · u (u a unit)
• Lemma 5: (1-ζ) is prime in 𝓞 K

The argument: since ∏ γ_j is associated to (1-ζ)^M for some M, and (1-ζ) is prime in the integral domain 𝓞 K, we iteratively extract (1-ζ) factors from the product (using that 𝓞 K/(1-ζ) ≅ F₂ is a domain). When the power of (1-ζ) on the RHS is exhausted, the remaining product is a unit, so each factor is a unit.

noncomputable def eigenvalueOI {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] (H : CirculantHadamardMatrix n) (ζ_int : NumberField.RingOfIntegers K) (j : ZMod n) : NumberField.RingOfIntegers K

The eigenvalue of a circulant Hadamard matrix H at index j, viewed as an element of the ring of integers 𝓞 K, given a root of unity ζ_int in 𝓞 K. γ_j = ∑ᵢ a_i · ζ_int^(i·j).

theorem dvd_of_dvd_mul_prime_right {R : Type u_1} [CommRing R] [IsDomain R] {p c b : R} (hp : Prime p) (hpc : ¬p ∣ c) (h : c ∣ b * p) : c ∣ b

In an integral domain, if p is prime and p ∤ c, then c ∣ b * p implies c ∣ b.

theorem dvd_of_dvd_mul_prime_pow_right {R : Type u_1} [CommRing R] [IsDomain R] {p c b : R} (hp : Prime p) (hpc : ¬p ∣ c) (M : ℕ) : c ∣ b * p ^ M → c ∣ b

Iterated version: if p prime, p ∤ c, and c ∣ b * p^M, then c ∣ b.

theorem zeta_pow_half_eq_neg_one (k : ℕ) (K : Type u_1) [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : hζ.toInteger ^ 2 ^ k = -1

ζ^{2^k} = -1 for a primitive 2^{k+1}-th root of unity. Since ζ is a primitive 2^{k+1}-th root, ζ^{2^k} is a primitive 2nd root of unity, hence = -1.

Helper lemmas for the circulant determinant = product of eigenvalues

theorem prod_eigenvalueOI_eq_algebraMap_det (k : ℕ) (K : Type u_1) [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : ∏ j : ZMod (2 ^ (k + 1)), eigenvalueOI H hζ.toInteger j = (algebraMap ℤ (NumberField.RingOfIntegers K)) H.toMatrix.det

theorem prod_eigenvalueOI_eq_pm_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : ∃ (s : ℤ), s ^ 2 = 1 ∧ ∏ j : ZMod (2 ^ (k + 1)), eigenvalueOI H hζ.toInteger j = (algebraMap ℤ (NumberField.RingOfIntegers K)) (s * 2 ^ ((k + 1) * 2 ^ k))

Equations (1)+(2). The product of eigenvalues of a circulant Hadamard matrix of order 2^(k+1) equals ± 2^((k+1) · 2^k) in 𝔼 K. Combines det(H) = ±n^{n/2} (from HHᵀ = nI) with ∏ eigenvalues = det(circulant) (DFT diagonalization).

theorem algebraMap_two_pow_eq_unit_mul_zeta_sub_one_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (N : ℕ) : ∃ (v : (NumberField.RingOfIntegers K)ˣ) (M : ℕ), (algebraMap ℤ (NumberField.RingOfIntegers K)) 2 ^ N = ↑v * (hζ.toInteger - 1) ^ M

Any power of 2 in 𝓞 K can be written as a unit times a power of (ζ-1).

theorem eigenvalue_product_eq (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : ∃ (u : (NumberField.RingOfIntegers K)ˣ) (M : ℕ), ∏ j : ZMod (2 ^ (k + 1)), eigenvalueOI H hζ.toInteger j = ↑u * (hζ.toInteger - 1) ^ M

theorem circulantHadamard_eigenvalue_factorization (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) (j : ZMod (2 ^ (k + 1))) : ∃ (h_j : ℕ) (v_j : (NumberField.RingOfIntegers K)ˣ), eigenvalueOI H hζ.toInteger j = ↑v_j * (hζ.toInteger - 1) ^ h_j

Lemma 6. Each eigenvalue γ_j of a circulant Hadamard matrix of order n = 2^(k+1) can be written as γ_j = v_j · (ζ - 1)^{h_j} where v_j is a unit in 𝓞 K and h_j ≥ 0.

Proof. Since 2 is a multiple of (1-ζ) by Lemma 4, we have by Equation (3) that ∏ γ_j = 0 in 𝓞 K/(ζ-1). Since 𝓞 K/(ζ-1) is a domain (by Lemma 5), some factor γ_j is divisible by (ζ-1). Divide this factor and the right-hand side of Equation (3) by (ζ-1), and iterate. We continue to divide until the right-hand side becomes a unit. Hence each factor has the form v·(ζ-1)^h where v is a unit.

theorem unit_mul_pow_dvd_unit_mul_pow {R : Type u_2} [CommMonoidWithZero R] (v₀ v₁ : Rˣ) (p : R) {h₀ h₁ : ℕ} (h_le : h₀ ≤ h₁) : ↑v₀ * p ^ h₀ ∣ ↑v₁ * p ^ h₁

Helper: unit * p^h₀ divides unit' * p^h₁ when h₀ ≤ h₁.

theorem circulantHadamard_eigenvalue_ratio_integral (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : eigenvalueOI H hζ.toInteger 1 ∣ eigenvalueOI H hζ.toInteger 0 ∨ eigenvalueOI H hζ.toInteger 0 ∣ eigenvalueOI H hζ.toInteger 1

Corollary 7. Either γ₀/γ₁ ∈ ℤ[ζ] or γ₁/γ₀ ∈ ℤ[ζ].

Formalized as: either eigenvalueOI H ζ_int 0 divides eigenvalueOI H ζ_int 1 or vice versa, in the ring of integers 𝓞 K. Divisibility in 𝓞 K is equivalent to the ratio being in 𝓞 K, which is the statement γ₀/γ₁ ∈ ℤ[ζ].

Proof. By Lemma 6, γ_j = v_j · (ζ-1)^{h_j} with v_j a unit. Then γ₀/γ₁ = (v₀/v₁) · (ζ-1)^{h₀-h₁}. Since v₀/v₁ is a unit, this is in ℤ[ζ] when h₀ ≥ h₁; otherwise γ₁/γ₀ ∈ ℤ[ζ].

Root of unity characterization in 2-power cyclotomic fields

Step (1) of the proof of Theorem 1: any root of unity in Q(ζ_{2^{k+1}}) is a power of ζ. This follows from Kronecker's theorem (Theorem 9) combined with a degree argument that rules out primitive roots of order 2^{k+2}.

theorem root_of_unity_eq_pow_zeta (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) {x : K} (hx : IsOfFinOrder x) : ∃ (i : ℕ), x = ζ ^ i

In a 2^{k+1}-th cyclotomic extension of ℚ, any element of finite order in K is a power of the primitive root ζ. This uses the fact that the only roots of unity in Q(ζ_{2^{k+1}}) are the 2^{k+1}-th roots, since -1 = ζ^{2^k}.

The proof: by dvd_of_isCyclotomicExtension, the primitive order l of x divides 2 · 2^{k+1} = 2^{k+2}. If l = 2^{k+2}, then φ(l) = 2^{k+1} > 2^k = [K:ℚ], contradicting [ℚ(x):ℚ] ≤ [K:ℚ]. Hence l | 2^{k+1}, so x^{2^{k+1}} = 1, and eq_pow_of_pow_eq_one gives x = ζ^i.

theorem root_of_unity_eq_pm_zeta_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (u : (NumberField.RingOfIntegers K)ˣ) (hu : ∃ m > 0, ↑u ^ m = 1) : ∃ (r : ℤ) (s : ℤ), s ^ 2 = 1 ∧ ↑u = (algebraMap ℤ (NumberField.RingOfIntegers K)) s * hζ.toInteger ^ r.natAbs

In the 2-power cyclotomic ring of integers, any root of unity is ±ζ^r. Since ζ^{2^k} = -1 in Q(ζ_{2^{k+1}}), any root of unity is simply a power of ζ. The ± sign is included for compatibility with the general statement (where n might be odd and -1 would not be a power of ζ).

Eigenvalue ratio is ±ζ^r

By Corollary 7, γ₀/γ₁ (or γ₁/γ₀) is in 𝓞 K. By the norm argument, this ratio has absolute value 1 under every embedding. By Kronecker's theorem, it is a root of unity, hence ±ζ^r.

theorem eigenvalueOI_map_eq_eigenvalue {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] (H : CirculantHadamardMatrix n) (ζ_int : NumberField.RingOfIntegers K) (σ : K →+* ℂ) (j : ZMod n) : σ ((algebraMap (NumberField.RingOfIntegers K) K) (eigenvalueOI H ζ_int j)) = H.eigenvalue (σ ((algebraMap (NumberField.RingOfIntegers K) K) ζ_int)) j

The image of eigenvalueOI under an embedding σ : K →+* ℂ equals the complex eigenvalue at σ(ζ). This bridges the ring-of-integers eigenvalue to the complex eigenvalue.

theorem dvd_ratio_isRootOfUnity (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) {a b : NumberField.RingOfIntegers K} (hdvd : a ∣ b) (ha : ∀ (σ : K →+* ℂ), ‖σ ((algebraMap (NumberField.RingOfIntegers K) K) a)‖ = √(2 ^ (k + 1))) (hb : ∀ (σ : K →+* ℂ), ‖σ ((algebraMap (NumberField.RingOfIntegers K) K) b)‖ = √(2 ^ (k + 1))) : ∃ (r : ℤ) (s : ℤ), s ^ 2 = 1 ∧ b = (algebraMap ℤ (NumberField.RingOfIntegers K)) s * hζ.toInteger ^ r.natAbs * a

If a ∣ b in 𝓞 K and both have the same nonzero norm under all embeddings, then the quotient c (with b = a * c) has ‖σ(c)‖ = 1 for every embedding σ, hence is a root of unity by Kronecker's theorem.

theorem eigenvalue_ratio_eq_pm_zeta_pow (k : ℕ) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : ∃ (r : ℤ) (s : ℤ), s ^ 2 = 1 ∧ eigenvalueOI H hζ.toInteger 0 = (algebraMap ℤ (NumberField.RingOfIntegers K)) s * hζ.toInteger ^ r.natAbs * eigenvalueOI H hζ.toInteger 1

Corollary 7 + Theorem 9. The eigenvalue ratio γ₀/γ₁ is ±ζ^r, i.e., γ₀ = (±ζ^r) · γ₁.

This is Step 2 of the proof of Theorem 1 (no circulant Hadamard matrix of order 2^k for k ≥ 3). The chain of reasoning is:

1. By circulantHadamard_eigenvalue_ratio_integral (Corollary 7), one eigenvalue divides the other in 𝓞 K.
2. The quotient c has |σ(c)| = 1 for every embedding σ (since both eigenvalues have the same absolute value √n by Lemma 3).
3. Since c is integral with all conjugates on the unit circle, kronecker_isRootOfUnity_of_cyclotomic (Theorem 9) shows c is a root of unity.
4. By root_of_unity_eq_pm_zeta_pow, c = ±ζ^r in the 2-power cyclotomic ring of integers.

Theorem 1: No circulant Hadamard matrix of order 2^k for k ≥ 3

The proof combines the eigenvalue theory above with a power-basis coefficient comparison argument. The key steps are:

1. (∑ aᵢ)² = n from the orthogonality condition.
2. By Corollary 7 + Kronecker (Theorem 9), γ₀ = ζ^{-r} · γ₁ for some r.
3. Expanding in the power basis {1, ζ, …, ζ^{n/2-1}} and comparing the constant coefficient yields ∑ aᵢ = aᵣ - a_{n/2+r} for some r.
4. Since each aᵢ = ±1, the RHS lies in {-2, 0, 2}, so (∑ aᵢ)² ≤ 4. But for k ≥ 3, n = 2^k ≥ 8, contradicting (∑ aᵢ)² = n.

theorem CirculantHadamardMatrix.a_eq_one_or_neg_one {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) (i : ZMod n) : H.a i = 1 ∨ H.a i = -1

Each entry of a circulant Hadamard matrix is ±1.

theorem CirculantHadamardMatrix.sum_sq_eq {n : ℕ} [NeZero n] (H : CirculantHadamardMatrix n) : (∑ i : ZMod n, H.a i) ^ 2 = ↑n

The square of the sum of entries equals the order.

theorem eigenvalue_zero_eq_sum (k : ℕ) (K : Type u_1) [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : eigenvalueOI H hζ.toInteger 0 = (algebraMap ℤ (NumberField.RingOfIntegers K)) (∑ i : ZMod (2 ^ (k + 1)), H.a i)

When j = 0, the eigenvalue γ₀ = ∑ᵢ aᵢ is the sum of all entries of H.

theorem eigenvalue_zero_sq (k : ℕ) (K : Type u_1) [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : eigenvalueOI H hζ.toInteger 0 ^ 2 = (algebraMap ℤ (NumberField.RingOfIntegers K)) (2 ^ (k + 1))

γ₀² = n from orthogonality: (∑ aᵢ)² = n follows from the Hadamard condition.

theorem sum_zmod_split_halves (k : ℕ) [NeZero (2 ^ (k + 1))] (R : Type u_1) [AddCommGroup R] (f : ZMod (2 ^ (k + 1)) → R) (gLo gHi : ℕ → R) (hlo : ∀ j ∈ Finset.range (2 ^ k), f ↑j = gLo j) (hhi : ∀ j ∈ Finset.range (2 ^ k), f ↑(j + 2 ^ k) = gHi j) : ∑ x : ZMod (2 ^ (k + 1)), f x = ∑ j ∈ Finset.range (2 ^ k), gLo j + ∑ j ∈ Finset.range (2 ^ k), gHi j

Splitting a sum over ZMod (2^(k+1)) into low and high halves.

theorem eigenvalueOI_one_expanded (k : ℕ) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : eigenvalueOI H hζ.toInteger 1 = ∑ j ∈ Finset.range (2 ^ k), (algebraMap ℤ (NumberField.RingOfIntegers K)) (H.a ↑j - H.a (↑j + ↑(2 ^ k))) * hζ.toInteger ^ j

Eigenvalue expansion. The eigenvalue γ₁ = eigenvalueOI H ζ 1 can be expanded in the power basis {1, ζ, …, ζ^{2^k-1}} using ζ^{2^k} = -1: γ₁ = ∑{j=0}^{2^k-1} (a_j - a{j+2^k}) · ζ^j.

This groups the 2^{k+1} terms of the eigenvalue sum into 2^k pairs, where the term at index j + 2^k contributes -a_{j+2^k} · ζ^j.

Connecting the algebraic number theory chain to Theorem 1

The proof of Theorem 1 relies on the following chain of results:

1. Corollary 7 (circulantHadamard_eigenvalue_ratio_integral): either γ₁ | γ₀ or γ₀ | γ₁ in 𝓞 K. This uses Lemma 6, which uses Lemma 4, Lemma 5, and Equations (1)–(3).
2. Lemma 3 (circulantHadamard_eigenvalue_abs): |γ_j| = √n, so the ratio has absolute value 1.
3. Theorem 9 (kronecker_isRootOfUnity_of_cyclotomic): the ratio, being an algebraic integer of absolute value 1 in a cyclotomic field, is a root of unity.
4. Root of unity characterization (root_of_unity_eq_pow_zeta): in Q(ζ_{2^{k+1}}), any root of unity is a power of ζ.
5. Coefficient extraction: Expanding γ₁ = ∑ aᵢζⁱ using ζ^{n/2} = -1 and comparing the constant coefficient of ζ^r · γ₁ against γ₀ = ∑ aᵢ gives ∑ aᵢ = aᵣ - a_{r+n/2}.

Steps 1–4 are fully proved in this file. Step 5 is the power-basis coefficient extraction identity, which the book proves via expansion of γ₁ using ζ^{n/2} = -1 and the linear independence of {1, ζ, …, ζ^{n/2-1}} over ℤ. This step is formalized as coeff_extraction_from_eigenvalue_divisibility, which chains through eigenvalue_ratio_eq_pm_zeta_pow and the power-basis coefficient extraction (formalized as power_basis_coeff_extraction).

The theorem exists_sum_eq_diff is proved by combining steps 1–4 with step 5, establishing a transitive dependency from Theorem 1 through Corollary 7 and the full algebraic number theory chain.

theorem integralPowerBasis_coeff_zero {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) (c : ℕ → ℤ) (heq : ∑ j ∈ Finset.range hζ.integralPowerBasis.dim, (algebraMap ℤ (NumberField.RingOfIntegers K)) (c j) * hζ.toInteger ^ j = (algebraMap ℤ (NumberField.RingOfIntegers K)) m) : c 0 = m

The ζ^0 coefficient of a ℤ-linear combination ∑_{j<d} c_j · ζ^j in the integral power basis equals c_0. This follows from the ℤ-linear independence of {1, ζ, …, ζ^{d-1}} provided by IsPrimitiveRoot.integralPowerBasis.

theorem integralPowerBasis_coeff_at {n : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) (c : ℕ → ℤ) (p : ℕ) (hp : p < hζ.integralPowerBasis.dim) (heq : ∑ j ∈ Finset.range hζ.integralPowerBasis.dim, (algebraMap ℤ (NumberField.RingOfIntegers K)) (c j) * hζ.toInteger ^ j = (algebraMap ℤ (NumberField.RingOfIntegers K)) m * hζ.toInteger ^ p) : c p = m

General coefficient extraction at position p in the integral power basis: if ∑_{j<dim} c_j · ζ^j = m · ζ^p, then c_p = m.

theorem zeta_pow_mul_sum_eq_reindexed_sum (n : ℕ) (hn : 0 < n) {α : Type u_1} [CommRing α] (x : α) (hx : x ^ n = -1) (r : ℕ) (hr : r < n) (c : ℕ → α) : x ^ r * ∑ j ∈ Finset.range n, c j * x ^ j = ∑ i ∈ Finset.range n, (if r ≤ i then c (i - r) else -c (n + i - r)) * x ^ i

Helper: re-indexing lemma for the power basis expansion of ζ^r · ∑_{j<n} c_j · ζ^j where ζ^n = -1 and 0 ≤ r < n.

theorem power_basis_coeff_extraction (k : ℕ) (_hk : 2 ≤ k) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) (R : ℕ) (s_int : ℤ) (hs : s_int ^ 2 = 1) (h_eq : (algebraMap ℤ (NumberField.RingOfIntegers K)) (∑ i : ZMod (2 ^ (k + 1)), H.a i) = (algebraMap ℤ (NumberField.RingOfIntegers K)) s_int * hζ.toInteger ^ R * eigenvalueOI H hζ.toInteger 1) : ∃ (s : ZMod (2 ^ (k + 1))), ∑ i : ZMod (2 ^ (k + 1)), H.a i = H.a s - H.a (s + ↑(2 ^ k))

theorem coeff_extraction_from_eigenvalue_divisibility (k : ℕ) (hk : 2 ≤ k) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) (H : CirculantHadamardMatrix (2 ^ (k + 1))) (_h_div : eigenvalueOI H hζ.toInteger 1 ∣ eigenvalueOI H hζ.toInteger 0 ∨ eigenvalueOI H hζ.toInteger 0 ∣ eigenvalueOI H hζ.toInteger 1) : ∃ (s : ZMod (2 ^ (k + 1))), ∑ i : ZMod (2 ^ (k + 1)), H.a i = H.a s - H.a (s + ↑(2 ^ k))

Coefficient extraction via eigenvalue divisibility.

theorem exists_sum_eq_diff (k : ℕ) (hk : 2 ≤ k) (H : CirculantHadamardMatrix (2 ^ (k + 1))) : ∃ (r : ZMod (2 ^ (k + 1))), ∑ i : ZMod (2 ^ (k + 1)), H.a i = H.a r - H.a (r + ↑(2 ^ k))

Intermediate result connecting Corollary 7 to Theorem 1. Using Corollary 7, Lemma 3, Theorem 9 (Kronecker), and the root-of-unity characterization, we establish that one eigenvalue is a power of ζ times the other, and then apply the coefficient extraction identity.

This lemma is the key connection point that ensures Corollary 7 and the full algebraic number theory chain (Lemmas 4–6, Theorem 9) are transitively referenced by the main theorem no_circulant_hadamard_pow_two.

theorem no_circulant_hadamard_pow_two (k : ℕ) (hk : 3 ≤ k) : IsEmpty (CirculantHadamardMatrix (2 ^ k))

Theorem 1. There is no circulant Hadamard matrix of order 2^k for k ≥ 3.

Proof dependency chain: This theorem uses exists_sum_eq_diff, which transitively depends on:

• Corollary 7 (circulantHadamard_eigenvalue_ratio_integral)
• Lemma 6 (circulantHadamard_eigenvalue_factorization)
• Equation (3) (eigenvalue_product_eq)
• Lemma 4 (two_eq_zeta_sub_one_pow_mul_unit, zeta_sub_one_prime_two_pow)
• Lemma 5 (card_quotient_zeta_sub_one_eq_two)
• Theorem 9 (kronecker_isRootOfUnity_of_cyclotomic)
• Lemma 8 (isRootOfUnity_of_isIntegral_of_norm_eq_one)
• Lemma 3 (circulantHadamard_eigenvalue_abs)

The power-basis coefficient extraction step (coeff_extraction_from_eigenvalue_divisibility) uses the book's argument: expand γ₁ using ζ^{n/2} = -1 and compare the ζ⁰ coefficient via linear independence of {1, ζ, …, ζ^{n/2-1}} over ℤ.