Hurwitz's √5 theorem in Lean without continued fractions (Farey/Stern–Brocot), ~300 lines

Mathlib's GenContFract API is heavy. Hurwitz's theorem (|α - q| < 1/(√5 den²) infinitely often) is much easier by Hardy–Wright Thm 193. (1) Bracketing by induction on N: ∃ a b c d : ℤ, 0<b, 0<d, b*c - a*d = 1, a/b < α < c/d, N ≤ b+d. Base case ⌊α⌋/1 and (⌊α⌋+1)/1, where strictness comes from irrationality: hα ⟨⌊α⌋, by push_cast; exact h⟩. Step: α ≠ the mediant, so lt_or_gt_of_ne decides which endpoint to replace, and the determinant and omega take care of the rest. (2) Of a/b, mediant, c/d, one is good. Otherwise, summing the two failed bounds next to α gives B²+D² ≤ √5BD and B²+(B+D)² ≤ √5B(B+D). Divide by B² with t = D/B : ℚ: (2t-√5)² ≤ 1 and (2t+2-√5)² ≤ 1 force √5 = 2t+1, contradicting Nat.Prime.irrational_sqrt (by decide : Nat.Prime 5). norm_num can't prove Nat.Prime 5 without the extension import, but decide can. (3) Infinitude: if the set were finite, Finset.inf' of |α - q| over hfin.toFinset is positive (Finset.lt_inf'_iff), and a good q inside a bracket of length 1/(bd) ≤ 1/(N+1) contradicts it. For den((x:ℚ)/y) ≤ y, rewrite with ← Rat.divInt_eq_div and use Int.le_of_dvd hy (Rat.den_dvd x y). Sharpness for φ: n²(q-φ)(q-ψ) = p²-pn-n² is a nonzero integer (linear_combination with goldenRatio_add_goldenConj and goldenRatio_mul_goldenConj). The finiteness goes through (hbox.preimage hinj.injOn).subset, with q ↦ (num, den) injective by Rat.ext. Gotcha: linear_combination needs Mathlib.Tactic.LinearCombination explicitly in a module file, and otherwise it fails as 'unknown tactic'.