[Dijkstra] LEDGER-pov: complete the proof — gov re-derivation; Certs/Utxo/Utxow facts as parameters (#1223)

Completes the Dijkstra LEDGER preservation-of-value proof.
Ledger/Properties/PoV.lagda.md typechecks end-to-end (Agda 2.8.0 via the Nix
flake, --safe, no postulates/holes).

- Lift the Certs-PoV facts (CERTS-pov, CERTS-coinFromDeposits-updateCertDeposits)
  to module parameters of ENTITIES-PoV and LEDGER-PoV; remove the Certs-PoV
  provider modules.
- Complete the LEDGER-V chain to the four-summand goal getCoin s ≡ getCoin s',
  including the gov-deposit re-derivation: UTXOW-batch-balance-coin (the
  consumedBatch ≡ producedBatch coin projection) carries the produced-side
  govProposalsDeposits as a single trailing totGov, threaded through
  bat'/LHS+E≡RHS+E/step-ii (three-summand); SUBLEDGERS-gov-coin +
  GOVS-coinFromGovDeposit (+ the proposalsOf bridge) +
  rmOrphanDRepVotes-coinFromGovDeposit give gov-acc.
- The Utxo/Utxow-PoV facts remain module parameters, discharged by #1186.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Author: williamdemeo

src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md

@@ -14,6 +14,4 @@ module Ledger.Dijkstra.Specification.Certs.Properties where
 
 ```agda
 open import Ledger.Dijkstra.Specification.Certs.Properties.Computational
-open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas
-open import Ledger.Dijkstra.Specification.Certs.Properties.PoV
 ```