English
If d > 0 and d is not a square, the group of solutions to the Pell equation x^2 − d y^2 = 1 has a unique positive generator up to sign.
Русский
Если d > 0 и не является квадратом, группа решений уравнения Пелля x^2 − d y^2 = 1 имеет единственный положительный генератор ( up to sign ).
LaTeX
$$$\forall d \in \mathbb{Z},\; d > 0 \land \lnot \text{IsSquare}(d) \Rightarrow \exists! a_1 \in \text{Solution}_1(d),\; 1 < a_1.x \land 0 < a_1.y \land \forall a \in \text{Solution}(d),\; \exists n \in \mathbb{Z},\; a = a_1^{n} \lor a = -a_1^{n}.$$$
Lean4
/-- When `d` is positive and not a square, then the group of solutions to the Pell equation
`x^2 - d*y^2 = 1` has a unique positive generator (up to sign). -/
theorem existsUnique_pos_generator (h₀ : 0 < d) (hd : ¬IsSquare d) :
∃! a₁ : Solution₁ d, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ a : Solution₁ d, ∃ n : ℤ, a = a₁ ^ n ∨ a = -a₁ ^ n :=
by
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd
refine ⟨a₁, ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩, fun a (H : 1 < _ ∧ _) => ?_⟩
obtain ⟨Hx, Hy, H⟩ := H
obtain ⟨n₁, hn₁⟩ := H a₁
obtain ⟨n₂, hn₂⟩ := ha₁.eq_zpow_or_neg_zpow a
rcases hn₂ with (rfl | rfl)
· rw [← zpow_mul, eq_comm, @eq_comm _ a₁, ← mul_inv_eq_one, ← @mul_inv_eq_one _ _ _ a₁, ← zpow_neg_one, neg_mul, ←
zpow_add, ← sub_eq_add_neg] at hn₁
rcases hn₁ with hn₁ | hn₁
· rcases
Int.isUnit_iff.mp
(isUnit_of_mul_eq_one _ _ <| sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
(rfl | rfl)
· rw [zpow_one]
· rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy
exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)
· rw [← zpow_zero a₁, eq_comm] at hn₁
exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)
· rw [x_neg, lt_neg] at Hx
have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx
norm_num at this
