BinaryContradiction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CirculantHadamard.binary_sign_norm_impossible line 16

Source documentation

The binary contradiction starts with the original integer sign row and its full cyclic norm equation.

theorem binary_sign_norm_impossible {u : ℕ} [NeZero u]
    (hu : 1 < u) (hodd : Odd u)
    (f : Elem ℤ (4 * u ^ 2)) (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * ringStar f = scalar (4 * u ^ 2) ((4 * u ^ 2 : ℕ) : ℤ)) :
    False := by
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.not_exists_four_mul_odd_square line 42
Source documentation
No real circulant sign Hadamard matrix has order 4u² for odd u > 1. The original real-matrix predicate is converted by the proved integer-row equivalence; every subsequent construction is made from that actual row.
```
theorem not_exists_four_mul_odd_square {u : ℕ}
    (hu : 1 < u) (hodd : Odd u) :
    ¬ ExistsRealCirculantHadamard (4 * u ^ 2) := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard