[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.

Author: williamdemeo

CHANGELOG.md

@@ -6,7 +6,7 @@
 
 - Apply batch-wide direct deposits to `CertState` in `LEDGER-V` output (CIP-159).
 - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises.
-- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159).
+- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` (CIP-159).
 - Extend `TxInfo` with `txDirectDeposits` and `txBalanceIntervals` fields (CIP-159).
 - Remove `allBalanceIntervals` batch-level aggregation helper; balance interval
   assertions will be checked per-(sub)transaction in `UTXO`/`SUBUTXO` rules (see #1117).