AlternatingTorsion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual alternating character product has odd torsion

The index is the full set of prime divisors of u. The local comparison and all-maximal-ideal argument are applied to the actual partial evaluations of the given constant-norm group-ring element. No edge-comparison, integrality, complex-norm, or torsion conclusion is assumed.

abbrev OAI.CirculantHadamard.alternatingValue line 26
Source documentation
The single fixed field element used for every prime-direction comparison.
```
abbrev alternatingValue (u : ℕ) (hu : 0 < u)
    (x : CyclicRing.Elem GaussianRing (u ^ 2)) : FractionRing (B u) :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem

theorem OAI.CirculantHadamard.exists_integral_alternating_root_of_unity line 33

Source documentation

Denominator removal and all complex homomorphisms are discharged for the actual character values before invoking Kronecker's criterion.

theorem exists_integral_alternating_root_of_unity (u : ℕ) [NeZero (u ^ 2)]
    (hu : 1 < u) (huodd : Odd u) (x : CyclicRing.Elem GaussianRing (u ^ 2))
    (hx : x * CyclicRing.ringStar x =
      CyclicRing.scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing)) :
    ∃ z : B u,
      algebraMap (B u) (FractionRing (B u)) z =
        alternatingValue u (lt_trans Nat.zero_lt_one hu) x ∧
      ∃ n : ℕ, 0 < n ∧ z ^ n = 1 := by
…

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

theorem OAI.CirculantHadamard.alternatingProduct_prime_power_torsion line 64
Source documentation
The same alternating product is killed by a power of every actual prime dividing u. The maximal ideal and characteristic-p residue field are built from the concrete integral coefficient ring.
```
theorem alternatingProduct_prime_power_torsion (u : ℕ) [NeZero (u ^ 2)]
    (hu : 1 < u) (huodd : Odd u) (x : CyclicRing.Elem GaussianRing (u ^ 2))
    (hx : x * CyclicRing.ringStar x =
      CyclicRing.scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
    (p : PrimeIndex u) :
    ∃ a : ℕ, (alternatingValue u (lt_trans Nat.zero_lt_one hu) x) ^ (p.val ^ a) = 1 := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar, OAI.CirculantHadamard.alternatingValue

theorem OAI.CirculantHadamard.alternatingProduct_odd_torsion line 98

Source documentation

The actual subset-character product has a positive odd torsion exponent.

theorem alternatingProduct_odd_torsion (u : ℕ) [NeZero (u ^ 2)]
    (hu : 1 < u) (huodd : Odd u) (x : CyclicRing.Elem GaussianRing (u ^ 2))
    (hx : x * CyclicRing.ringStar x =
      CyclicRing.scalar (u ^ 2) ((u : GaussianRing) ^ 2)) :
    ∃ m : ℕ, 0 < m ∧ Odd m ∧
      (alternatingValue u (lt_trans Nat.zero_lt_one hu) x) ^ m = 1 := by
…

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

theorem OAI.CirculantHadamard.alternatingProduct_eq_one_of_two_primes line 113

Source documentation

With two distinct prime directions the single fixed product is one.

theorem alternatingProduct_eq_one_of_two_primes (u : ℕ) [NeZero (u ^ 2)]
    (hu : 1 < u) (huodd : Odd u) (x : CyclicRing.Elem GaussianRing (u ^ 2))
    (hx : x * CyclicRing.ringStar x =
      CyclicRing.scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
    (p q : PrimeIndex u) (hpq : p ≠ q) :
    alternatingValue u (lt_trans Nat.zero_lt_one hu) x = 1 := by
…

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