Ramanujan–Nagell in Lean: QuadraticAlgebra ℤ (-2) 1 plus norm descent (no UFD), and Skolem's p-adic step via linear_combination

For x²+7 = 2ⁿ: (1) Mathlib's QuadraticAlgebra ℤ (-2) 1 is ℤ[ω] with ω² = ω - 2. It has @[simp] re_mul/im_mul, ext, and norm as a MonoidHom (norm_def: re² + b·re·im - a·im²). You don't need a UFD instance. Prove N z = 2^k → z = ±ωⁱω̄ʲ by induction on k. An even norm means re or re+im is even (Int.even_mul), and the quotient by ω or ω̄ is an explicit ⟨_, _⟩ checked by ext <;> simp. (2) Name the Lucas sequence as a structural def u with u (m+2) = u (m+1) - 2 u m, and prove w^(m+1) = ⟨-2 u m, u (m+1)⟩. Small values then go by decide or simp [u]. (3) Skolem lifting: (1+s)^(7^l r) = 1 + 7^l r s + 7^(l+1) c, with s² = -7. In the inductive step, introduce X and Y as opaque variables via obtain ⟨X, hX⟩ : ∃ X, X = ... := ⟨_, rfl⟩, NOT set, so linear_combination/ring see them as atoms. Then the whole (1+X)^7 step is one linear_combination 7*hX + (7*Q' + X*(X⁴ + X²·K + K²))*hX2 with hX2 : X² = K. Mathlib's dvd_sub_pow_of_dvd_sub : ↑p ∣ a - b → ↑p^(k+1) ∣ a^p^k - b^p^k gives 7^(l+1) ∣ 8^(r·7^l) - 1. Gotchas: Int.ModEq notation and Int.prime_iff_natAbs_prime need extra imports in a module file (Mathlib.RingTheory.Int.Basic for the latter). Nat.exists_eq_pow_mul_and_not_dvd splits off the 7-part of t. norm_num can't prove Nat.Prime 7 without its extension import, so use decide.