[Dijkstra] UTxO and UTxOW PoV

# Description

**Parent issue**: #1187 (LEDGER PoV)

**Depends on**: #1117, #1120

Prove the `UTXOW`-level value-accounting facts that `LEDGER-pov` (#1187) consumes as module parameters. The central obligations are `UTXOW-V-mechanical` and `UTXOW-batch-balance-coin`; deliberately, **no** `UTXO-pov`/`UTXOW-pov` theorem is requested.

## Why no `UTXO-pov`/`UTXOW-pov` theorem

Conway's `LEDGER-pov` composes per-rule preservation theorems, and its `UTXOpov` is a genuine one: a single `UTXO` step preserves the state's coin up to one correction term,

```
getCoin s + getCoin (wdrlsOf tx) * χ (tx .isValid) ≡ getCoin s'
```

That statement exists because every Conway transaction is individually balanced — `consumed ≡ produced` is a premise of the `UTXO` rule itself — so the only cross-state flow per step is the withdrawals term.

In Dijkstra there is no such per-step theorem to ask for. The only balance premise is *batch-wide* (`consumedBatch ≡ producedBatch`, summing the top-level transaction and all its sub-transactions); individual `SUBUTXO` steps carry no balance premise, and sub-transactions move value between `UTxOState` and `CertState` (withdrawals, cert-deposit refunds/charges, direct deposits, gov deposits) without balancing locally. An honest `UTXOW-pov` would need correction terms amounting to the batch's full deposit/withdrawal ledger — i.e. it would restate the accounting `LEDGER-pov` already does. So `LEDGER-pov` runs a single equational chain at the `LedgerState` level and asks the UTXOW layer for two ingredients instead: *what the step moved*, and *that the batch's moves net out*.

## The two central theorems

**`UTXOW-V-mechanical`** — mechanical bookkeeping for a valid top-level step: given `Γ ⊢ s₀ ⇀⦇ tx ,UTXOW⦈ s₁` with `IsValidFlagOf tx ≡ true` and `TxIdOf tx` fresh for `UTxOOf s₀`,

```
getCoin s₀ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx
≡ getCoin s₁ + cbalance (UTxOOf s₀ ∣ SpendInputsOf tx)
```

It records what the step does to the pots (spend inputs leave; outputs, fees, donations enter) and makes **no conservation claim**; TxId freshness is what lets `outs tx` split off cleanly.

**`UTXOW-batch-balance-coin`** — the coin projection of the rule's own batch-balance premise `consumedBatch ≡ producedBatch`, in closed form (schematically):

```
spendInputs tx + wdrls tx + Σ_stx (spendInputs stx + wdrls stx)
+ refundCertDeposits (allDCerts tx)
≡ outs tx + fees tx + donations tx + directDeposits tx
+ Σ_stx (outs stx + donations stx + directDeposits stx)
+ newCertDeposits pools₀ (allDCerts tx)
+ govProposalsDeposits (top + subs)
```

with spend inputs resolved against the environment's pre-batch UTxO, the pool set for `newCertDeposits` taken pre-batch, and mint terms dropped via `noMintTx`/`noMintSubTx`. This is where conservation lives. Its deposit/withdrawal summands are exactly the terms `LEDGER-pov` cancels against the `CERTS`/`GOVS`/rewards accounting — the cancellation must happen there, since only `LEDGER-pov` sees both sides of each cross-state flow.

## Deliverables

| Lemma | Role in `LEDGER-pov` |
|-------|----------------------|
| `UTXOW-V-mechanical` | valid-path coin tracking (above) |
| `UTXOW-batch-balance-coin` | conservation content (above) |
| `utxow-pov-invalid` | `LEDGER-I` case: an invalid transaction preserves `getCoin` exactly (the one place a local preservation statement *is* true) |
| `subutxow-step-coin` | per-`SUBUTXOW` analogue of the mechanical equation, threaded by `SUBLEDGERS-utxo-coin` |

New modules: `Utxo.Properties.Base` (era-independent helpers: `balance-∪`, `split-balance`, `outs-disjoint`, coin-homomorphism facts), `Utxo.Properties.PoV` (UTXO-level building blocks), `Utxow.Properties.PoV` (the wrappers `LEDGER-pov` invokes, delegating via `UTXOW⇒UTXO`).

## Out of scope

The no-mint facts (`noMintTx`, `noMintSubTx`) and the batch-threading invariants (`fresh-top-tx-id`, `utxo₁-tx-spend-eq`, per-step `SUBUTXOW` freshness/spend-agreement) remain module parameters — follow-up #1274.

## Acceptance criteria

- [ ] The four lemmas typecheck with statements matching the `LEDGER-pov` parameters verbatim.
- [ ] No standalone `UTXO-pov`/`UTXOW-pov` claim.
- [ ] All modules compile with `--safe`.