[Conway] Derive the EventuallyRefunded refund-deadline invariant from the CHAIN rule

## Description

PR #1217 (see #414) proves `gaDepositsEventuallyRefunded` in `Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded`: once the chain has progressed two epochs past a governance action's `expiresIn`, the action's deposit is no longer in the deposit pot.

The theorem takes as a premise a per-state invariant, imposed (via `RTC-All`) at every state reached along the `CHAINS` trace:

```agda
InvariantAt gaid gaSt cs = (¬ gaDepositInPot cs gaid)
⊎ (LastEpochOf cs ≤ sucᵉ (expiresIn gaSt))
```

i.e. at every visited state, either the deposit has already been refunded, or the refund deadline (one epoch past `expiresIn`, owing to the two-epoch `RATIFY`/`GovernanceUpdate` pipeline) has not yet passed.

This invariant holds at every *reachable* chain state, but it is currently an assumption. This issue tracks discharging it: proving that the theorem's preconditions at the initial state imply `RTC-All (InvariantAt gaid gaSt) chain` for every `CHAINS` derivation `chain` from that state.

### What the derivation needs

1. **`govDepsMatch` propagation along the trace** — the `rrm` premise of `CHAIN-govDepsMatch` must be available at each step.

2. **Tracking the action through `LEDGERS` and the `RATIFIES` pipeline** — while live, `LEDGER` steps preserve the action's `GovState` entry and deposit; at epoch `sucᵉ (expiresIn)`, `RATIFIES` places the expired action in `removed`; at the following boundary, `GovernanceUpdate` filters it out and strips the deposit.
3. **A `TxId`-freshness assumption** — after the refund, the deposit must not reappear. A `GovActionID` contains the proposing transaction's `TxId`, which in reality is a cryptographic hash and never reused, but the specification does not enforce `TxId` freshness syntactically, so "stays gone" needs an abstract freshness hypothesis.

4. **An `EpochStructure` axiom that `sucᵉ` is least** — `e < e' → sucᵉ e ≤ e'` is needed for the epoch-boundary bookkeeping; it holds for the ℕ instance but is not derivable from the current `EpochStructure` axioms. (Could be split into its own small issue, since it is independently useful.)

---

### Partial machinery already developed

Much of items 2--4 was proved on the #1217 branch and removed in the simplification commit 7671dafbf.

Starting points, on the PR branch:

+ ef3875101 `FreshId` hypothesis; `govDepsMatch` bridges (`gdm-dep⇒dpMap`, `gdm-¬dpMap⇒¬dep`);
+ 74a63537a two-epoch pipeline analysis; `RATIFY` lemmas;
+ 8359a41b5 `SucIsLeast`; `govUpdate-removes`; `ratifies-expired∈⇒in-removed`, `ratify/ratifies-removed-mono`;
+ e6781d97d deposit-absence through `updateDeposits` (`updCertDeps-GA-absent`, `updPropDeps-GA-absent`, `updateDeposits-GA-absent`, `GovActionDeposit-inj`)
+ 32d444462 the "stays gone" chain: `EPOCH-GA-absent`, `LEDGER(S)-GA-absent`, `CHAIN-GA-absent`, `CHAINStar-GA-absent`

Start at Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded and the gaDepositsEventuallyRefunded preconditions, then trace the CHAINS derivation through CHAIN-govDepsMatch, LEDGERS, RATIFIES, and GovernanceUpdate. Review the partial machinery from commits ef3875101, 74a63537a, 8359a41b5, e6781d97d, and 32d444462; done means proving RTC-All (InvariantAt gaid gaSt) from the initial assumptions with freshness and the sucᵉ leastness axiom.

Written by the indexing model from the issue text.