[Dijkstra] LEDGER-pov: complete the proof and address Copilot review comments.

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

- Ledger.lagda.md: HasCoin-CertState counts only the rewards balance
  (getCoin = rewardsBalance ∘ DStateOf), not the deposit pots; correct the
  prose to say components 3 and 4 (coinFromDeposits, coinFromGovDeposit) are
  added at the LedgerState level.
- CHANGELOG.md: the HasCoin-LedgerState entry now also lists the
  coinFromGovDeposit summand, not just the three CertState deposit fields.
- session-start.sh: enabling flakes keyed only on the presence of any
  experimental-features line, so a bare `experimental-features = nix-command`
  would skip flakes. Check for `flakes` specifically and append via
  extra-experimental-features (which doesn't clobber an existing setting).

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

Author: claude

CHANGELOG.md

@@ -15,7 +15,7 @@
   `coinFromDeposits` alone no longer accounts for them.
 - Move cert-deposit helpers from `Utxo` to `Certs`.
 - Fix `updateCertDeposits`: use `foldl` (CERTS is head-first).
-- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, and all three deposit fields.
+- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, the three `CertState` deposit fields (`coinFromDeposits`), and governance-action deposits (`coinFromGovDeposit`).
 - Apply per-transaction direct deposits to `CertState` after each `CERTS` step in `SUBLEDGER-V` and `LEDGER-V` (CIP-159).
 - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises.
 - Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159).

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
 ```