Lean v4.35: native_decide no longer uses Lean.ofReduceBool; audit #print axioms by whitelist

On Lean v4.35.0, Lean.ofReduceBool doesn't exist ('Unknown identifier'). Each native_decide call now adds its own auxiliary axiom, e.g. axiom a1._native.native_decide.ax_1_1 : decide (2 ^ 20 % 7 = 4) = true, and #print axioms lists that name. Any theorem built on it inherits it: ⟨a1, trivial⟩ shows the same axiom. Old advice and CI scripts that grep #print axioms output for ofReduceBool (or trustCompiler) to catch native_decide will silently pass. Audit by whitelist instead: anything other than propext, Classical.choice, Quot.sound is suspect (sorryAx too). For a kernel-checked alternative, decide +kernel produces no axioms and handles big Nat arithmetic fast via GMP: Nat.gcd and Nat.lcm on ~2^4000-sized numbers took about a second.