[Dijkstra] Certs PoV

# Description

**Parent issue**: #1187 (LEDGER PoV)

**Builds on**: #1203 (the `LEDGER-PoV` contract), #1250 (explicit-deposit certificates / `newCertDeposits`)

This issue discharges the **five Certs-side module parameters** of the `LEDGER-PoV` contract (the parameter block of `module LEDGER-PoV` in `src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md`, frozen by #1203) as theorems, with statements matching the contract verbatim.

**Implementation**: PR #1210 (stacked on #1203's branch; retarget to `master` once #1203 merges).

## The five target statements

All vocabulary from `Ledger.Dijkstra.Specification.Certs`:

- **`CERTS-rewards-pov`** — a `CERTS` run preserves the rewards balance:
`Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s'`
- **`CERTS-deposits-pov`** — closed-form deposit accounting, under `PoolDepositsRegistered s`:
`coinFromDeposits s + newCertDeposits (PParamsOf Γ) (dom (PoolsOf s)) dCerts ≡ coinFromDeposits s' + refundCertDeposits (PParamsOf Γ) dCerts`
- **`CERTS-deposits-registered`** — a `CERTS` run preserves `PoolDepositsRegistered`.
- **`CERTS-new-thread`** — `newCertDeposits` over an appended certificate list splits at a `CERTS`-run boundary, the second half charged against the run's *final* pool set (what lets per-step accounting compose across a batch).
- **`refundCertDeposits-++`** — `refundCertDeposits` distributes over `_++_`.

## Decomposition

In Dijkstra, `CERTS` is a plain reflexive–transitive closure of the single-certificate rule `CERT` — the withdrawal and direct-deposit handling formerly attached to the Conway-era `CERTS` (the old `PRE-CERT`/`POST-CERT` phases) lives at the `ENTITIES` layer and is proved inside #1203 (`Entities.Properties.{PoV,ApplyToRewardsPoV}`). So each fact is an induction over the closure whose step case is a per-`CERT` lemma, plus fold algebra for the deposit folds:

- **Per-step accounting** — case split over the eight `DELEG`/`POOL`/`GOVCERT` rules. `_∪⁺_` additions add their deposit to the pot total (`getCoin-∪⁺-singleton`, new in `Ledger.Prelude`); removals split off the entry whose value the rule's membership premise pins down (`getCoin-remove`); `POOL-reg` adds through a *left-biased* union, so it needs the key fresh in the pot — the rule's premise gives freshness in `pools`, and `PoolDepositsRegistered` transports it to the pot. That is the invariant's only use, and it is preserved because `POOL-reg` extends pot and pool map by the same key.
- **Pool-set threading** — `newCertDeposits` folds a pair accumulator (coin so far, pool keys registered so far); `nextPools`/`CERT-poolSet` identify the accumulator's evolution with `dom (PoolsOf -)` across a `CERT` step, up to `≡ᵉ`, absorbed by a congruence lemma (the fold consumes the set only through membership tests). Since the fold's per-step function is local to `Certs`, the fold lemmas reach it through `newCertDeposits` itself via seed certificates (a fold state `(d , P)` is definitionally the fold from `(0 , P)` over one `delegate`/`regdrep` certificate carrying deposit `d`).

## Modules

| Module | Purpose |
|--------|---------|
| `Certs.Properties.PoVLemmas` | per-`CERT`-step lemmas (`CERT-rewards-pov`, `CERT-deposits-pov`, `CERT-deposits-registered`, `CERT-poolSet`) and fold lemmas (`newCertDeposits-∷`/`-cong`, shift lemmas, `refundCertDeposits-++`) |
| `Certs.Properties.PoV` | the five `CERTS`-level facts, statements matching the `LEDGER-PoV` parameters verbatim |
| `Ledger.Prelude` (additions) | `getCoin-∪⁺-singleton`, `getCoin-remove`, `dom-∪ˡ-singleton` and supporting `∪⁺` lemmas |

## Acceptance criteria

- [ ] All five `LEDGER-PoV` Certs-side parameters are provable by direct substitution (statements verbatim); verified by a drop-in instantiation of `LEDGER-PoV`.
- [ ] Everything compiles under `--safe`, with **no deferred module parameters** on the Certs side.
- [ ] Both property modules are registered in `Certs.Properties` (reachable from the `Ledger.Dijkstra` root).
- [ ] Follow-up (out of scope here): the mechanical rewiring of `Ledger.Properties.PoV` to `open` these proofs in place of its parameters — the Certs analogue of #1277.

## References

- The contract: `module LEDGER-PoV` parameters in `src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md` (#1203).
- The consumer: `Entities.Properties.PoV` (`module ENTITIES-PoV`, inside #1203).
- Deposit folds and `PoolDepositsRegistered`: `src/Ledger/Dijkstra/Specification/Certs.lagda.md` (#1250).
- Sibling UTxO-side issue/PR: #1186 / #1189.

---

*History (2026-08-05): this body was rewritten. The previous version predated #1250 and #1203's contract restatement: it targeted a single `CERTS-pov` lemma with the withdrawal/direct-deposit flows attached to `CERTS` and an `applyToRewards` fold decomposition — that machinery now lives at the `ENTITIES` layer inside #1203, and the three agda-sets bridging assumptions it listed are the `ApplyToRewards-PoV` parameters there, no longer in this issue's scope.*