Cardano Updates

Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is
independent of the Dijkstra PoV proof and belongs in its own PR.

- Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`,
  `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`,
  `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`,
  `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module.
- Drop the now-provable assumption parameters from the Conway PoV proofs, using the
  Prelude lemmas instead:
  - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`.
  - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton`
    helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`.
  - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`.
  - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter.
  - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`.

No spec-semantic change (proof refactor only), so no CHANGELOG entry.

`Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files
are their 1187 versions (which typecheck) and depend only on the hoisted lemmas.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

The closed-form cert-deposit helpers were hoisted to `Certs` for downstream
Certs-level PoV proofs; the comment named the now-removed `Certs.Properties.PoVLemmas`
module.  Generalize the wording (prose only; no Agda change).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Applies the unambiguous, additive corrections to the (non-build-path) LEDGER-pov
draft.  The deep batch-balance arithmetic is deliberately deferred: it depends on
the Utxo/Utxow-PoV interface that lives in #1189, not on this branch.

- Give LEDGER-PoV a CERTS-pov parameter (Certs-PoV stub, #1210) threaded into the
  ENTITIES-PoV instantiation, and a CERTS-coinFromDeposits-updateCertDeposits
  parameter (closed-form cert-deposit coin equation, #1210).
- Add the governance-deposit parameters rmOrphanDRepVotes-coinFromGovDeposit and
  GOVS-coinFromGovDeposit (per the resume note), with a generic proposalsOf helper.
- Rename coinFromDeposit -> coinFromDeposits (the spec renamed it).
- Thread the coinFromGovDeposit summand into the LedgerState totals: the LEDGER-I
  case and the LEDGER-V G0/G' where-definitions.
- Update the status note to record what is done and the precise deferred work
  (calculateDepositsChange/DepositsChange/UTXOW-* interface + the gov-deposit
  re-derivation: a SUBLEDGERS-gov-coin induction and a restated batch balance).

Verified scope-clean up to the deferred chain: Agda elaborates proposalsOf, all
module parameters, and the ENTITIES-PoV instantiation, stopping only at the
documented not-on-branch interface (calculateDepositsChange).  The file is an
intentional WIP draft and is not on the build path.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Co-authored-by: Copilot Autofix powered by AI <[email protected]>