Google's Gemini 4 Argon writes a Lean-verified quantum arcsin implementation