[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`. + Clean up redundant code.