Q dvd l2Norm Sq of not is Unit

theorem q_dvd_l2NormSq_of_not_isUnit (hq5 : q % 8 = 5) {c : Rq Φ} (hc : ¬ IsUnit c) :    (q : ℤ) ∣ (Rq.l2NormSq Φ c : ℤ) := by  rcases Nat.eq_zero_or_pos α with hα0 | hαpos  · -- α = 0: `φ.toPoly = X + 1` irreducible, so `Rq Φ` is a field; a non-unit is `0`.    subst hα0    have hφ : (powTwoCyclotomic (R := ZMod q) 0).φ.toPoly = X + 1 := by      rw [phi_toPoly]; norm_num    have hirr : Irreducible ((powTwoCyclotomic (R := ZMod q) 0).φ.toPoly) := by      rw [hφ, show (X + 1 : (ZMod q)[X]) = X - C (-1) by rw [C_neg, C_1, sub_neg_eq_add]]      exact irreducible_X_sub_C (-1)    haveI hfact : Fact (Irreducible ((powTwoCyclotomic (R := ZMod q) 0).φ.toPoly)) := ⟨hirr⟩    haveI hmax : ((powTwoCyclotomic (R := ZMod q) 0).modIdeal).IsMaximal := by      rw [modIdeal]; exact PrincipalIdealRing.isMaximal_of_irreducible hirr    have hisfield : IsField ((powTwoCyclotomic (R := ZMod q) 0).CyclotomicRing) :=      (Ideal.Quotient.maximal_ideal_iff_isField_quotient _).mp hmax    have hnu := Rq.not_isUnit_toQuotientHom_of_not_isUnit      (powTwoCyclotomic (R := ZMod q) 0) hc    have hz : Rq.toQuotientHom (powTwoCyclotomic (R := ZMod q) 0) c = 0 := by      by_contra hne      obtain ⟨b, hb⟩ := hisfield.mul_inv_cancel hne      exact hnu (IsUnit.of_mul_eq_one b hb)    have hc0 : c = 0 := by      have hmap : Rq.toQuotientHom (powTwoCyclotomic (R := ZMod q) 0) c          = Rq.toQuotientHom (powTwoCyclotomic (R := ZMod q) 0) 0 := by        rw [hz, map_zero]      exact Rq.toQuotient_injective (powTwoCyclotomic (R := ZMod q) 0) hmap    rw [hc0]    have hzero : Rq.l2NormSq (powTwoCyclotomic (R := ZMod q) 0) (0 : Rq _) = 0 := by      unfold Rq.l2NormSq      refine Finset.sum_eq_zero (fun k _ ↦ ?_)      rw [Rq.zero_val, CompPoly.CPolynomial.coeff_zero, ZMod.valMinAbs_zero, Int.natAbs_zero]      norm_num    rw [hzero]; norm_num  · have hα : 1 ≤ α := hαpos    obtain ⟨r, hr⟩ := exists_sq_eq_neg_one_of_mod_eight_eq_five (q := q) hq5    set g1 : (ZMod q)[X] := X ^ (2 ^ (α - 1)) - C r with hg1    set g2 : (ZMod q)[X] := X ^ (2 ^ (α - 1)) + C r with hg2    set ct : (ZMod q)[X] := c.1.toPoly with hct    have hmul : g1 * g2 = (powTwoCyclotomic (R := ZMod q) α).φ.toPoly := by      rw [hg1, hg2, powTwoCyclotomic_splits_of_sq_eq_neg_one α hr hα, phi_toPoly]    have hirr1 : Irreducible g1 := by      rw [hg1]      apply irreducible_X_pow_sub_C_r α hq5 hα r hr      convert orderOf_q_mod_two_pow hq5 α hα using 2    -- `g2 = X^{2^{α-1}} - C (-r)` with `(-r)² = -1`, reusing the same factor lemma for `-r`.    have hrr : (-r) ^ 2 = -1 := by rw [neg_pow]; simp [hr]    have hg2eq : g2 = X ^ (2 ^ (α - 1)) - C (-r) := by rw [hg2, C_neg, sub_neg_eq_add]    have hirr2 : Irreducible g2 := by      rw [hg2eq]      apply irreducible_X_pow_sub_C_r α hq5 hα (-r) hrr      convert orderOf_q_mod_two_pow hq5 α hα using 2    have hnu : ¬ IsUnit (Ideal.Quotient.mk        (Ideal.span {(powTwoCyclotomic (R := ZMod q) α).φ.toPoly}) ct) := by      have hh := Rq.not_isUnit_toQuotientHom_of_not_isUnit        (powTwoCyclotomic (R := ZMod q) α) hc      rw [Rq.toQuotientHom] at hh      change ¬ IsUnit (Ideal.Quotient.mk        (Ideal.span {(powTwoCyclotomic (R := ZMod q) α).φ.toPoly}) c.1.toPoly) at hh      simpa only [hct] using hh    have hdvd : g1 ∣ ct ∨ g2 ∣ ct := by      by_contra hcon      rw [not_or] at hcon      obtain ⟨hd1, hd2⟩ := hcon      have hcop1 : IsCoprime ct g1 := (hirr1.coprime_iff_not_dvd.mpr hd1).symm      have hcop2 : IsCoprime ct g2 := (hirr2.coprime_iff_not_dvd.mpr hd2).symm      have hcop : IsCoprime ct ((powTwoCyclotomic (R := ZMod q) α).φ.toPoly) := by        rw [← hmul]; exact hcop1.mul_right hcop2      exact hnu (isUnit_mk_of_isCoprime hcop)    have finish : ∀ (g : (ZMod q)[X]) (s : ZMod q),        Irreducible g → g = X ^ (2 ^ (α - 1)) - C s → s ^ 2 = -1 → g ∣ ct →        (q : ℤ) ∣ (Rq.l2NormSq Φ c : ℤ) := by      intro g s hirr hgeq hs hdvdg      haveI : Fact (Irreducible g) := ⟨hirr⟩      have hgmonic : g.Monic := by rw [hgeq]; exact monic_X_pow_sub_C s (by positivity)      have hgnd : g.natDegree = 2 ^ (α - 1) := by rw [hgeq, natDegree_X_pow_sub_C]      let F := AdjoinRoot g      let ζ : F := AdjoinRoot.root g      have hroot : (Polynomial.aeval ζ) g = 0 := by        change (Polynomial.aeval (AdjoinRoot.root g)) g = 0        rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]      have hζ : ζ ^ (2 ^ (α - 1)) = algebraMap (ZMod q) F s := by        have h0 : (Polynomial.aeval ζ) (X ^ (2 ^ (α - 1)) - C s) = 0 := by          rw [← hgeq]; exact hroot        rw [map_sub, map_pow, Polynomial.aeval_X, Polynomial.aeval_C] at h0        linear_combination h0      have hctdeg : ct.natDegree < 2 ^ α := by        have hlt : ct.degree < (powTwoCyclotomic (R := ZMod q) α).φ.toPoly.degree :=          (powTwoCyclotomic (R := ZMod q) α).degree_toPoly_lt_of_reduced c.2        rw [phi_toPoly] at hlt        have hnd : ((X : (ZMod q)[X]) ^ (2 ^ α) + 1).natDegree = 2 ^ α := by compute_degree!        have hφne : ((X : (ZMod q)[X]) ^ (2 ^ α) + 1) ≠ 0 := by          intro h; rw [h, natDegree_zero] at hnd; exact absurd hnd.symm (by positivity)        by_cases hctz : ct = 0        · rw [hctz, natDegree_zero]; positivity        · rw [Polynomial.degree_eq_natDegree hctz,            Polynomial.degree_eq_natDegree hφne, hnd] at hlt          exact_mod_cast hlt      have hmkzero : AdjoinRoot.mk g ct = 0 := AdjoinRoot.mk_eq_zero.mpr hdvdg      have hsum : ∑ k ∈ Finset.range (2 ^ α),          algebraMap (ZMod q) F (ct.coeff k) * ζ ^ k = 0 := by        have he : (Polynomial.aeval ζ) ct = AdjoinRoot.mk g ct := by          change (Polynomial.aeval (AdjoinRoot.root g)) ct = AdjoinRoot.mk g ct          rw [AdjoinRoot.aeval_eq]        rw [Polynomial.aeval_eq_sum_range' hctdeg] at he        rw [hmkzero] at he        rw [← he]        apply Finset.sum_congr rfl        intro k _; rw [Algebra.smul_def]      have hindep : LinearIndependent (ZMod q)          (fun i : Fin (2 ^ (α - 1)) ↦ ζ ^ (i : ℕ)) := by        have hli := (AdjoinRoot.powerBasis' hgmonic).basis.linearIndependent        have hbpow : ⇑(AdjoinRoot.powerBasis' hgmonic).basis            = fun i : Fin (AdjoinRoot.powerBasis' hgmonic).dim ↦              (AdjoinRoot.powerBasis' hgmonic).gen ^ (i : ℕ) :=          (AdjoinRoot.powerBasis' hgmonic).coe_basis        rw [hbpow] at hli        have hdim : (AdjoinRoot.powerBasis' hgmonic).dim = 2 ^ (α - 1) := hgnd        rw [hdim] at hli        exact hli      set a : ℕ → ZMod q := fun k ↦ ct.coeff k with ha      have hcoeff_eq : ∀ k, c.1.coeff k = a k := by        intro k; rw [ha, hct, CompPoly.CPolynomial.coeff_toPoly]      have hdvdj : ∀ j, j < 2 ^ (α - 1) →          (q : ℤ) ∣ ((a j).valMinAbs ^ 2 + (a (2 ^ (α - 1) + j)).valMinAbs ^ 2) := by        intro j hj        exact dvd_sq_add_sq α hα ζ s hζ hs hindep a hsum j hj      have hsumeq : (Rq.l2NormSq Φ c : ℤ)          = ∑ k ∈ Finset.range (2 ^ α), ((c.1.coeff k).valMinAbs ^ 2 : ℤ) := by        unfold Rq.l2NormSq        rw [phi_natDegree, Nat.cast_sum]        apply Finset.sum_congr rfl        intro k _        push_cast        rw [sq_abs]      have hpow : 2 ^ α = 2 ^ (α - 1) + 2 ^ (α - 1) := by        rw [← two_mul, ← pow_succ']; congr 1; omega      rw [hsumeq, hpow, Finset.sum_range_add]      have hpair : (∑ j ∈ Finset.range (2 ^ (α - 1)), ((c.1.coeff j).valMinAbs ^ 2 : ℤ))          + ∑ j ∈ Finset.range (2 ^ (α - 1)),              ((c.1.coeff (2 ^ (α - 1) + j)).valMinAbs ^ 2 : ℤ)          = ∑ j ∈ Finset.range (2 ^ (α - 1)),              ((c.1.coeff j).valMinAbs ^ 2                + (c.1.coeff (2 ^ (α - 1) + j)).valMinAbs ^ 2 : ℤ) := by        rw [← Finset.sum_add_distrib]      rw [hpair]      apply Finset.dvd_sum      intro j hj      rw [Finset.mem_range] at hj      rw [hcoeff_eq j, hcoeff_eq (2 ^ (α - 1) + j)]      exact hdvdj j hj    rcases hdvd with h1 | h2    · exact finish g1 r hirr1 hg1 hr h1    · exact finish g2 (-r) hirr2 hg2eq hrr h2