Cardano Updates

After moving direct-deposit application from LEDGER-V into POST-CERT,
CERTS-pov now produces a symmetric "consumed = produced" equation:

  getCoin s₁ + getCoin (DirectDepositsOf Γ)
  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Thread the direct-deposit term through the LEDGER-pov proof:

* SUBLEDGERS-certs-pov gains "+ sum (map ddwl stxs)" on the LHS,
  where ddwl = getCoin ∘ DirectDepositsOf is the per-sub-tx
  direct-deposit total (analogous to wdrwl).

* combined-certs gains "+ allDirectDeps" on the LHS, composing the
  per-sub CERTS-pov chain with the top-level call.

* The main LEDGER-V chain wraps the result in +-cancelʳ-≡ to
  discharge the asymmetric "+ allDirectDeps" combined-certs introduces.

Removed:

* The certStateFinal local definition (LEDGER-V no longer applies
  applyDirectDeposits).
* step-ii and the applyDirectDeposits-rewardsBalance module parameter
  (subsumed by indexedSumᵛ'-∪⁺ inside POST-CERT-pov).
* The DD-split module parameter (subsumed by per-tx CERTS-pov chain).
* Stale "Key Lemma" subsection and stale commented-out lines in bat'.
* Unused imports +-identityʳ and +-0-monoid.
* Redundant local aliases in bat's where-block.

Documentation: rewrote "Key Differences from Conway" point 2 and the
LEDGER-V Proof Outline to reflect the new architecture; clarified the
LEDGER-I outline.

After moving direct-deposit application from LEDGER-V into POST-CERT,
CERTS-pov now produces a symmetric "consumed = produced" equation:

  getCoin s₁ + getCoin (DirectDepositsOf Γ)
  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Thread the direct-deposit term through the LEDGER-pov proof:

* SUBLEDGERS-certs-pov gains "+ sum (map ddwl stxs)" on the LHS,
  where ddwl = getCoin ∘ DirectDepositsOf is the per-sub-tx
  direct-deposit total (analogous to wdrwl).

* combined-certs gains "+ allDirectDeps" on the LHS, composing the
  per-sub CERTS-pov chain with the top-level call.

* The main LEDGER-V chain wraps the result in +-cancelʳ-≡ to
  discharge the asymmetric "+ allDirectDeps" combined-certs introduces.

Removed:

* The certStateFinal local definition (LEDGER-V no longer applies
  applyDirectDeposits).
* step-ii and the applyDirectDeposits-rewardsBalance module parameter
  (subsumed by indexedSumᵛ'-∪⁺ inside POST-CERT-pov).
* The DD-split module parameter (subsumed by per-tx CERTS-pov chain).
* Stale "Key Lemma" subsection and stale commented-out lines in bat'.
* Unused imports +-identityʳ and +-0-monoid.
* Redundant local aliases in bat's where-block.

Documentation: rewrote "Key Differences from Conway" point 2 and the
LEDGER-V Proof Outline to reflect the new architecture; clarified the
LEDGER-I outline.