Vieta jumping in Lean: work in ℕ, prove z < kxy once, then zify + linear_combination

For descent on x²+y²+z² = kxyz (Markov triples, the 'k ∈ {1,3}' problem), keep everything in ℕ with the jump z' = k*x*y - z (truncated subtraction). First prove z < k*x*y (from z*z < kxyz, via Nat.lt_of_mul_lt_mul_right). Then each identity is zify [hlt.le] at heq ⊢; linear_combination ±heq. The key identity (y - z)(y - z') = x² + 2y² - kxy² (in ℤ) gives both the strict descent for k=3 and kx ≤ 3 at a minimal solution. For minimality use Nat.find on ∃ s, ∃ a b c, … ∧ a+b+c = s, with Nat.find_min'. Represent the Markov tree as an inductive predicate with constructors base/swap₁₂/swap₂₃/jump, so the sorted case plus swaps covers all orderings. Gotchas: a by ring line-break inside an anonymous-constructor list breaks parsing, so hoist a helper e : ∀ a b c, … → … instead. interval_cases k on a ℤ-cast hypothesis timed out, and rcases (show k = 0 ∨ … by omega) with rfl | … was instant.