Davenport–Cassels (Aubry's trick) in Lean: an all-integer descent, ~150 lines

Goal: if n ∈ ℤ is Q(x) for a rational x, with Q = ∑ c_i x_i², c_i > 0 and ∑ c_i < 4, then it is Q of an integer point. Stay in ℤ: v : Fin k → ℤ, d : ℕ, Q v = n d². Strong induction on d (Nat.strong_induction_on). Rounding: for each coordinate, use u % d and u / d (Int.emod_add_mul_ediv u d : u % d + d*(u/d) = u) and pick t = u/d or u/d+1 depending on 2(u%d) ≤ d. nlinarith then gives 4(u - d t)² ≤ d². Collect with fun i => (key (v i)).choose. Descent step: a = Q y - n, b = 2(n d - B v y), d' = a d + b, v' = a v + b y. Then d·d' = Q(v - d y) (one ring after rewriting Q(v - dy) = Qv - 2d B + d² Qy), so 0 < d' < d unless v = dy. Q(v') = n d'² is a single rw [Q_comb, ...]; ring, where Q_comb : Q(a v + b w) = a² Q v + 2ab B v w + b² Q w is proved by simp only [Q, B, mul_sum, ← sum_add_distrib]; exact sum_congr rfl fun i _ => by ring. Clearing rational denominators: D = ∏ den_i and v_i = num_i * ∏_{j≠i} den_j. Then (v_i : ℚ) = x_i * D by Finset.mul_prod_erase and Rat.mul_den_eq_num. Gotcha: an explicit section variable (c) that a lemma statement doesn't mention is NOT included, so don't pass it. Corollary: r ≥ 0 rational is a sum of three rational squares iff num·den ≠ 4^a(8b+7). To evaluate (7/4 : ℚ).num, decide gets stuck; rewrite to Rat.divInt 7 4 and use Rat.num_divInt / Rat.den_divInt.