BinaryNorms.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Cancelling the factor four in the binary norm identities

The coefficient ring may be a domain; the finite cyclic group algebra is not assumed to be a domain. Cancellation is performed separately at every coefficient. In particular these statements apply both to complex coefficients and to the actual Gaussian subring of ℂ.

CyclicRing.ringStar conjugates coefficients as well as reversing exponents. The evaluation bridge requires compatibility with this full operation, including at the fourth root i; an inversion-only operation would not suffice.

theorem OAI.CirculantHadamard.BinaryNorms.four_nsmul_cancel line 39
Source documentation
Cancel four coefficientwise, without any domain assumption on the group algebra.
```
theorem four_nsmul_cancel {f g : Elem R n}
    (h : (4 : ℕ) • f = (4 : ℕ) • g) : f = g := by
…
```
theorem OAI.CirculantHadamard.BinaryNorms.ringStar_nsmul line 63
Source documentation
Coefficient conjugation fixes natural scalar multiples.
```
theorem ringStar_nsmul (k : ℕ) (x : Elem R n) :
    ringStar (k • x) = k • ringStar x := by
…
```
theorem OAI.CirculantHadamard.BinaryNorms.two_nsmul_norm line 69
Source documentation
The exact factor four before cancellation; this is valid even when the coefficient ring itself has zero divisors.
```
theorem two_nsmul_norm (x : Elem R n) :
    ((2 : ℕ) • x) * ringStar ((2 : ℕ) • x) =
      (4 : ℕ) • (x * ringStar x) := by
…
```
theorem OAI.CirculantHadamard.BinaryNorms.norm_of_two_nsmul line 78
theorem OAI.CirculantHadamard.BinaryNorms.norm_of_evaluation line 92

theorem OAI.CirculantHadamard.BinaryNorms.mappedBlock_intCast line 112

Source documentation

The partial evaluation uses the same literal coefficient cast as the constructed Gaussian element.

theorem mappedBlock_intCast {R : Type uR} [CommRing R]
    (f : ProductElem ℤ m) (j : ZMod 4) :
    mappedBlock m (Int.castRingHom R) f j =
      AddMonoidAlgebra.ofCoeff (castCoeffs (block f j).coeff) := by
…

theorem OAI.CirculantHadamard.BinaryNorms.evaluation_one_eq_two_c line 123

Source documentation

The value at one is twice the actual integral c, not a freely chosen element with a prescribed evaluation.

theorem evaluation_one_eq_two_c (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a)) :
    partialEval m (RingHom.id ℤ) 1 (by simp) f =
      (2 : ℕ) • AddMonoidAlgebra.ofCoeff (c (fun j => (blocks f j).coeff)) := by
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.evaluation_neg_one_eq_two_d line 135

Source documentation

The value at minus one is twice the actual integral d.

theorem evaluation_neg_one_eq_two_d (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a)) :
    partialEval m (RingHom.id ℤ) (-1) (by norm_num) f =
      (2 : ℕ) • AddMonoidAlgebra.ofCoeff (d (fun j => (blocks f j).coeff)) := by
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.evaluation_fourthRoot_eq_two_gOver line 149

Source documentation

The fourth-root evaluation is twice the constructed Gaussian pair. The coefficient ring is arbitrary, including the actual Gaussian ring, without assuming a group-algebra domain.

theorem evaluation_fourthRoot_eq_two_gOver {R : Type uR} [CommRing R]
    (i : R) (hi : i ^ 2 = -1) (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a)) :
    partialEval m (Int.castRingHom R) i (fourthRoot_pow_four i hi) f =
      (2 : ℕ) • AddMonoidAlgebra.ofCoeff (gOver i (fun j => (blocks f j).coeff)) := by
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.c_norm_of_product_norm line 162

theorem OAI.CirculantHadamard.BinaryNorms.d_norm_of_product_norm line 174

Source documentation

The second norm uses the real fourth root -1 and its genuine star law.

theorem d_norm_of_product_norm (u : ℕ) (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * groupStar f = ((4 * u ^ 2 : ℕ) : ProductElem ℤ m)) :
    Mul.mul (α := Elem ℤ m) (AddMonoidAlgebra.ofCoeff (d (fun j => (blocks f j).coeff))) (ringStar (AddMonoidAlgebra.ofCoeff (d (fun j => (blocks f j).coeff)))) =
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.gOver_norm_of_product_norm line 187

Source documentation

The third norm uses conjugation of the fourth root, not exponent reversal alone. Both the square equation and the conjugation equation are explicit.

theorem gOver_norm_of_product_norm {R : Type uR} [CommRing R] [StarRing R]
    [IsDomain R] [CharZero R] (i : R) (hi : i ^ 2 = -1) (hstar : star i = -i)
    (u : ℕ) (f : ProductElem ℤ m) (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * groupStar f = ((4 * u ^ 2 : ℕ) : ProductElem ℤ m)) :
    Mul.mul (α := Elem R m) (AddMonoidAlgebra.ofCoeff (gOver i (fun j => (blocks f j).coeff))) (ringStar (AddMonoidAlgebra.ofCoeff (gOver i (fun j => (blocks f j).coeff)))) =
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.g_norm_of_product_norm line 202

Source documentation

The same cancellation is valid in ℂ[C_m], despite that ring having zero divisors. This specializes the actual coefficient construction g.

theorem g_norm_of_product_norm (u : ℕ) (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * groupStar f = ((4 * u ^ 2 : ℕ) : ProductElem ℤ m)) :
    Mul.mul (α := Elem ℂ m) (AddMonoidAlgebra.ofCoeff (g (fun j => (blocks f j).coeff))) (ringStar (AddMonoidAlgebra.ofCoeff (g (fun j => (blocks f j).coeff)))) =
…

Mentions: OAI.CirculantHadamard.IsSign

theorem OAI.CirculantHadamard.BinaryNorms.star_gaussianI line 210
Source documentation
Conjugation negates the imaginary unit in the actual Gaussian subring.
```
theorem star_gaussianI : star CyclotomicRings.gaussianI = -CyclotomicRings.gaussianI := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicRings.gaussianI
theorem OAI.CirculantHadamard.BinaryNorms.gaussian_g_norm_of_product_norm line 216
Source documentation
The integral Gaussian norm, before any character evaluation or localization.
```
theorem gaussian_g_norm_of_product_norm (u : ℕ) (f : ProductElem ℤ m)
    (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * groupStar f = ((4 * u ^ 2 : ℕ) : ProductElem ℤ m)) :
    Mul.mul (α := Elem CyclotomicRings.GaussianRing m)
…
```
Mentions: OAI.CirculantHadamard.IsSign, OAI.CirculantHadamard.CyclotomicRings.GaussianRing
theorem OAI.CirculantHadamard.BinaryNorms.binary_norms_of_cyclic_norm line 232
Source documentation
The complete binary norm step starts from the original cyclic sign row. The CRT transport, block signs, doubled evaluation values, full-star compatibility, and scalar cancellation are all proved in the construction. No separate norm premise for c, d, or g is accepted.
```
theorem binary_norms_of_cyclic_norm {u : ℕ} [NeZero u] (hu : Odd u)
    (f : Elem ℤ (4 * u ^ 2)) (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * ringStar f = scalar (4 * u ^ 2) ((4 * u ^ 2 : ℕ) : ℤ)) :
    let H := BinaryBlocks.blocks (BinaryBlocks.crt ℤ u hu f)
…
```
Mentions: OAI.CirculantHadamard.IsSign, OAI.CirculantHadamard.BinaryBlocks.blocks, OAI.CirculantHadamard.BinaryBlocks.crt