OrderCyclotomicDivisibility.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Dyadic divisibility of opposite coefficient differences

We evaluate the actual integer cyclic group ring in the cyclotomic extension of the integers localized at two. The norm identity forces divisibility in that DVR. Its free monic presentation then transfers this divisibility to the paired coefficient differences, and localization reflects it to the integers.

theorem OAI.CirculantHadamard.integerCyclotomicEvaluation_coefficientPolynomial line 30
Source documentation
The canonical polynomial with the literal integer coefficients of a cyclic element evaluates to the same element in the cyclotomic quotient.
```
theorem integerCyclotomicEvaluation_coefficientPolynomial
    (A : Type uA) [CommRing A] (n : ℕ) [NeZero n] (T : CyclicRing.Elem ℤ n) :
    integerCyclotomicEvaluation A n T =
      AdjoinRoot.mk (cyclotomic n A)
        (DyadicRemainder.coefficientPolynomial n
          (fun i => algebraMap ℤ A (T.coeff (i : ZMod n)))) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.integerCyclotomicEvaluation, OAI.CirculantHadamard.DyadicRemainder.coefficientPolynomial
theorem OAI.CirculantHadamard.dyadic_difference_dvd line 55
Source documentation
A scalar norm of the stated dyadic size forces each opposite coefficient difference to be divisible by its square-root dyadic factor. No condition on the parity of the coefficients, or separate positivity of u, is required.
```
theorem dyadic_difference_dvd (k t u : ℕ)
    (T : CyclicRing.Elem ℤ (2 ^ (k + 1))) (hu : Odd u)
    (hnorm : T * CyclicRing.ringStar T =
      CyclicRing.scalar (2 ^ (k + 1)) ((2 ^ (2 * t) * u ^ 2 : ℕ) : ℤ)) :
    ∀ j : ZMod (2 ^ k), (2 : ℤ) ^ t ∣
      T.coeff (j.val : ZMod (2 ^ (k + 1))) -
        T.coeff ((j.val + 2 ^ k : ℕ) : ZMod (2 ^ (k + 1))) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar