Prepare the Mathlib-free polynomial gcd-domain lift

[kim-em]

The proof-only polynomial gcd-domain lift was using its single sorry for all four class fields, and the SPEC's intended arity induction lacked a Mathlib-free multiplicative recursive view. This slice proves the divisibility, nontriviality, and zero-product fields directly, adds toUnivariate_mul at the first variable, and leaves only gcd_exists inside the existing gap.

It also makes the executable LawfulGcdOps domain proof independent of the remaining gcd-existence gap. Exporting an existing HexPoly convolution proof changes its source fingerprint but no executable definition, so the PR records the exact proof-only blob transition required by the benchmark freshness guard. This is an incremental prerequisite for #10082; it does not close the tracker or reduce the remaining literal sorry count.

Validation:

• lake build HexMvGcd HexMvHensel HexMvFactor HexMvFactorizationTests (619 jobs)
• lake build HexMvGcd.Normalize HexMvGcd.Gauss HexMvGcd.Gcd after review cleanup
• python3 scripts/bench/check_factor_sweep_freshness.py
• 75 benchmark-freshness unit tests
• git diff --check
• #print axioms Hex.MvPoly.toUnivariate_mul
• #print axioms Hex.MvPoly.zero_product

Both audited theorems depend only on propext, Classical.choice, and Quot.sound.

[kim-em]

I ran the requested independent Claude Opus review. It found no soundness blocker and confirmed that the new recursive-view multiplication and zero-product proofs are structurally independent of the remaining gcd_exists proof.

I addressed its concrete cleanup concerns:

• Removed the unused private classical division scaffolding, avoiding a future competing-Div problem because Fraction is indexed by the division instance.
• Renamed the public domain lemma to the short, unambiguous zero_product.
• Generalized the private fold helper over its element universe.

I retained toUnivariate_mul in HexMvGcd.View: a minimal build importing only HexMvPoly.Recursive cannot synthesize the MvPoly commutative-ring instance required by the convolution proof. View is the first existing Mathlib-free module with both the recursive definitions and packaged ring laws.

I also left the pre-existing polynomial GcdDomainLaws instance priority unchanged. Lowering it would not create a clean alternative yet: the executable LawfulGcdOps construction still has other proof fields that were elaborated through the Gauss-law path. That broader instance cleanup should accompany closure of gcd_exists.

[kim-em]

The superseded CI run caught the benchmark freshness fingerprint for HexPoly/Euclid/MulRing.lean. I added the required exact proof-only transition record. The factorization freshness checker and its 75 unit tests now pass locally; a new CI run is starting on the amended head.