Formalise the Poisson conjecture and the JC ⟹ PC ⟹ DC chain (United Conjectures, math/0608009 Thm 7)

Follow-up to the disproof of the Jacobian conjecture (#4474).

### Relation to existing issues

- **#1837 already covers the Dixmier conjecture**, specifically `DC_1` — every endomorphism of the first Weyl algebra `A₁ = k⟨x, y | yx - xy = 1⟩` is an automorphism — and correctly flags that `A₁` is not yet in Mathlib as the blocking prerequisite. That issue remains the home for the Dixmier conjecture itself; this one does not duplicate it, and the `WeylAlgebra` definition proposed below is intended to discharge its prerequisite.
- **#4474** is the disproof of the Jacobian conjecture, which is what makes the chain below load-bearing rather than decorative.

What is *not* covered anywhere yet, and is the subject of this issue: the **Poisson conjecture**, and the **implication chain** tying `JC`, `PC`, and `DC` together across dimensions.

### The chain

Per [Adjamagbo–van den Essen, arXiv:math/0608009](https://arxiv.org/abs/math/0608009) ("United Conjectures", Theorem 7), for each dimension `n` (characteristic zero):

```
JC_2n ⟹ PC_n ⟹ DC_n ⟹ JC_n
```

with `DC_n ⟹ JC_n` classical ([Bass–Connell–Wright, Bull. AMS 7 (1982)](https://doi.org/10.1090/S0273-0979-1982-15032-7)). Since `JC_n` is now false for all `n ≥ 3`, the Dixmier and Poisson conjectures are false for all `n ≥ 3`, and the surviving open cases form the totally ordered chain

```
PC_2 ⟹ DC_2 ⟹ JC_2 ⟹ PC_1 ⟹ DC_1
```

with `DC_1` = Problem 1 of Dixmier (1968) — the `DC_1` of #1837 — as the weakest open link.

### Plan

Two stacked PRs, statements only; implications registered as cited sorries.

1. Canonical Poisson bracket on `MvPolynomial (σ ⊕ σ) R` + per-dimension `PC_n` statements. **New work, no overlap.**
2. `WeylAlgebra R σ` (RingQuot of the free algebra by the canonical commutation relations) + the implications `PC_n ⟹ DC_n` and `DC_n ⟹ JC_n`.
- The `WeylAlgebra R σ` definition is the Mathlib prerequisite #1837 identifies as missing; landing it here unblocks that issue rather than competing with it.
- The per-dimension `DC_n` statements belong to #1837 as its `n`-dimensional generalisation. Happy to land them there instead, or here and cross-link — reviewer's preference.

Announced in the Zulip thread [#AI authored projects > Counterexample to the Jacobian conjecture](https://leanprover.zulipchat.com/#narrow/channel/AI.20authored.20projects/topic/Counterexample.20to.20the.20Jacobian.20conjecture).

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

Start by reading the existing Jacobian conjecture work in #4474 and the Dixmier conjecture context in #1837, then review Theorem 7 of United Conjectures. The first PR is done when the canonical Poisson bracket on MvPolynomial (σ ⊕ σ) R and the per-dimension PC_n statements exist; the second adds WeylAlgebra R σ and the cited PC_n ⟹ DC_n and DC_n ⟹ JC_n implications as statements.

Written by the indexing model from the issue text.