[Dijkstra] Prove `updateCertDepositsStep` agrees with `CERT` sub-rule deposit updates

## Summary

Add a property in `Ledger.Dijkstra.Specification.Certs.Properties` formalizing the invariant that the cert-deposit step function `updateCertDepositsStep` and the operational `CERT` sub-rule produce *identical* deposit updates on every certificate.

The TODO was flagged in `src/Ledger/Dijkstra/Specification/Certs.lagda.md` in the "Cert-State Deposit Accounting" section (PR #1209, issue #1208).

## Why this matters

The `consumedBatch ≡ producedBatch` equation in the `UTXO` rule depends on `newCertDeposits` and `refundCertDeposits`, which are derived from `updateCertDepositsStep` (and its iterated form `updateCertDeposits`), while the actual `CertState` evolution of deposits is determined by the `CERT` sub-rules (`DELEG`, `POOL`, `GOVCERT`).

Any drift between the two is a soundness problem: it would make it possible to have a valid `consumedBatch ≡ producedBatch` equation in list of `UTXO` premises for a transaction whose genuine `CertState` deposits evolution doesn't balance — i.e. transactions that create or destroy value out of thin air relative to the deposit of the `CertState`.

The `Utxo.lagda.md` "Design Note: Cert-State Threading and Deposit Accounting" already records the obligation in prose; this issue tracks formalizing it as a proof.

## The property

In `Ledger.Dijkstra.Specification.Certs.Properties` (parameterized only by `GovStructure`), state and prove:

```agda
CERT-updateCertDepositsStep :
∀ {Γ : CertEnv} {s s' : CertState} {c : DCert}
→ Γ ⊢ s ⇀⦇ c ,CERT⦈ s'
→ depositTripleOf s' ≡ depositTripleOf (updateCertDepositsStep (PParamsOf Γ) s c)
```

Equivalently (and likely the form that falls out cleanest from case analysis on `CERT-deleg` / `CERT-pool` / `CERT-gov`):

```agda
CERT-updateCertDeposit :
∀ {Γ : CertEnv} {s s' : CertState} {c : DCert}
→ Γ ⊢ s ⇀⦇ c ,CERT⦈ s'
→ depositTripleOf s' ≡ updateCertDeposit (PParamsOf Γ) c (depositTripleOf s)
```

The two forms are interconvertible: `updateCertDepositsStep pp s c` updates the three deposit fields of `s` from the components of `updateCertDeposit pp c (depositTripleOf s)`, so `depositTripleOf (updateCertDepositsStep pp s c) ≡ updateCertDeposit pp c (depositTripleOf s)` is provable definitionally (or with a single `refl` after `case`-splitting `c`).

The natural RTC sibling, which `LEDGER-pov` will consume:

```agda
CERTS-updateCertDeposits :
∀ {Γ : CertEnv} {s s' : CertState} {cs : List DCert}
→ Γ ⊢ s ⇀⦇ cs ,CERTS⦈ s'
→ depositTripleOf s' ≡ depositTripleOf (updateCertDeposits (PParamsOf Γ) s cs)
```

by induction on the `BS-ind` structure of `_⊢_⇀⦇_,CERTS⦈_`, using `CERT-updateCertDepositsStep` at each step.

## Proof sketch

Case-split on the `CERT` constructor:

+ **`CERT-deleg`**. Case-split on `DELEG-delegate` / `DELEG-dereg`. Each `DELEG` constructor updates exactly the `DState.deposits` field; `updateCertDeposit` does likewise on the first component of the `DepositTriple`. Pool and gov deposits unchanged.
+ **`CERT-pool`**. Case-split on `POOL-reg` / `POOL-rereg` / `POOL-retirepool`. `POOL-reg` updates `PState.deposits` with `pools ∪ˡ ❴ kh , poolDeposit ❵`, matching the `regpool` case of `updateCertDeposit`. `POOL-rereg` and `POOL-retirepool` leave deposits untouched (`updateCertDeposit` also leaves all three components unchanged for `retirepool`, and there is no `rereg` cert constructor — see below).
+ **`CERT-gov`**. Case-split on `GOVCERT-regdrep` / `GOVCERT-deregdrep` / `GOVCERT-ccreghot`. The first two update `GState.deposits` in the way `updateCertDeposit` does for `regdrep` / `deregdrep`; `ccreghot` leaves deposits unchanged.

## Notes / things to watch

+ **`POOL-rereg` vs `regpool`**. `POOL-rereg` fires on the same `regpool kh _` cert as `POOL-reg` (gated by `Is-just (isPoolRegistered pools kh)`). Crucially `POOL-rereg`'s result state leaves `deposits` untouched, while `updateCertDeposit`'s `regpool` case computes `dp ∪ˡ ❴ kh , pp .poolDeposit ❵`. On a pre-existing `kh`, `_∪ˡ_` is left-biased so the existing value is preserved and the singleton is dropped — so the two agree. This is exactly the "do not count pool deposits a second time when reregistering pools" property already enforced by `_∪ˡ_`'s left-bias (and noted in the Conway CHANGELOG). The proof of `CERT-updateCertDeposit` will need this left-bias fact, possibly as a small helper lemma `pp ∪ˡ ❴ k , v ❵ ≡ pp` when `k ∈ dom pp`.
+ **No-op `CERT` constructors**. Several `CERT` paths leave `deposits` unchanged on the operational side (`POOL-rereg`, `POOL-retirepool`, `GOVCERT-ccreghot`). `updateCertDeposit`'s wildcard `_` case (`retirepool`, `ccreghot`, `reg` if present) similarly returns the input triple unchanged. Verify constructor-for-constructor that the wildcard cases line up.
+ **`reg` cert**. Dijkstra's `DCert` includes a `reg` constructor (see Conway's `updateCertDeposit`). `updateCertDeposit` in Dijkstra currently hits the wildcard case for `reg` — confirm this is intentional (Dijkstra DELEG appears not to have a `DELEG-reg` constructor in the current spec, unlike Conway). If a `DELEG-reg` is added later, both the helper functions and this proof need updating.

