OrderDescent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite descent of an odd dyadic cyclic norm

The invariant 1 ≤ t and t + 2 ≤ k records exactly the range needed to halve an odd row until its norm is 4*u^2 while retaining a group order divisible by eight. Every step invokes the concrete cyclotomic halving theorem. The final step is the coefficient-square contradiction modulo eight.

theorem OAI.CirculantHadamard.odd_norm_impossible line 23

Source documentation

An odd-coefficient dyadic cyclic norm cannot have two more group exponents than norm half-exponents. No halving is performed when t = 1.

theorem odd_norm_impossible {k t u : ℕ}
    (ht : 1 ≤ t) (hkt : t + 2 ≤ k) (hu : Odd u)
    (T : Elem ℤ (2 ^ k)) (hodd : ∀ a, Odd (T.coeff a))
    (hnorm : T * ringStar T = scalar (2 ^ k) ((2 ^ (2 * t) * u ^ 2 : ℕ) : ℤ)) :
    False := by
…

theorem OAI.CirculantHadamard.initial_even_power_norm_impossible line 57