BinaryResidue.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CirculantHadamard.binaryLr line 19
Source documentation
The coefficient of the ratio d / c along 2. Division by c means multiplication by the inverse of the supplied unit.
```
def binaryLr (c : Oˣ) (b : O) : O :=
…
```
def OAI.CirculantHadamard.binaryLw line 23
Source documentation
The coefficient of the ratio g / c along 1 + i.
```
def binaryLw (c : Oˣ) (i b J U : O) : O :=
…
```
theorem OAI.CirculantHadamard.binary_ratio_r line 27
theorem OAI.CirculantHadamard.binary_ratio_w line 41
theorem OAI.CirculantHadamard.binaryLr_add_binaryLw line 61
Source documentation
This identity is exact before applying the residue map.
```
theorem binaryLr_add_binaryLw (c : Oˣ) (i b J U : O) :
    binaryLr c b + binaryLw c i b J U =
      -J * (↑(c⁻¹) : O) - (1 - i) * (b + U) * (↑(c⁻¹) : O) := by
…
```
Mentions: OAI.CirculantHadamard.binaryLr, OAI.CirculantHadamard.binaryLw
theorem OAI.CirculantHadamard.binary_one_add_i_ne_zero line 68
Source documentation
Nonvanishing of 2 also makes the second first-order parameter nonzero.
```
theorem binary_one_add_i_ne_zero (i : O) (hi : i ^ 2 = -1)
    (h2 : (2 : O) ≠ 0) : 1 + i ≠ 0 := by
…
```

theorem OAI.CirculantHadamard.binaryLr_unique line 84

Source documentation

The displayed coefficient is the unique coefficient along 2.

theorem binaryLr_unique (c d : Oˣ) (a b L : O)
    (hc : (c : O) = a + b) (hd : (d : O) = a - b)
    (h2 : (2 : O) ≠ 0)
    (hL : ((d * c⁻¹ : Oˣ) : O) = 1 + (2 : O) * L) :
    L = binaryLr c b := by
…

Mentions: OAI.CirculantHadamard.binaryLr

theorem OAI.CirculantHadamard.binaryLw_unique line 93

Source documentation

The displayed coefficient is the unique coefficient along 1 + i.

theorem binaryLw_unique (c g : Oˣ) (a b J U i L : O)
    (hc : (c : O) = a + b)
    (hg : (g : O) = a + i * b - ((1 + i) * J + 2 * U))
    (hi : i ^ 2 = -1) (h2 : (2 : O) ≠ 0)
    (hL : ((g * c⁻¹ : Oˣ) : O) = 1 + (1 + i) * L) :
    L = binaryLw c i b J U := by
…

Mentions: OAI.CirculantHadamard.binaryLw

theorem OAI.CirculantHadamard.binary_residue_sum line 109
Source documentation
The two coefficients have residues summing to the residue of J / c.
```
theorem binary_residue_sum (φ : O →+* k) (c : Oˣ) (i b J U : O)
    (hi : φ i = 1) :
    φ (binaryLr c b) + φ (binaryLw c i b J U) =
      φ (J * (↑(c⁻¹) : O)) := by
…
```
Mentions: OAI.CirculantHadamard.binaryLr, OAI.CirculantHadamard.binaryLw

theorem OAI.CirculantHadamard.binary_signed_product_residue_one line 119

Source documentation

A signed product of units with residue one again has residue one. The powers are formed in the unit group, including for negative exponents.

theorem binary_signed_product_residue_one [CharP k 2] {ι : Type uIota}
    (φ : O →+* k) (s : Finset ι) (u : ι → Oˣ) (ε : ι → ℤ)
    (hu : ∀ j ∈ s, φ (u j : O) = 1) :
    φ ((∏ j ∈ s, (u j) ^ (ε j) : Oˣ) : O) = 1 := by
…

theorem OAI.CirculantHadamard.binary_residue_contradiction line 143

Source documentation

The same-residue-field contradiction for a finite signed family of binary decompositions. All arithmetic input to the concrete application is explicit: unit decompositions, a square root of -1, odd torsion of both signed products, and a nonzero signed J / c residue sum.

theorem binary_residue_contradiction {ι : Type uIota}
    (φ : O →+* k) (i : O) (hi : i ^ 2 = -1) (hφi : φ i = 1)
    (h2 : (2 : O) ≠ 0) (s : Finset ι) (ε : ι → ℤ)
    (c d g : ι → Oˣ) (a b J U : ι → O)
    (hc : ∀ j ∈ s, (c j : O) = a j + b j)
    (hd : ∀ j ∈ s, (d j : O) = a j - b j)
    (hg : ∀ j ∈ s,
      (g j : O) = a j + i * b j - ((1 + i) * J j + 2 * U j))
    (hrOdd : ∃ m : ℕ, 0 < m ∧ Odd m ∧
      (∏ j ∈ s, (d j * (c j)⁻¹) ^ (ε j)) ^ m = 1)
    (hwOdd : ∃ m : ℕ, 0 < m ∧ Odd m ∧
      (∏ j ∈ s, (g j * (c j)⁻¹) ^ (ε j)) ^ m = 1)
…