ModEight.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The odd-coefficient obstruction modulo eight

The identity coefficient of an integer cyclic norm is the sum of the actual coefficient squares. Every odd square is one modulo eight. Consequently an odd-coefficient element in a cyclic group of order divisible by eight cannot have norm scalar 4 * u^2 with u odd. The divisibility hypothesis excludes order four, so the explicit order-four example is not ruled out.

theorem OAI.CirculantHadamard.odd_sq_mod_eight line 26
Source documentation
Every odd integer square is congruent to one modulo eight.
```
theorem odd_sq_mod_eight {a : ℤ} (ha : Odd a) :
    Int.ModEq 8 (a ^ 2) 1 := by
…
```

theorem OAI.CirculantHadamard.sum_odd_sq_mod_eight line 35

Source documentation

A finite sum of odd integer squares is congruent to the number of terms.

theorem sum_odd_sq_mod_eight {ι : Type uIota} (s : Finset ι) (a : ι → ℤ)
    (ha : ∀ i ∈ s, Odd (a i)) :
    Int.ModEq 8 (∑ i ∈ s, a i ^ 2) (s.card : ℤ) := by
…

theorem OAI.CirculantHadamard.sum_univ_odd_sq_mod_eight line 52

Source documentation

The same congruence for all members of a finite type.

theorem sum_univ_odd_sq_mod_eight {ι : Type uIota} [Fintype ι] (a : ι → ℤ)
    (ha : ∀ i, Odd (a i)) :
    Int.ModEq 8 (∑ i, a i ^ 2) (Fintype.card ι : ℤ) := by
…

theorem OAI.CirculantHadamard.odd_sq_sum_ne_four_mul_sq line 58

Source documentation

A multiple of eight odd squares cannot sum to four times an odd square.

theorem odd_sq_sum_ne_four_mul_sq {ι : Type uIota} [Fintype ι] (a : ι → ℤ)
    (ha : ∀ i, Odd (a i)) (hcard : 8 ∣ Fintype.card ι)
    {u : ℤ} (hu : Odd u) : (∑ i, a i ^ 2) ≠ 4 * u ^ 2 := by
…

theorem OAI.CirculantHadamard.odd_sq_sum_ne_four_mul_nat_sq line 73

Source documentation

Natural norm parameters are cast only after forming the literal scalar.

theorem odd_sq_sum_ne_four_mul_nat_sq {ι : Type uIota} [Fintype ι] (a : ι → ℤ)
    (ha : ∀ i, Odd (a i)) (hcard : 8 ∣ Fintype.card ι)
    {u : ℕ} (hu : Odd u) : (∑ i, a i ^ 2) ≠ ((4 * u ^ 2 : ℕ) : ℤ) := by
…

theorem OAI.CirculantHadamard.odd_norm_four_impossible line 80
Source documentation
The actual cyclic norm equation is impossible for an all-odd row when the cyclic order is divisible by eight and the norm parameter is odd.
```
theorem odd_norm_four_impossible {n u : ℕ} [NeZero n]
    (hcard : 8 ∣ n) (hu : Odd u) (T : CyclicRing.Elem ℤ n)
    (hodd : ∀ a, Odd (T.coeff a))
    (hnorm : T * CyclicRing.ringStar T =
      CyclicRing.scalar n ((4 * u ^ 2 : ℕ) : ℤ)) : False := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar

theorem OAI.CirculantHadamard.odd_norm_four_impossible_two_pow line 92

Source documentation

For k ≥ 3, the order 2^k meets the exact modulo-eight obstruction.

theorem odd_norm_four_impossible_two_pow {k u : ℕ} [NeZero (2 ^ k)]
    (hk : 3 ≤ k) (hu : Odd u) (T : CyclicRing.Elem ℤ (2 ^ k))
    (hodd : ∀ a, Odd (T.coeff a))
    (hnorm : T * CyclicRing.ringStar T =
      CyclicRing.scalar (2 ^ k) ((4 * u ^ 2 : ℕ) : ℤ)) : False := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar