English
The map n ↦ (a^n).y is strictly increasing when a is fundamental.
Русский
Отображение n ↦ (a^n).y строго возрастает, когда a — фундаментальное решение.
LaTeX
$$$\text{IsFundamental}(a) \rightarrow \text{StrictMono}(\lambda n:(\mathbb{Z})\,, (a^n).y)$$$
Lean4
/-- The map sending an integer `n` to the `y`-coordinate of `a^n` for a fundamental
solution `a` is strictly increasing. -/
theorem y_strictMono {a : Solution₁ d} (h : IsFundamental a) : StrictMono fun n : ℤ => (a ^ n).y :=
by
have H : ∀ n : ℤ, 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y :=
by
intro n hn
rw [← sub_pos, zpow_add, zpow_one, y_mul, add_sub_assoc]
rw [show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring]
refine
add_pos_of_pos_of_nonneg (mul_pos (x_zpow_pos h.x_pos _) h.2.1) (mul_nonneg ?_ (by rw [sub_nonneg]; exact h.1.le))
rcases hn.eq_or_lt with (rfl | hn)
· simp only [zpow_zero, y_one, le_refl]
· exact (y_zpow_pos h.x_pos h.2.1 hn).le
refine strictMono_int_of_lt_succ fun n => ?_
rcases le_or_gt 0 n with hn | hn
· exact H n hn
· let m : ℤ := -n - 1
have hm : n = -m - 1 := by simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]
rw [hm, sub_add_cancel, ← neg_add', zpow_neg, zpow_neg, y_inv, y_inv, neg_lt_neg_iff]
exact H _ (by cutsat)
