OrderProjection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The first order projection

The quotient sends the original cyclic generator to the cyclic generator of the smaller order. Its coefficients are the sums over the actual reduction fibers. When n = m * d, every fiber contains exactly d original indices; an odd number of signs therefore produces an odd integer coefficient.

The norm scalar is preserved by the quotient map. In particular, projecting from 2^(2*s) * u^2 to 2^(2*s) does not divide the original norm scalar.

theorem OAI.CirculantHadamard.cyclic_reduction_fiber_card line 30

Source documentation

Every fiber of reduction modulo a divisor has the exact quotient size.

theorem cyclic_reduction_fiber_card {n m d : ℕ} [NeZero n] [NeZero m]
    (hdiv : m ∣ n) (hn : n = m * d) (a : ZMod m) :
    Fintype.card {x : ZMod n // ZMod.castHom hdiv (ZMod m) x = a} = d := by
…

theorem OAI.CirculantHadamard.odd_sum_of_signs line 55

Source documentation

An odd finite family of actual integer signs has odd sum.

theorem odd_sum_of_signs {α : Type uα} [Fintype α] (f : α → ℤ)
    (hf : ∀ x, IsSign (f x)) (hcard : Odd (Fintype.card α)) :
    Odd (∑ x, f x) := by
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.cyclicProjection_odd_coefficients line 71
Source documentation
The actual quotient coefficient is odd because its fiber consists of exactly the specified odd number of original signs.
```
theorem cyclicProjection_odd_coefficients {n m d : ℕ} [NeZero n] [NeZero m]
    (hdiv : m ∣ n) (hn : n = m * d) (hd : Odd d)
    (f : CyclicRing.Elem ℤ n) (hf : CyclicSignRow f) (a : ZMod m) :
    Odd ((cyclicProjection ℤ hdiv f).coeff a) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicSignRow, OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.exists_odd_cyclic_projection line 85

Source documentation

First projection in the order reduction: every coefficient is odd and the scalar on the right of the norm equation remains the original order.

theorem exists_odd_cyclic_projection {n s u : ℕ} [NeZero n]
    (hu : Odd u) (heq : n = 2 ^ (2 * s) * u ^ 2)
    (f : CyclicRing.Elem ℤ n) (hsign : CyclicSignRow f)
    (hnorm : f * CyclicRing.ringStar f = CyclicRing.scalar n (n : ℤ)) :
    ∃ T : CyclicRing.Elem ℤ (2 ^ (2 * s)),
      (∀ a, Odd (T.coeff a)) ∧
        T * CyclicRing.ringStar T =
          CyclicRing.scalar _ ((2 ^ (2 * s) * u ^ 2 : ℕ) : ℤ) := by
…

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