Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Classification of positive real circulant sign Hadamard orders

The existence predicate retains the actual real matrix, its sign entries, literal cyclic rows, and full Gram identity. Square-order and two-adic descent reduce every nontrivial order to 4 * u^2 with u positive and odd. The binary contradiction excludes u > 1, while explicit matrices realize orders one and four.

theorem OAI.CirculantHadamard.exists_iff_order_one_or_four line 21
Source documentation
An actual real circulant sign Hadamard matrix of positive order exists exactly at orders one and four.
Distinct definitions of this name: ComparatorChallenges/CirculantHadamard.lean:24 (same statement text; different proof or body). Qualify references as OAI.CirculantHadamard.exists_iff_order_one_or_four@path.
```
theorem exists_iff_order_one_or_four (n : ℕ) (hn : 0 < n) :
    ExistsRealCirculantHadamard n ↔ n = 1 ∨ n = 4 := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard