OrderHalving.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Halving an odd-coefficient dyadic group-ring element

The integer averaging lemmas retain the original paired coefficients. The group-ring step uses their actual quotient fiber sums and the concrete cyclotomic divisibility theorem; the ring is not assumed to be a domain.

def OAI.CirculantHadamard.pairAverage line 24
Source documentation
The coefficient obtained by projecting a pair and dividing by two.
```
def pairAverage (a b : ℤ) : ℤ := (a + b) / 2
```
theorem OAI.CirculantHadamard.two_mul_pairAverage line 26
theorem OAI.CirculantHadamard.odd_pairAverage line 34
Source documentation
Congruent odd coefficients modulo four have an odd integral average.
```
theorem odd_pairAverage {a b : ℤ} (hb : Odd b) (hab : (4 : ℤ) ∣ a - b) :
    Odd (pairAverage a b) := by
…
```
Mentions: OAI.CirculantHadamard.pairAverage
theorem OAI.CirculantHadamard.odd_pairAverage_of_two_pow_dvd line 42
theorem OAI.CirculantHadamard.normScalar_halving line 49
def OAI.CirculantHadamard.halvePairs line 58
Source documentation
Literal paired coefficients on the quotient of a cyclic group of even order. Integer divisibility is proved separately before this is used.
```
noncomputable def halvePairs {m : ℕ} [NeZero m] (T : Elem ℤ (2 * m)) : Elem ℤ m :=
…
```
theorem OAI.CirculantHadamard.halvePairs_apply line 62
theorem OAI.CirculantHadamard.halvePairs_odd line 67
theorem OAI.CirculantHadamard.four_smul_cancel line 77
Source documentation
Cancellation takes place in each integer coefficient. A cyclic group ring has zero divisors, which are irrelevant to this scalar cancellation.
```
theorem four_smul_cancel {m : ℕ} {S T : Elem ℤ m}
    (h : (4 : ℤ) • S = (4 : ℤ) • T) : S = T := by
…
```
theorem OAI.CirculantHadamard.norm_of_double_norm line 86
theorem OAI.CirculantHadamard.cyclicProjection_eq_two_smul_halvePairs line 110
Source documentation
Odd coefficients make the literal projected fiber sums exactly twice the integer averages. This is an identity for the actual cyclic quotient map.
```
theorem cyclicProjection_eq_two_smul_halvePairs {m : ℕ} [NeZero m]
    (h : m ∣ 2 * m) (T : Elem ℤ (2 * m)) (hodd : ∀ j, Odd (T.coeff j)) :
    cyclicProjection ℤ h T = (2 : ℤ) • halvePairs T := by
…
```
Mentions: OAI.CirculantHadamard.cyclicProjection, OAI.CirculantHadamard.halvePairs
theorem OAI.CirculantHadamard.halvePairs_norm line 122
Source documentation
Projecting and dividing by two divides the scalar norm by four. All coefficient and star identities are consequences of the actual quotient.
```
theorem halvePairs_norm {m : ℕ} [NeZero m] [NeZero (2 * m)]
    (T : Elem ℤ (2 * m)) (c : ℤ) (hodd : ∀ j, Odd (T.coeff j))
    (hnorm : T * ringStar T = scalar (2 * m) (4 * c)) :
    halvePairs T * ringStar (halvePairs T) = scalar m c := by
…
```
Mentions: OAI.CirculantHadamard.halvePairs

theorem OAI.CirculantHadamard.halvePairs_odd_norm_of_pair_divisibility line 133

Source documentation

Algebraic halving with paired divisibility. In the dyadic case, cyclotomic evaluation supplies this divisibility from the norm equation.

theorem halvePairs_odd_norm_of_pair_divisibility {m : ℕ} [NeZero m] [NeZero (2 * m)]
    (t u : ℕ) (T : Elem ℤ (2 * m)) (ht : 2 ≤ t)
    (hodd : ∀ j, Odd (T.coeff j))
    (hnorm : T * ringStar T = scalar (2 * m) ((2 ^ (2 * t) * u ^ 2 : ℕ) : ℤ))
    (hpair : ∀ j : ZMod m, (2 : ℤ) ^ t ∣
      T.coeff (j.val : ZMod (2 * m)) - T.coeff ((j.val + m : ℕ) : ZMod (2 * m))) :
    (∀ j, Odd ((halvePairs T).coeff j)) ∧
      halvePairs T * ringStar (halvePairs T) =
        scalar m ((2 ^ (2 * (t - 1)) * u ^ 2 : ℕ) : ℤ) := by
…

Mentions: OAI.CirculantHadamard.halvePairs

theorem OAI.CirculantHadamard.exists_odd_halving line 156

Source documentation

The actual dyadic order-halving step. The paired divisibility is supplied by cyclotomic evaluation and localization, not assumed in this statement. The constructed witness is the literal paired average halvePairs.

theorem exists_odd_halving (k t u : ℕ) (T : Elem ℤ (2 ^ (k + 1)))
    (ht : 2 ≤ t) (hu : Odd u) (hodd : ∀ j, Odd (T.coeff j))
    (hnorm : T * ringStar T =
      scalar (2 ^ (k + 1)) ((2 ^ (2 * t) * u ^ 2 : ℕ) : ℤ)) :
    ∃ U : Elem ℤ (2 ^ k), (∀ j, Odd (U.coeff j)) ∧
      U * ringStar U = scalar (2 ^ k) ((2 ^ (2 * (t - 1)) * u ^ 2 : ℕ) : ℤ) := by
…