refactor: move cons_zero and cons_zero_many to CommRing section

These theorems no longer depend on `[Field R]` — they only need
`[CommRing R] [LinearOrder R] [IsStrictOrderedRing R]`.

Renamed `affineOfBinary_cons_zero_field` → `affineOfBinary_cons_zero`
since the `_field` suffix was indicating the now-removed Field dependency.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em