WIP: Clay Millennium Prize Problems (missing statements)

Hi! I am preparing formalised statements for the three Clay Millennium problems that are not yet in `FormalConjectures/Millenium/`, and will open a Pull Request once the branch is ready.

## Scope

| Problem | Proposed path | Status in this package |
|---------|----------------|------------------------|
| **Hodge conjecture** | `FormalConjectures/Millenium/Hodge.lean` | `research open` (main); Lefschetz (1,1) and weight 0 as `research solved` |
| **Birch–Swinnerton-Dyer** | `FormalConjectures/Millenium/BirchSwinnertonDyer.lean` | `research open` (full Clay statement); Gross–Zagier/Kolyvagin rank ≤ 1 as `research solved` |
| **Yang–Mills existence and mass gap** | `FormalConjectures/Millenium/YangMills.lean` | `research open` (∀ compact simple $G$; OS axioms and mass gap $\Delta > 0$) |

**Already present in the repository (not re-proposed here):**

- `Millenium/RiemannHypothesis.lean`
- `Millenium/Poincare.lean`
- `Millenium/PvsNP.lean`
- `Millenium/NavierStokes.lean`

Opening this issue as a WIP to coordinate and avoid duplicated efforts on the remaining three.

## Design notes (for reviewers)

These statements deliberately use **opaque interfaces** where Mathlib (and this repo) do not yet expose the full analytic/geometric package required by the Clay formulations:

| File | Opaque interfaces (summary) |
|------|-----------------------------|
| **Hodge** | `ComplexProjectiveVariety`, `HodgeClass`, `IsAlgebraicClass` |
| **BSD** | elliptic curve over $\mathbb{Q}$, algebraic/analytic rank, period, regulator, Sha order, Tamagawa product, torsion order, leading coefficient of $L(E,s)$ |
| **Yang–Mills** | compact simple Lie group, physical Hilbert space, Hamiltonian, vacuum / first-excitation energies, Osterwalder–Schrader axioms as a non-trivial `Prop` |

Packaging choices shared with our other contributions:

- One principal `@[category research open]` per Clay problem (no double-counting via unpacked forms).
- Unpacked / specialised forms use `@[category API]` or `textbook` with `(H : type_of% …)` so they do not inherit `sorry` from the open statement.
- **BSD:** full conjecture is the single open theorem; rank equality and leading term appear as textbook consequences of that hypothesis (not three separate open problems). Gross–Zagier/Kolyvagin for algebraic rank ≤ 1 remains `research solved`.
- **Yang–Mills:** `SU(3)` is an `opaque` constant (not a global `axiom`); the QCD special case is a textbook specialisation under the main hypothesis.
- **Hodge:** Lefschetz theorem on $(1,1)$-classes and the weight-zero case are recorded as classical `research solved` variants.
- Cross-links: BSD notes existing Weierstrass/rank material in `Wikipedia/EllipticCurveRank.lean` without duplicating it.

## Observations / questions for maintainers

1. **Folder name:** files target `FormalConjectures/Millenium/` to match the existing directory spelling in this repository (not “Millennium”).
2. **Opacity vs Mathlib:** if maintainers prefer thinner statements (e.g. BSD only as rank equality, or Yang–Mills only via an external reference), happy to trim or split in review.
3. **BSD tracking:** an alternative is two independent `research open` statements (rank vs leading term) with the full conjecture as `API` conjunction; we chose the single Clay open for metric cleanliness—open to flipping if preferred.
4. **Formal proofs:** long proofs are not included (repository policy). Solved variants use `sorry` with informal acceptance documented in docstrings; links via `formal_proof` can be added where a citable formalisation exists.
5. **AI assistance:** if the PR description should declare tooling used for drafting, please say so in the issue thread and I will include it in the PR.

References in each file point to the Clay PDF statements and Wikipedia (plus Osterwalder–Schrader for Yang–Mills).

Feedback welcome before the PR.

Review the existing files in FormalConjectures/Millenium/, especially RiemannHypothesis.lean, Poincare.lean, PvsNP.lean, and NavierStokes.lean, before assessing the proposed Hodge.lean, BirchSwinnertonDyer.lean, and YangMills.lean statements. Confirm the opaque interfaces, category annotations, cross-links, and single-open-theorem choices with maintainers; done means the three files are ready for a coordinated pull request.

Written by the indexing model from the issue text.