FormalConjectures.Arxiv.«2402.13202».CirculantHadamard

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil
import FormalConjectures.Wikipedia.Hadamard

The circulant Hadamard conjecture

A circulant matrix is generated by cyclically shifting one row. The circulant Hadamard conjecture, also attributed to Ryser, says that no circulant Hadamard matrix has order greater than $4$.

Reference:

S. Steinerberger, A note on approximate Hadamard matrices

namespace CirculantHadamard

A generator for a circulant Hadamard matrix of order four.

def orderFourGenerator : Fin 4 → ℝ :=
  ![1, 1, 1, -1]

The order-four generator gives a circulant Hadamard matrix.

@[category test, AMS 15]
theorem orderFourGenerator_isHadamard :
    Hadamard.IsHadamard' (Matrix.circulant orderFourGenerator) := by⊢ Hadamard.IsHadamard' (Matrix.circulant orderFourGenerator)
  constructorleft⊢ ∀ (i j : Fin 4), Matrix.circulant orderFourGenerator i j ∈ {1, -1}right⊢ (Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator = ↑4
  ·left⊢ ∀ (i j : Fin 4), Matrix.circulant orderFourGenerator i j ∈ {1, -1} intro i jlefti:Fin 4j:Fin 4⊢ Matrix.circulant orderFourGenerator i j ∈ {1, -1}
    fin_cases ileft.«0»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) j ∈ {1, -1}left.«1»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) j ∈ {1, -1}left.«2»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) j ∈ {1, -1}left.«3»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) j ∈ {1, -1} <;>left.«0»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) j ∈ {1, -1}left.«1»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) j ∈ {1, -1}left.«2»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) j ∈ {1, -1}left.«3»j:Fin 4⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) j ∈ {1, -1} fin_cases jleft.«3».«0»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ∈ {1, -1}left.«3».«1»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ∈ {1, -1}left.«3».«2»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ∈ {1, -1}left.«3».«3»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ∈ {1, -1} <;>left.«0».«0»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ∈ {1, -1}left.«0».«1»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ∈ {1, -1}left.«0».«2»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ∈ {1, -1}left.«0».«3»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ∈ {1, -1}left.«1».«0»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ∈ {1, -1}left.«1».«1»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ∈ {1, -1}left.«1».«2»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ∈ {1, -1}left.«1».«3»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ∈ {1, -1}left.«2».«0»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ∈ {1, -1}left.«2».«1»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ∈ {1, -1}left.«2».«2»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ∈ {1, -1}left.«2».«3»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ∈ {1, -1}left.«3».«0»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ∈ {1, -1}left.«3».«1»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ∈ {1, -1}left.«3».«2»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ∈ {1, -1}left.«3».«3»⊢ Matrix.circulant orderFourGenerator ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ∈ {1, -1}
      norm_num [Matrix.circulant, orderFourGenerator, Fin.sub_def, Fin.neg_def]All goals completed! 🐙
  ·right⊢ (Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator = ↑4 ext i jrighti:Fin 4j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) i j = ↑4 i j
    fin_cases iright.«0»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) jright.«1»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) jright.«2»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) jright.«3»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) j <;>right.«0»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) jright.«1»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) jright.«2»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) jright.«3»j:Fin 4⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩) j =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) j fin_cases jright.«3».«0»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)right.«3».«1»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)right.«3».«2»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)right.«3».«3»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨3, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) <;>right.«0».«0»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩)
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)right.«0».«1»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩)
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)right.«0».«2»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩)
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)right.«0».«3»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨0, ⋯⟩)
    ((fun i ↦ i) ⟨3, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩)right.«1».«0»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩)
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)right.«1».«1»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩)
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)right.«1».«2»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩)
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)right.«1».«3»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨1, ⋯⟩)
    ((fun i ↦ i) ⟨3, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩)right.«2».«0»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩)
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)right.«2».«1»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩)
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)right.«2».«2»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩)
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)right.«2».«3»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨2, ⋯⟩)
    ((fun i ↦ i) ⟨3, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩)right.«3».«0»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)right.«3».«1»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)right.«3».«2»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)right.«3».«3»⊢ ((Matrix.circulant orderFourGenerator).transpose * Matrix.circulant orderFourGenerator) ((fun i ↦ i) ⟨3, ⋯⟩)
    ((fun i ↦ i) ⟨3, ⋯⟩) =
  ↑4 ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩)
      norm_num [Matrix.mul_apply, Matrix.circulant, orderFourGenerator, Fin.sum_univ_succ,
        Fin.sub_def, Fin.neg_def, Matrix.ofNat_apply]All goals completed! 🐙

Every circulant Hadamard matrix has order at most four.

@[category research open, AMS 15]
theorem circulant_hadamard_conjecture {n : ℕ} (v : Fin n → ℝ)
    (hv : Hadamard.IsHadamard' (Matrix.circulant v)) : n ≤ 4 := byn:ℕv:Fin n → ℝhv:Hadamard.IsHadamard' (Matrix.circulant v)⊢ n ≤ 4
  sorryAll goals completed! 🐙

end CirculantHadamard