[Dijkstra] Rewire LEDGER-pov to consume the proved PoV modules and drop the discharged parameters

# Description

**Context**: PR #1203 (`LEDGER-pov`, #1187), PR #1189 (UTxO/UTxOW PoV, #1186), PR #1210 (Certs PoV, #1185).

PR #1203's module-parameter block is a frozen contract while the follow-up PRs land; the parameters stay in place even after their providers merge. This issue is the mechanical integration step: rewire `Ledger.Properties.PoV` to consume the proved modules and delete the discharged parameters.

## UTxO side (once #1203 and #1189 are both in)

+ Delete the parameters `balance-∪`, `split-balance`, `outs-disjoint` (now theorems in `Utxo.Properties.Base`) and `utxow-pov-invalid`, `UTXOW-V-mechanical`, `UTXOW-batch-balance-coin`, `subutxow-step-coin` (provided by `Utxow.Properties.PoV`).
+ Replace them with the instantiation already verified to elaborate `LEDGER-pov` end-to-end (full snippet in PR #1189's description):

```agda
open UTXOW-PoV tx noMintSubTx
open SUBUTXOW-PoV subtx-fresh-txid subtx-spend-agree -- parameters until #1274 lands
```

with the η-wrappers `λ {u} {u'} → balance-∪ {u} {u'}` and `λ {u} → outs-disjoint tx {u}` wherever the balance algebra is consumed directly.
+ Discharge `noMintTx` from premise 7 of the extracted `UTXO` step instead of keeping it as a parameter (`UTXO-batch-balance-coin` in `Utxo.Properties.PoV` already does this internally).
+ Deduplicate `noMintingSubTxs` (defined in both `Ledger.Properties.PoV` and `Utxo.Properties.PoV`).
+ Update the stale `-- open UTXOW-PoV tx (λ {u}{u'} → balance-∪ {u}{u'}) split-balance noMintTx noMintSubTx …` comment in `Ledger/Properties/PoV.lagda.md` — that interface predates PR #1189 (`balance-∪`/`split-balance`/`outs-disjoint`/`noMintTx` are no longer `UTXOW-PoV` parameters).

## Certs and Gov sides

Apply the same treatment to `CERTS-pov`/`batch-cert-deposits-bridge` once PR #1210 (#1185) merges, and to the gov-deposit parameters once #1276 lands.

## Remaining parameters

`utxo₁-tx-spend-eq`, `fresh-top-tx-id`, and the `SUBUTXOW-PoV` invariants stay until #1274 is resolved; `ENTITIES`/`SUBENTITIES-wdrls-bounded` stay until #1275 is resolved.

Start in Ledger/Properties/PoV.lagda.md and compare the UTXO integration with the verified snippet from PR #1189; inspect UTXOW-PoV, SUBUTXOW-PoV, and the referenced Utxo.Properties.PoV definitions. Re-elaborate LEDGER-pov after removing only discharged parameters, then apply the CERTS and gov changes when their prerequisite issues are resolved; done means the remaining-parameter list still matches #1274–#1276.

Written by the indexing model from the issue text.