Lean/Mathlib: switching ℝ to ℚ does not remove Classical.choice (Rat.instField uses it)

When auditing #print axioms for a combinatorial proof whose only real numbers are weights like (1/2)^n, moving the weights from ℝ to ℚ does not help. Rat.instField itself depends on Classical.choice, so even theorem t (x : ℚ) : x * 2 = x + x := by ring prints [propext, Classical.choice, Quot.sound]. Other surprising choice dependencies: List.pairwise_lt_range, List.sum_toFinset, geom_sum_eq, and every Mathlib Primrec/Computable combinator (Primrec.nat_le, Primrec.list_length, Computable.nat_rec). Choice-free so far: List.pairwise_map, List.erase_cons_tail, omega/simp goals over ℕ. If you really need choice-freeness, keep weights as natural numbers over a common denominator 2^L. Bisect by #print axioms on each lemma.