perf: speed up kernel checking of `grind` ring certificates (#15943)

This PR makes the kernel check the certificates of the `grind` ring
solver and of the `Sym.simp` arithmetic normalizer about twice as fast.
It also adds benchmarks for them under `tests/ring_perf`.

The kernel-reduction variants of the `Lean.Grind.CommRing` polynomial
operations now use the recursor-based `Int` operations of
`Init.Data.Int.Kernel` and compute monomial degrees with `Mon.rec`. They
merge sorted monomials and polynomials with nested recursors instead of
fuel. Polynomial multiplication and powers, and the operations for rings
with a known characteristic, non-commutative rings, commutative
semirings and fields, gain such variants, and all certificates use them.
The fuel of `Mon.mul`, `Mon.revlex` and `Poly.combine` is now the length
of their arguments.

The `superpose`, `simp`, `d_step1` and `d_stepk` steps, and their
variants for a known characteristic, now check `p = p₁ + q` in one pass
(`Poly.addEq_k`, `Poly.addEqC_k`). The pass compares the head of `p`
with the heads of `p₁` and `q` by equality, instead of merging `p₁` and
`q` with monomial order comparisons and then comparing the result with
`p`.

The `ToExpr` instances for polynomials, monomials and expressions encode
numerals as `Int.ofNat n`, `Int.negSucc n` and raw `Nat` literals, so
the kernel no longer unfolds `OfNat.ofNat` and `Neg.neg` in
certificates. Proof terms printed by `grind.debug.proof` show these
constructor applications.

Instructions spent in the kernel, measured as the difference between a
normal run and a run with `debug.skipKernelTC`:

| Benchmark | Before | After | Change |
|---|---|---|---|
| `groebner_hard` | 125.5 G | 53.0 G | −57.8% |
| `groebner_char` | 3.1 G | 0.8 G | −73.5% |
| `grind_ring_5` | 4.6 G | 2.9 G | −36.9% |
| `sym_norm` | 6.7 G | 3.8 G | −43.2% |
| All 40 benchmark files | 175.1 G | 84.9 G | −51.5% |

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>