Cardano Updates

State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.

There were unresolved proof obligations from Conway.

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

Add preservation-of-value property modules for the Dijkstra era,
adapted from the Conway PoV proof structure for CIP-159 (partial
withdrawals and direct deposits).

New modules:
- Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov,
  PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics)
- Certs.Properties.PoV: CERTS-pov top-level theorem
- Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing
  applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls
- Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement
  with proof sketch for direct deposit cancellation

Design notes:
- PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction)
  instead of Conway's constMap/res-decomp/sumConstZero chain
- LEDGER-pov identifies the applyDirectDeposits cancellation as the
  main new proof obligation vs Conway
- applyWithdrawals-pov is structured as three layers: single-step
  (applyOne-pov), fold induction (foldl-applyOne-pov), top-level

Status: Skeleton with holes; does not yet fully typecheck.

Add the applyWithdrawals preservation-of-value proof machinery and
prove several lemmas that were previously assumed as module parameters
in Conway.

New proofs in Ledger.Prelude (previously Conway module parameters):
- indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ
- sumConstZero: getCoin (constMap X 0) ≡ 0
- getCoin-cong: indexedSum' proj₂ respects set equality
- res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ))
- getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom,
  ∪ˡsingleton0≡: singleton map getCoin lemmas
- indexedSumL-proj₂-zero: sum of zero-valued entries is zero
- setToList-∈: opaque bridge from list membership to set membership

New module Certs.Properties.ApplyWithdrawalsPoV:
- applyOne-pov: single withdrawal step decreases getCoin by amt
- foldl-applyOne-pov: fold induction with Unique invariant
- applyWithdrawals-pov: top-level lemma for PRE-CERT-pov
- ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves
  domain membership for other credentials

Remaining assumptions (deferred to agda-sets library):
- ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys
- sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ'
- setToList-Unique: credential uniqueness of withdrawal list
- ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

Introduce three new modules implementing the UTXO-level building blocks
of the Dijkstra-era preservation-of-value proof (towards closing #1123 /
CIP-159-11):

+  `Utxo/Properties/Base.lagda.md`
   Era-independent helper lemmas: `∙-homo-Coin`, `newTxid⇒disj`,
   `outs-disjoint`.  Intentionally minimal for now — the Conway Base
   proofs of `balance-cong`, `balance-∪`, and `split-balance` do not
   port verbatim because Dijkstra defines `balance` as `∑ˢ` over a set
   of Values rather than as `indexedSumᵐ` over a map of hashed TxOuts.
   Tracking issue filed for the proper port.

+  `Utxo/Properties/PoV.lagda.md`
   The Dijkstra UTXO preservation-of-value proof is split into two
   orthogonal pieces:

   -  Mechanical state change (`UTXO-I-getCoin`, `UTXO-V-mechanical`):
      relates `getCoin s₀` to `getCoin s₁` from the UTxOState transition
      alone, using `split-balance` and `balance-∪`.  Proved.

   -  Batch coin balance (`batch-balance-coin`): the coin projection of
      the `consumedBatch ≡ producedBatch` premise (premise p₇ of the
      UTXO rule).  Proved from the two module parameters
      `coin-of-consumedBatch` and `coin-of-producedBatch`, which are
      themselves left as assumptions for now (see PoV follow-up work).

   The combined `UTXO-pov` theorem is stated but left as a placeholder
   (`?`); its exact form depends on how `LEDGER-pov`'s
   `BatchUtxoAccounting` consumer threads sub-transaction state.

+  `Utxow/Properties/PoV.lagda.md`
   UTXOW-level wrappers that extract the UTXO derivation from either
   `UTXOW-normal` or `UTXOW-legacy` (via a shared `UTXOW⇒UTXO`
   extractor) and delegate to the UTXO-level lemmas.  Provides
   `utxow-pov-invalid` in the exact shape required as a module
   parameter by `Ledger/Properties/PoV.lagda.md`.

Proof-internal notes:

+  `balance-∪` and `split-balance` are currently module parameters
   to `Utxo/Properties/PoV` pending the port of Conway Base's balance
   arithmetic to Dijkstra (see tracking issue).

+  The 7-term +-commutative-monoid shuffle in `UTXO-V-mechanical` is
   proved by hand using a `swap-right` helper; this could later be
   replaced by a call to a commutative-monoid solver.

+  All three modules typecheck under `--safe`.

Complete the LEDGER preservation-of-value proof structure for Dijkstra.

- LEDGER-I: Fully proved via utxow-pov-invalid.
- LEDGER-V: Complete equational chain with no holes or unresolved metas.
  Decomposes into:
  - step-i: combined CERTS accounting (sub + top level)
  - arithmetic-1, arithmetic-2: ℕ rearrangements
  - step-iii-iv: batch UTxO + deposit accounting (assumption)
  - step-ii: applyDirectDeposits cancellation (assumption)

New sub-lemma proved:
- SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing
  rewardsBalance decreases by exactly the sum of sub-withdrawal amounts.
  Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and
  SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from
  SUBUTXOW → SUBUTXO premises).

Remaining assumptions (module parameters):
- batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection
  combined with mechanical UTxO tracking and deposit accounting
- applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin)
- utxow-pov-invalid: collateral collection preserves getCoin utxoSt
- ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique

State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.