Cardano Updates

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

Bumps [tar](https://github.com/isaacs/node-tar) from 7.5.13 to 7.5.16.
- [Release notes](https://github.com/isaacs/node-tar/releases)
- [Changelog](https://github.com/isaacs/node-tar/blob/main/CHANGELOG.md)
- [Commits](https://github.com/isaacs/node-tar/compare/v7.5.13...v7.5.16)

---
updated-dependencies:
- dependency-name: tar
  dependency-version: 7.5.16
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <[email protected]>

Fix Moog CLI download for new asset naming

Koz/999

Per the top-down LEDGER-pov strategy (#1203), the Certs-PoV facts become
module-parameter stubs, discharged later by #1210, so this PR proves only
the ENTITIES/LEDGER layer.

- Delete the provider modules Certs/Properties/PoV.lagda.md and
  Certs/Properties/PoVLemmas.lagda.md.
- Drop their imports from Certs/Properties.lagda.md (keep Computational).
- Add CERTS-pov as a parameter of the ENTITIES-PoV module in
  Entities/Properties/PoV.lagda.md, replacing the deleted import.

Certs.Properties and Entities.Properties.PoV typecheck under Agda 2.8.0 via
the project Nix flake.

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

Replace the Blockfrost-raw and cardano-wallet detection tabs with Evolution and Mesh provider tabs (keeping cardano-cli), so the page uses the same SDK tabs as the rest of the curriculum and its own send section. Detection polls the address UTXOs via each SDK's provider and sums lovelace.

Standardize closing-section headings to Next steps and Key takeaways, fix the Module 6 overview title (was DeFi and Integrations for the Build a dApp module), add the missing id to the optimization page, clarify two sidebar labels, and convert all em and en dashes to ASCII across the curriculum.

The File Hygiene workflow (reusable lint-files.yml from
hyperledger-identus/.github) runs markdownlint-cli2 over **/*.md.
The repo config (.markdownlint-cli2.yaml) ignored only the root
CHANGELOG.md, but per-package CHANGELOGs (packages/**/CHANGELOG.md)
are auto-generated by `nx release` and written without a trailing
newline, violating MD047/single-trailing-newline.

This made the lint / Markdown job fail on every PR after each release
that rewrote the per-package changelogs (e.g. Dependabot PR #661).

Fix: change the ignore from "CHANGELOG.md" to "**/CHANGELOG.md" so all
generated changelogs (root + per-package) are exempt, consistent with
how the root changelog was already handled.

Verified locally: markdownlint-cli2 '**/*.md' -> 0 error(s).

Signed-off-by: Pat Losoponkul <[email protected]>