## Acceptance criteria

+ `CERT-updateCertDepositsStep` (or the equivalent `CERT-updateCertDeposit`) lives in `Ledger.Dijkstra.Specification.Certs.Properties` (parameterised over `GovStructure`), typechecks under `--safe`.
+ RTC sibling `CERTS-updateCertDeposits` typechecks, by induction on `BS-ind`.
+ The TODO marker in `src/Ledger/Dijkstra/Specification/Certs.lagda.md` (section "Cert-State Deposit Accounting") is removed, replaced with a cross-reference to the new property.
+ The "consistency obligation" mentioned in the prose in the Utxo module, just before the "Consumed and Produced" section, is discharged, or at least the paragraph is updated to reflect what we proved.
+ CHANGELOG entry recording the new soundness lemma.

## Out of scope

+ The coin-form bridges `CERT-coinFromDeposits-step` and `CERTS-coinFromDeposits-updateCertDeposits` — those are downstream consequences (apply `cong coinFromDepositTriple`) and are tracked by the Certs PoV PR / issue.
+ Any `Ledger.Properties.PoV` work.

## Related

+ PR #1209 / issue #1208: introduced the TODO.
+ Branch `1185-dijkstra-NEW-ENTITIES-certs-pov`: the Certs PoV PR that will hopefully discharge this issue.

Start in src/Ledger/Dijkstra/Specification/Certs.Properties and inspect the CERT, DELEG, POOL, GOVCERT, and BS-ind constructors, then compare them with updateCertDeposit and updateCertDeposits. Verify the step and CERTS properties under --safe, remove the TODO in Certs.lagda.md, update the Utxo consistency note, and add the requested CHANGELOG entry.

Written by the indexing model from the issue text.