Cleanup: bridge one-variable upper-half-plane stability predicates

[PerAlexandersson]

Parent

Part of #238, milestone 1 ("inventory and alias cleanup").

Problem

The repository currently has two upper-half-plane stability predicates with the
same intended one-variable semantics:

• IsUpperHalfPlaneStable : ℂ[X] → Prop in
  RealRooted/HermiteBiehler.lean;
• MvUpperHalfPlaneStable : MvPolynomial σ ℂ → Prop in
  RealRooted/MultivariateStability.lean.

For σ = Fin 1 (or Mathlib's canonical one-variable index), these should be
connected by a checked equivalence rather than supporting parallel lemma
families. This is API cleanup, not a request for a third stability predicate.

Required outline

1. Inventory Mathlib's canonical equivalence between Polynomial ℂ and a
   one-variable MvPolynomial. Reuse it; do not introduce an ad hoc
   coefficient conversion if Mathlib already supplies the equivalence.
2. Prove the corresponding evaluation formula, including the exact variable
   indexing convention.
3. Prove an ↔ bridge between IsUpperHalfPlaneStable p and
   MvUpperHalfPlaneStable of the converted polynomial.
4. Check the upper-half-plane inequality and nonzero conventions in both
   directions. In particular, zero must remain unstable.
5. Migrate at least one existing cross-boundary consumer to the bridge instead
   of reproving nonvanishing manually.
6. Keep the existing public predicates as compatibility APIs for now. Do not
   mass-rename unrelated Hermite--Biehler or multivariate declarations in this
   issue.

Deduplication rule

After the bridge exists, closure facts should live with the most general
multivariate predicate and be transported to the univariate API when practical.
Do not add duplicate one-variable versions unless their polynomial formulation
is materially easier to use.

Acceptance criteria

• A canonical polynomial/MvPolynomial conversion is identified and used.
• Evaluation compatibility is proved.
• A two-way stability bridge is proved with the checked sign/index convention.
• At least one existing consumer uses the bridge.
• No new primitive stability predicate or admitted analytic fact is introduced.
• Focused and full Lake builds pass without warnings.

[PerAlexandersson]

Implementation audit update:

• Pinned Mathlib provides the canonical equivalence
  MvPolynomial.uniqueAlgEquiv C (Fin 1).
• The polynomial-to-multivariate direction is its inverse.
• MvPolynomial.eval2_uniqueAlgEquiv_symm is the canonical evaluation
  compatibility theorem; variable 0 is the unique Fin 1 coordinate.
• The older pUnitAlgEquiv API is deprecated and should not be used.
• Both local stability predicates use the same strict open upper half-plane
  and both exclude zero.

The isolated cleanup patch adds the evaluation lemma and an iff bridge, then
transports polynomial multiplication from MvUpperHalfPlaneStable.mul and
uses that transported theorem in the existing Hermite--Biehler common-root
cofactor proof. This removes its manual product-nonvanishing split.

The patch is not committed yet because one named argument needs the
identifier correction phi := to φ :=; no build has been run.