BinaryBlocks.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

The actual four-block decomposition and partial evaluations

The Chinese remainder equivalence transports the actual cyclic group ring, not just a coefficient count. Coefficients of its four slices are the original signs. Partial evaluation is a ring homomorphism defined on the product group algebra and intertwines coefficient conjugation with index reversal.

abbrev OAI.CirculantHadamard.BinaryBlocks.ProductElem line 30
theorem OAI.CirculantHadamard.BinaryBlocks.four_coprime_sq line 33
def OAI.CirculantHadamard.BinaryBlocks.crtIndex line 37
Source documentation
The concrete CRT map on the exponent group.
```
def crtIndex (u : ℕ) (hu : Odd u) :
    ZMod (4 * u ^ 2) ≃+ ZMod 4 × ZMod (u ^ 2) :=
…
```
def OAI.CirculantHadamard.BinaryBlocks.crt line 42
Source documentation
The resulting algebra equivalence preserves the actual convolution.
```
def crt (R : Type uR) [CommRing R] (u : ℕ) (hu : Odd u) :
    Elem R (4 * u ^ 2) ≃ₐ[R] ProductElem R (u ^ 2) :=
…
```
Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem
theorem OAI.CirculantHadamard.BinaryBlocks.crt_apply line 46
theorem OAI.CirculantHadamard.BinaryBlocks.crt_ringStar line 51
theorem OAI.CirculantHadamard.BinaryBlocks.crt_norm line 57
def OAI.CirculantHadamard.BinaryBlocks.block line 63
theorem OAI.CirculantHadamard.BinaryBlocks.block_apply line 67
def OAI.CirculantHadamard.BinaryBlocks.blocks line 71
Source documentation
Fin-four indexing agrees with the coefficient arithmetic used by the halves.
```
def blocks {R : Type uR} [Semiring R] {m : ℕ} [NeZero m]
    (f : ProductElem R m) : Fin 4 → Elem R m := fun j => block f j
```
Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem, OAI.CirculantHadamard.BinaryBlocks.block
theorem OAI.CirculantHadamard.BinaryBlocks.blocks_apply line 74
theorem OAI.CirculantHadamard.BinaryBlocks.blocks_signs line 77
theorem OAI.CirculantHadamard.BinaryBlocks.crt_blocks_signs line 81
def OAI.CirculantHadamard.BinaryBlocks.partialCharacter line 93
Source documentation
A fourth-root character on the first factor, retaining the second factor.
```
def partialCharacter (z : S) (hz : z ^ 4 = 1) :
    Multiplicative (ZMod 4 × ZMod m) →* Elem S m where
…
```
def OAI.CirculantHadamard.BinaryBlocks.partialEval line 113
Source documentation
Actual partial evaluation, allowing the integer-to-complex coefficient map.
```
def partialEval (φ : R →+* S) (z : S) (hz : z ^ 4 = 1) :
    ProductElem R m →+* Elem S m :=
…
```
Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_single line 119
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_apply line 130
Source documentation
The four coefficients are summed, with no loss of the second coordinate.
```
theorem partialEval_apply (φ : R →+* S) (z : S) (hz : z ^ 4 = 1)
    (f : ProductElem R m) (b : ZMod m) :
    (partialEval m φ z hz f).coeff b =
      ∑ j : ZMod 4, φ (f.coeff (j, b)) * z ^ j.val := by
…
```
Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem, OAI.CirculantHadamard.BinaryBlocks.partialEval
def OAI.CirculantHadamard.BinaryBlocks.mappedBlock line 152
theorem OAI.CirculantHadamard.BinaryBlocks.mappedBlock_apply line 155
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_four line 158
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_one line 172
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_neg_one line 177
theorem OAI.CirculantHadamard.BinaryBlocks.fourthRoot_pow_four line 185
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_fourthRoot line 191
Source documentation
The Gaussian coefficient ring can use its actual imaginary unit directly.
```
theorem partialEval_fourthRoot (φ : R →+* S) (i : S) (hi : i ^ 2 = -1)
    (f : ProductElem R m) :
    partialEval m φ i (fourthRoot_pow_four i hi) f =
      mappedBlock m φ f 0 + i • mappedBlock m φ f 1 -
        mappedBlock m φ f 2 - i • mappedBlock m φ f 3 := by
…
```
Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem, OAI.CirculantHadamard.BinaryBlocks.partialEval, OAI.CirculantHadamard.BinaryBlocks.fourthRoot_pow_four, OAI.CirculantHadamard.BinaryBlocks.mappedBlock
theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_I line 204

theorem OAI.CirculantHadamard.BinaryBlocks.partialEval_groupStar line 217

Source documentation

Intertwining is proved on the actual ring maps, with both parts of the star.

theorem partialEval_groupStar (φ : R →+* S) (z : S) (hz : z ^ 4 = 1)
    (hφ : ∀ r, φ (star r) = star (φ r))
    (hchar : ∀ a : ZMod 4, z ^ (-a).val = star (z ^ a.val))
    (f : ProductElem R m) :
    partialEval m φ z hz (groupStar f) = ringStar (partialEval m φ z hz f) := by
…

Mentions: OAI.CirculantHadamard.BinaryBlocks.ProductElem, OAI.CirculantHadamard.BinaryBlocks.partialEval

theorem OAI.CirculantHadamard.BinaryBlocks.one_character_star line 238
theorem OAI.CirculantHadamard.BinaryBlocks.neg_one_character_star line 242
theorem OAI.CirculantHadamard.BinaryBlocks.fourthRoot_character_star line 255
theorem OAI.CirculantHadamard.BinaryBlocks.I_character_star line 274