fix: limit ring solver polynomial degree in grind

[leodemoura]

This PR adds a ringMaxDegree configuration option (default 1024) that bounds the maximum degree of polynomials processed by the grind ring solver. Equality constraints whose polynomial exceeds this threshold are discarded (with an issue reported once per goal), preventing pathological degree explosion on inputs such as r ^ (2 ^ 250 - 1).

This PR also introduces Poly.simpM?, a monadic version of Poly.simp? built on the existing safe arithmetic primitives (mulMonM, combineM, mulConstM) in Grind.Arith.CommRing.SafePoly. The previous reflection-oriented Poly.simp? in Sym.Arith.Poly lacked the abort mechanisms needed during proof search, so the simplification path used by EqCnstr now goes through the safe variant. A regression test tests/elab/grind_ring_degree_explosion.lean ensures grind fails quickly on high-degree problems.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-30 14:38:34)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-30 14:38:36)