OrderReduction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The order of an actual circulant sign Hadamard matrix

The matrix supplies its literal integer sign row. Its positive even square order has a two-adic decomposition. Projecting the actual row gives odd coefficients, and the proved cyclotomic halving descent excludes every two-adic exponent except two, without any coefficient-divisibility or descent assumption.

theorem OAI.CirculantHadamard.order_reduction line 22
Source documentation
Every nontrivial actual real circulant sign Hadamard matrix has order 4 * u^2 for a positive odd natural number u.
```
theorem order_reduction {n : ℕ} (hn : 1 < n)
    (h : ExistsRealCirculantHadamard n) :
    ∃ u : ℕ, 0 < u ∧ Odd u ∧ n = 4 * u ^ 2 := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard
theorem OAI.CirculantHadamard.order_reduction_of_matrix line 41
Source documentation
The order restriction stated directly for the supplied real matrix.
```
theorem order_reduction_of_matrix {n : ℕ} (hn : 1 < n) (H : RealMatrix n)
    (hc : IsCirculant H) (hh : IsSignHadamard H) :
    ∃ u : ℕ, 0 < u ∧ Odd u ∧ n = 4 * u ^ 2 :=
…
```
Mentions: OAI.CirculantHadamard.RealMatrix, OAI.CirculantHadamard.IsCirculant, OAI.CirculantHadamard.IsSignHadamard