OrderSquareEven.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Square and even order from actual circulant sign rows

Augmentation of the cyclic norm identity gives an integer square. A nonidentity correlation is a zero sum of signs; reduction modulo two makes its number of summands even. Both conclusions follow from the actual real circulant Hadamard matrix predicate.

theorem OAI.CirculantHadamard.positive_nat_square_of_int_square line 22
theorem OAI.CirculantHadamard.even_card_of_sign_sum_zero line 33
theorem OAI.CirculantHadamard.order_even_of_sign_norm line 50
Source documentation
A nonidentity norm coefficient is a zero sum of exactly n signs.
```
theorem order_even_of_sign_norm {n : ℕ} [NeZero n] (hn : 1 < n)
    (f : CyclicRing.Elem ℤ n) (hsign : CyclicSignRow f)
    (hnorm : f * CyclicRing.ringStar f = CyclicRing.scalar n (n : ℤ)) :
    Even n := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicSignRow, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar
theorem OAI.CirculantHadamard.order_square_even_of_sign_norm line 67
Source documentation
Square and even order from the actual integer sign norm equation.
```
theorem order_square_even_of_sign_norm {n : ℕ} [NeZero n] (hn : 1 < n)
    (f : CyclicRing.Elem ℤ n) (hsign : CyclicSignRow f)
    (hnorm : f * CyclicRing.ringStar f = CyclicRing.scalar n (n : ℤ)) :
    (∃ m : ℕ, 0 < m ∧ n = m ^ 2) ∧ Even n := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicSignRow, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar
theorem OAI.CirculantHadamard.order_square_even line 79
Source documentation
A nontrivial actual real circulant sign Hadamard matrix has positive square order and even order. The integer row and its norm identity are obtained from the proved matrix correspondence.
```
theorem order_square_even {n : ℕ} (hn : 1 < n)
    (h : ExistsRealCirculantHadamard n) :
    (∃ m : ℕ, 0 < m ∧ n = m ^ 2) ∧ Even n := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard