Cardano Updates

The proof is complete, so the three historical "deferred/WIP/does-not-typecheck"
status notes are replaced by one accurate note describing the module parameters
(discharged downstream) and the four-summand accounting.  Also refreshes the
GOVS-coinFromGovDeposit and G₀/G' comments, the arithmetic-helpers prose, and
removes the now-unused abcd-to-adcb shuffle.  No proof changes (still --safe, EXIT 0).

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

The Dijkstra LEDGER preservation-of-value proof now typechecks end-to-end
(nix develop --command agda, --safe, no postulates/holes).

The LEDGER-V chain now proves the full 4-summand goal
  getCoin s ≡ getCoin s'  =  U₀+R₀+D₀+G₀ ≡ U₂+R₂+D₂+G'
where G' = coinFromGovDeposit (rmOrphanDRepVotes cs₂ govSt₂), by:

- Restating UTXOW-batch-balance-coin (the consumedBatch ≡ producedBatch coin
  projection, #1186's obligation) with the produced-side govProposalsDeposits
  collected into a single trailing `totGov` term.
- Threading +totGov through bat' → LHS+E≡RHS+E → step-ii (mid-extract pulls it
  out of the middle; the existing arithmetic runs under cong (_+ totGov)),
  yielding three-summand : U₀+R₀+D₀ ≡ U₂+R₂+D₂+totGov.
- gov-acc : totGov + G₀ ≡ G', via SUBLEDGERS-gov-coin (sub-tx GOVS steps),
  GOVS-coinFromGovDeposit (top GOVS step) + the proposalsOf bridge, and
  rmOrphanDRepVotes-coinFromGovDeposit.
- Assembling the 4-summand goal from three-summand + gov-acc.

The UTXOW-PoV facts (utxow-pov-invalid, UTXOW-V-mechanical,
UTXOW-batch-balance-coin) remain module parameters, discharged downstream by
the utxo/utxow-pov work (#1186).

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

UI surface for the property tracker (catalog stays the source of truth):

- mkdocs: scan_properties.py now writes a second, byte-identical copy of the
  roadmap to build-tools/static/mkdocs/docs/ledger-properties-roadmap.md, added
  to the nav as the "Properties Roadmap" page. `--check` regenerates and verifies
  BOTH copies, so the site roadmap cannot drift from the canonical one. Validated
  with `mkdocs build -s` (strict): the page renders with no warnings.
- README: add CI and properties-check workflow badges alongside the existing
  nightly/license badges.
- ADR: document the dashboard (mkdocs page, badges) and how to stand up the
  optional read-only GitHub Projects v2 board (Era/STS/Status) by hand.

(The properties-check.yml trigger is extended to the site copy in a follow-up
commit via the API — git here lacks the `workflow` OAuth scope.)

Part of #1225.

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

Seeded the missing tracking issues from the catalog (Conway era + a Dijkstra
umbrella; the speculative Dijkstra port issues are deferred until that work
starts):

- Dijkstra umbrella #1227 (counterpart of the Conway umbrella #45).
- 14 Conway issues (#1228–#1241) for the proved/stated properties that had no
  tracking issue (the PoV theorems, the three govDepsMatch invariants, MinSpend,
  ConstRwds, CredDepsEqualDomRwds, PParamsWellFormed, NoPropSameDReps,
  VoteDelegsVDeleg, ChangePPGroup, ExpiredDReps).

Wrote the new numbers back into `properties.yaml` and regenerated the roadmap.
All Conway entries are now tracked; the 15 still-untracked entries are exactly
the deferred Dijkstra ports (status idea).

Also fix a `set_issue_numbers`/`set_umbrella` regex bug where the trailing group
captured the line's newline, inserting a spurious blank line after each edited
`issues:` line.

Part of #1225. Reconciliation tracked under #45.

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

Status is now computed entirely from the Agda, never declared in the catalog:
no module -> idea; module file absent -> planned; `coming soon` present ->
stated; otherwise -> proved. `properties.yaml` no longer carries a `status:`
field.

Because status is computed, the anti-drift gate is the generated roadmap
itself: `scan_properties.py --check` regenerates the dashboard and fails if the
committed copy is stale, so a proof landing (the marker disappearing) without a
roadmap refresh is a CI failure — the same #413/#414 guarantee, with no second
place for the status to drift.

- scan_properties.py: 4-way derivation; drop the declared-vs-derived reconcile;
  counts/badges key off the derived status; error if a stray `status:` remains.
- properties.yaml: drop all 34 `status:` fields; document the derivation.
- gh_project_populate.py, gh_project_render.py: derive status via
  scan_properties.derive_status instead of the removed field.
- 0001-ledger-property-tracking.md, README.md: document the derived model.
- ledger-properties-roadmap.md: regenerated — status values unchanged (the
  derivation reproduces exactly the previously hand-set values).

Part of #1225.

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

Foundational gov-deposit lemma (verified to typecheck): induct over SUBLEDGERS,
threading the per-GOVS gov-deposit growth via the GOVS-coinFromGovDeposit
parameter, to get

  coinFromGovDeposit (GovStateOf s₁)
    ≡ coinFromGovDeposit (GovStateOf s₀)
      + Σ_subs govProposalsDeposits pp (ListOfGovProposalsOf stx).

Also adds proposalsOf-Proposals+Votes : proposalsOf (GovProposals+Votes t) ≡
ListOfGovProposalsOf t (polymorphic helper, avoids the GovVote/GovProposal
double-import ambiguity), bridging the GOVS step's proposals to the batch
balance's ListOfGovProposalsOf.

Remaining: gov-inclusive UTXOW-batch-balance-coin + thread +totGov through
bat'/the chain, the gov-deposit accounting (G' ≡ G₀ + totGov), and the
4-summand assembly.

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

Follow-up to "update link": the index entry rendered as malformed markdown
(`[Gov-LastVoteApplied]][]`` `) and the link target pointed at the module page
rather than the claim. Make it a clean reference (`[Gov-LastVoteApplied][]`)
and point the link at the `#clm:LastVoteApplied` anchor, matching the sibling
`[Gov-ChangePPHasGroup]`. Also add the `[Gov.Properties.LastVoteApplied]`
module link for completeness.

Part of #417 (statement only; proof to follow).

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

The EventuallyRefunded statement stub typechecks under Agda 2.8.0 as-is
(no proof yet). Two refinements:

- Use the `*Proof*. (coming soon)` pending marker (was `(TODO)`), matching
  the convention the property-tracking scanner keys on, so the claim is read
  as `stated` (proof pending) rather than being mistaken for proved.
- Fix the roadmap entry in the Conway properties index: add the
  `[CHAIN-EventuallyRefunded]` / `[Chain.Properties.EventuallyRefunded]`
  link definitions and render the claim as a list item, matching siblings.

Part of #414 (statement only; proof to follow).

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

Checkpoint: the full LEDGER-V chain now typechecks up to the final clause, which
fails (as expected) because the existing 3-summand chain proves U₀+R₀+D₀ ≡
U₂+R₂+D₂ while the goal getCoin s ≡ getCoin s' carries the gov summand
G' = coinFromGovDeposit (rmOrphanDRepVotes cs₂ govSt₂).

Fixes in this commit:
- UTXOW-batch-balance-coin parameter (no-gov form for now), inlined ⊖ so it
  reduces to the chain's DepositsChangeTopOf/SubOf form.
- posPart-negPart-sym inductive clause via [1+m]⊖[1+n]≡m⊖n (⊖ does not reduce
  suc/suc definitionally).
- LEDGER-V pattern: correct implicit names in telescope order
  (utxoState₁, govState₁, certState₁, certState₂, govState₂, utxoState₂) and
  bind the top-level GOVS step (was discarded).
- extract-utxo-netId: UTXOW-normal-⋯/legacy-⋯ need 13 leading args + the UTXO
  premise (was 11).

Remaining: add govProposalsDeposits to UTXOW-batch-balance-coin's produced side,
thread +totGov through bat'/the chain, add SUBLEDGERS-gov-coin + the gov-deposit
accounting, and assemble the 4-summand goal.

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

- scan_properties.py: derive each property's status from the Agda (the
  'coming soon' marker = proof pending), reconcile against the catalog, and
  regenerate the roadmap; --check is the no-network CI drift gate.
- gh_project_populate.py: seed labels, per-era umbrella issues, and one issue
  per catalog entry, writing issue numbers back into the catalog
  (comment-preserving). Adapted from the agda-algebras populate script.
- gh_project_render.py: pull live issue state into a coordination view.
- README.md: usage.

Introduce a single, version-controlled source of truth for tracking ledger
properties across the Conway and Dijkstra eras:

- docs/notes/0001-ledger-property-tracking.md: ADR describing the three-layer
  model (Agda = truth for proof status; catalog = inventory; issues =
  coordination), conventions, and the initial issue-reconciliation plan
  (incl. the #413-vs-#414 correction).
- docs/notes/properties.yaml: curated catalog of every tracked property
  (id, era, STS, Agda module, tracking issue, intended status).
- docs/notes/ledger-properties-roadmap.md: generated dashboard.

Runs scan_properties.py --check on PRs touching the catalog, roadmap, scanner,
or any property module. No network/Nix needed; complements the Agda --safe
typecheck in ci.yml.

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

Two of the three Utxo/Utxow-PoV facts as #1186 module-parameter stubs, verified
to typecheck (the checker now advances to UTXOW-batch-balance-coin):

- utxow-pov-invalid: an invalid top-level tx's UTXOW step preserves UTxO coin.
- UTXOW-V-mechanical: the valid single-tx mechanical coin equation.

Remaining: UTXOW-batch-balance-coin (the consumedBatch ≡ producedBatch coin
projection, with govProposalsDeposits on produced) and the gov-summand
re-derivation through bat'/the main chain.

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