Is Unit of l1Norm le

theorem isUnit_of_l1Norm_le (hq5 : q % 8 = 5) {c : Rq Φ} {κ : ℕ}    (hpos : 0 < ‖c‖₁) (hle : ‖c‖₁ ≤ κ) (hκ : κ ^ 2 < q) :    IsUnit c := by  by_contra hc  -- Algebraic core: a non-unit has `q ∣ ‖c‖₂²`.  have hdvd : (q : ℤ) ∣ (Rq.l2NormSq Φ c : ℤ) := q_dvd_l2NormSq_of_not_isUnit α hq5 hc  have hdvdn : q ∣ Rq.l2NormSq Φ c := by exact_mod_cast hdvd  -- Norm bridge + hypotheses: `‖c‖₂² ≤ ‖c‖₁² ≤ κ² < q`.  have hb : Rq.l2NormSq Φ c < q :=    lt_of_le_of_lt (le_trans (Rq.l2NormSq_le_l1Norm_sq α c) (Nat.pow_le_pow_left hle 2)) hκ  -- A multiple of `q` below `q` is `0`.  have hz : Rq.l2NormSq Φ c = 0 := Nat.eq_zero_of_dvd_of_lt hdvdn hb  -- Zero squared norm ⇒ `c = 0`, contradicting `‖c‖₁ > 0`.  have hc0 : c = 0 := Rq.eq_zero_of_l2NormSq_eq_zero α hz  have hl1zero : Rq.l1Norm Φ (0 : Rq Φ) = 0 := by    unfold Rq.l1Norm    refine Finset.sum_eq_zero fun k _ ↦ ?_    rw [Rq.zero_val, CompPoly.CPolynomial.coeff_zero, ZMod.valMinAbs_zero, Int.natAbs_zero]  rw [hc0, hl1zero] at hpos  exact absurd hpos (lt_irrefl 0)