Bridge CERTS evolution to closed-form cert-deposit accounting
Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list. This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.
New proofs (PR branch):
+ `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`. Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.
+ `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`. RTC induction mirroring `CERTS-pov`. Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.
+ `CERTS-coinFromDeposits-updateCertDeposits`. Coin projection of the main lemma, immediately usable by `LEDGER-pov`.
Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.
Master-touching changes
+ **Bug fix in `updateCertDeposits`**. Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`. The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.
+ **Bug fix in `updateCertDeposits`**. Was using `foldr`, processing certs right-to-left. The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition). For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`. Switched to `foldl`. Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.
+ **Refactor**. Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.
+ **Hoist**. Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`. These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`. `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).
PR-branch-only changes:
+ `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural). `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`. Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.
![dependabot[bot]](https://avatars.githubusercontent.com/in/29110?v=4&s=80)
