English
If x > 0 and y > 0 for a Pell solution a, then the sign of the y-coordinate of a^n matches the sign of n for all integers n.
Русский
Если x > 0 и y > 0 для решения Пелля a, то знак y-координаты a^n совпадает со знаком n для всех целых n.
LaTeX
$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \land a_y>0 \rightarrow \forall n\in \mathbb{Z},\; \operatorname{sign}((a^n)_y) = \operatorname{sign}(n)$$$
Lean4
/-- If `(x, y)` is a solution with `x` and `y` positive, then the `y` component of any power
has the same sign as the exponent. -/
theorem sign_y_zpow_eq_sign_of_x_pos_of_y_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (n : ℤ) :
(a ^ n).y.sign = n.sign := by
rcases n with ((_ | n) | n)
· rfl
· rw [Int.ofNat_eq_coe, zpow_natCast]
exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)
· rw [zpow_negSucc]
exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))
