fix: accept only `denoteInt` spellings as numerals in `grind`'s field inverse rules

This PR fixes a kernel-rejected proof in `grind`'s ring module. For an inverse `a⁻¹` with a numeral `a`, `processInv` asserts `a * a⁻¹ = 1` or `a⁻¹ = 0` with theorems whose numeral is `denoteInt k`, i.e. an `OfNat` numeral or its negation, but the recognizer also accepted `↑(0 : Nat)`, `↑(3 : Int)`, `-0`, and `- -3`, which are only propositionally equal to `denoteInt k`; `Field.inv_zero : 0⁻¹ = 0` was then pushed as a proof of `(↑0)⁻¹ = ↑0`.

The recognizer now accepts the `denoteInt` spellings only, and the other numerals go through the `inv_split` case split, as non-numerals do. Normalization rewrites these spellings in most cases, so the term reached the ring module only through the `Sym.simp`-based normalizer before casts of numerals were normalized (`grind_9321`).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>