[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s',
where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three
cert-deposit pots, and the gov-action deposits.  Typechecks under --safe
with no postulates or holes.

Top-down plan: the supporting Certs / UTxO / Gov facts are module
parameters of `Ledger.Properties.PoV`, forming the frozen contract for the
follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV).

New modules:
- Ledger/Properties/PoV: LEDGER-pov.  The LEDGER-V case is a single
  LedgerState-level equational chain; direct-deposit value cancels between
  the UTxO and CertState sides, gov-deposit growth is matched against the
  produced-side govProposalsDeposits, and `bat'` converts the closed-form
  batch balance (#1186 shape) to the chain's two-level posPart/negPart
  deposit form via the batch-cert-deposits-bridge (#1210 shape) and
  net-arith.
- Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the
  value-flow equations for the post-#1256 tx-signal rules.  NetworkId and
  domain facts come from the rules' own premises; the no-truncation bound
  (withdrawal amount ≤ input-state balance) is an explicit hypothesis —
  the phantom-withdrawal gap flagged in the #1256 review, provided at the
  LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters.
- Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and
  applyDirectDeposits-pov fold lemmas.

Spec changes:
- Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand
  (gov-action deposits live in GovActionState.deposit, not
  GState.deposits, yet the UTXO batch balance charges
  govProposalsDeposits on the produced side).
- Certs: getCoin (CertState) is now total (rewards + deposit pots), with
  coinFromRewards / coinFromDeposits projections.
- Prelude: era-independent sum lemmas (+-interleave, sum-map-+).

Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased
onto master and adapted to #1250 (explicit cert deposits, closed-form
newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv,
SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and
deposit sign-swap fix in #1250, so it is no longer part of the diff.

AI-assisted: Claude Fable 5 (Anthropic)

Author: williamdemeo

src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md

@@ -181,10 +181,12 @@ conditions) are premises of the rule itself.
     aw = applyWithdrawals (WithdrawalsOf txSub) r₀
 ```
 
-The top-level analogue, with signal `txTop`{.AgdaBound}, by the same argument.  (In
-legacy mode the rule's own premise forces each top-level withdrawal to equal the
-account's current balance, which implies the `amts≤`{.AgdaBound} hypothesis; in
-normal mode the rule bounds withdrawals only against the pre-batch
+## The `ENTITIES-pov` theorem
+
+The top-level analogue, with signal `txTop`{.AgdaBound}, follows
+by the same argument.  (In legacy mode the rule's own premise forces each top-level
+withdrawal to equal the account's current balance, which implies the `amts≤`{.AgdaBound}
+hypothesis; in normal mode the rule bounds withdrawals only against the pre-batch
 `rewards₀`{.AgdaField}, so the hypothesis is genuinely extra information.)
 
 ```agda
@@ -194,7 +196,11 @@ normal mode the rule bounds withdrawals only against the pre-batch
     → Γ ⊢ s ⇀⦇ txTop ,ENTITIES⦈ s'
     → coinFromRewards s  + getCoin (DirectDepositsOf txTop)
       ≡ coinFromRewards s' + getCoin (WithdrawalsOf txTop)
+```
 
+**Proof**.
+
+```agda
   ENTITIES-pov {txTop = txTop} {s = ⟦ ⟦ _ , _ , r₀ , _ ⟧ᵈ , _ , _ ⟧ᶜˢ}
     amts≤
     (ENTITIES {rewards' = r₁} (wd-netId , wdrls⊆ , _ , _ , _ , _ , certsStep , _ , ddCreds⊆)) =