Trace H kernel

theorem traceH_kernel (α κ : ℕ) (h2 : (2 : R) ≠ 0) (hκ : κ + 1 ≤ α)    (p q : Fin (2 ^ α / 2 ^ κ)) :    traceH α (2 ^ κ) (Xpow (powTwoCyclotomic (R := R) α)        (packExp α (2 ^ κ) p.val + packExp α (2 ^ κ) q.val * conjExp α))      = if p = q then (2 ^ α / 2 ^ κ) • (1 : Rq (powTwoCyclotomic (R := R) α)) else 0 := by  have hk : 2 * 2 ^ κ ∣ 2 ^ α := by    rw [show 2 * 2 ^ κ = 2 ^ (κ + 1) from by rw [pow_succ]; ring]; exact pow_dvd_pow 2 hκ  set n := 2 ^ α / (2 * 2 ^ κ) with hn  have hrange : n = 2 ^ (α - κ - 1) := by    rw [hn, show 2 * 2 ^ κ = 2 ^ (κ + 1) from by rw [pow_succ]; ring, Nat.pow_div hκ (by norm_num),      Nat.sub_sub]  have hnpos : 0 < n := by rw [hrange]; positivity  have hn_dvd_M : n ∣ 2 ^ (α + 1) := by rw [hrange]; exact pow_dvd_pow 2 (by omega)  have hd2 : 2 ^ (α - 1) = 2 ^ κ * n := by rw [hrange, ← pow_add]; congr 1; omega  have hc1 : conjExp α + 1 = 2 ^ (α + 1) := by    have : 1 ≤ 2 ^ (α + 1) := Nat.one_le_two_pow; rw [conjExp]; omega  have htwon : 2 ^ α / 2 ^ κ = 2 * n := by    rw [hrange, Nat.pow_div (by omega) (by norm_num), ← pow_succ']; congr 1; omega  have h2α : 2 * 2 ^ (α - 1) = 2 ^ α := by rw [← pow_succ']; congr 1; omega  have hαα : 2 ^ α + 2 ^ α = 2 ^ (α + 1) := by rw [← two_mul, ← pow_succ']  have hpackmod : ∀ v, packExp α (2 ^ κ) v % n = v % n := by    intro v    unfold packExp    rw [← hn]    split_ifs with hv    · rfl    · rw [hd2, Nat.add_mod, Nat.mul_mod_left, Nat.zero_add, Nat.mod_mod,        ← Nat.mod_eq_sub_mod (Nat.not_lt.mp hv)]  set ep := packExp α (2 ^ κ) p.val with hep  set eq := packExp α (2 ^ κ) q.val with heq  have hzmod : eq * 2 ^ (α + 1) % n = 0 := by    obtain ⟨c, hc⟩ := hn_dvd_M.mul_left eq; rw [hc, Nat.mul_mod_right]  -- `n ∣ J ↔ p ≡ q (mod n)`  have hJn : (ep + eq * conjExp α + eq) % n = ep % n := by    rw [show ep + eq * conjExp α + eq = ep + eq * 2 ^ (α + 1) from by rw [← hc1]; ring,      Nat.add_mod, hzmod, Nat.add_zero, Nat.mod_mod]  have hJdvd : n ∣ (ep + eq * conjExp α) ↔ p.val % n = q.val % n := by    rw [Nat.dvd_iff_mod_eq_zero, ← hpackmod p.val, ← hpackmod q.val, ← hep, ← heq]    constructor    · intro h0      have h1 : (ep + eq * conjExp α + eq) % n = eq % n := by        rw [Nat.add_mod, h0, Nat.zero_add, Nat.mod_mod]      rw [hJn] at h1; exact h1    · intro hpq      have hb : (ep + eq * conjExp α + eq) % n = (0 + eq) % n := by rw [hJn, Nat.zero_add, hpq]      exact Nat.ModEq.add_right_cancel' eq hb  by_cases hpq : p = q  · subst hpq    rw [if_pos rfl,      show ep + ep * conjExp α = 2 ^ (α + 1) * ep from by        rw [conjExp, Nat.mul_sub, mul_one, Nat.add_sub_cancel'          (Nat.le_mul_of_pos_right _ (by positivity)), mul_comm],      Xpow_mul, Xpow_conductor, one_pow, traceH_one α (2 ^ κ) ⟨κ, rfl⟩ hk]  · rw [if_neg hpq]    by_cases hmod : p.val % n = q.val % n    · -- `±d/2` case: `X^{2J} = -1`, generalized Claim 3      refine traceH_Xpow_neg_one_sq α (2 ^ κ) _ ⟨κ, rfl⟩ hk ?_      have hqlt : q.val < 2 * n := htwon ▸ q.isLt      have hplt : p.val < 2 * n := htwon ▸ p.isLt      have hne : p.val ≠ q.val := fun h => hpq (Fin.ext h)      have h2pp : 2 * ep ≡ 2 ^ α + 2 * eq [MOD 2 ^ (α + 1)] := by        rcases lt_or_ge p.val n with hpn | hpn        · have hqn : ¬ q.val < n := fun hqn =>            hne (by rw [Nat.mod_eq_of_lt hpn, Nat.mod_eq_of_lt hqn] at hmod; exact hmod)          have hqv : q.val - n = p.val := by            have hp' : p.val % n = p.val := Nat.mod_eq_of_lt hpn            have hq' : q.val % n = q.val - n := by              rw [Nat.mod_eq_sub_mod (Nat.not_lt.mp hqn), Nat.mod_eq_of_lt (by omega)]            rw [hp', hq'] at hmod; exact hmod.symm          have hepv : ep = p.val := by rw [hep]; unfold packExp; rw [← hn, if_pos hpn]          have heqv : eq = 2 ^ (α - 1) + p.val := by            rw [heq]; unfold packExp; rw [← hn, if_neg hqn, hqv]          rw [hepv, heqv, Nat.ModEq,            show 2 ^ α + 2 * (2 ^ (α - 1) + p.val) = 2 ^ (α + 1) + 2 * p.val from by omega,            Nat.add_mod_left]        · have hqn : q.val < n := by            by_contra hqn'            have hp' : p.val % n = p.val - n := by              rw [Nat.mod_eq_sub_mod hpn, Nat.mod_eq_of_lt (by omega)]            have hq' : q.val % n = q.val - n := by              rw [Nat.mod_eq_sub_mod (Nat.not_lt.mp hqn'), Nat.mod_eq_of_lt (by omega)]            rw [hp', hq'] at hmod; exact hne (by omega)          have hpv : p.val - n = q.val := by            have hp' : p.val % n = p.val - n := by              rw [Nat.mod_eq_sub_mod hpn, Nat.mod_eq_of_lt (by omega)]            have hq' : q.val % n = q.val := Nat.mod_eq_of_lt hqn            rw [hp', hq'] at hmod; exact hmod          have hepv : ep = 2 ^ (α - 1) + q.val := by            rw [hep]; unfold packExp; rw [← hn, if_neg (not_lt.mpr hpn), hpv]          have heqv : eq = q.val := by rw [heq]; unfold packExp; rw [← hn, if_pos hqn]          rw [hepv, heqv,            show 2 * (2 ^ (α - 1) + q.val) = 2 ^ α + 2 * q.val from by omega]      have hJ2 : 2 * (ep + eq * conjExp α) + 2 * eq ≡ 2 * ep [MOD 2 ^ (α + 1)] := by        rw [Nat.ModEq, show 2 * (ep + eq * conjExp α) + 2 * eq            = 2 * ep + (2 * eq) * 2 ^ (α + 1) from by rw [← hc1]; ring, Nat.add_mul_mod_self_right]      have hkey : 2 * (ep + eq * conjExp α) % 2 ^ (α + 1) = 2 ^ α % 2 ^ (α + 1) :=        Nat.ModEq.add_right_cancel' (2 * eq) (hJ2.trans h2pp)      rw [Xpow_congr_mod α hkey, Xpow_natDegree]    · -- `d/2k ∤ J` case: Claim 2      refine traceH_Xpow_eq_zero α (2 ^ κ) h2 ⟨κ, rfl⟩ hk ?_      rw [← hn]      exact fun h => hmod (hJdvd.mp h)