[Dijkstra] Discharge the no-truncation withdrawal bounds (ENTITIES/SUBENTITIES-wdrls-bounded)

# Description

**Parent issue**: #1123 (umbrella). **Context**: PR #1203 (`LEDGER-pov`, #1187); the gap was flagged in the review of PR #1256.

`applyWithdrawals` subtracts with truncated subtraction (`_∸_`), so the `ENTITIES`/`SUBENTITIES` value-flow equations (`ENTITIES-pov`, `SUBENTITIES-pov`, PR #1203) need each withdrawal amount to be bounded by the account's balance in the **input state of the step that consumes it** — otherwise a withdrawal silently truncates and value is not preserved. `LEDGER-pov` takes these bounds as the module parameters `ENTITIES-wdrls-bounded` / `SUBENTITIES-wdrls-bounded` (`src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md`, provenance comments inline).

## The gap

The spec's premises bound withdrawals only against the *pre-batch* snapshot `rewards₀` (except top-level legacy mode, which forces exact-balance withdrawals). That does not bound them against the input state of a *later* step in the batch: earlier steps in the same batch may already have withdrawn from the same account, so a later withdrawal can exceed the remaining balance while still passing the `rewards₀` check — the phantom-withdrawal scenario. Cf. the [partial-withdrawals discussion in CIP-0159](https://github.com/cardano-foundation/CIPs/tree/master/CIP-0159#partial-withdrawals-and-native-asset-withdrawals) and item 3 of #1257 ("aggregated withdrawals must not exceed the pre-transaction account balance").

## To do

Decide and implement one of:

1. a **spec-side premise** strengthening the per-step withdrawal check (bound against the running rewards state), or
2. a **batch-threading invariant** showing that the batch's *aggregate* withdrawals per account are bounded by `rewards₀` — the CIP's stated intent — and that this implies the per-step input-state bound.

Then discharge the two module parameters and delete them from `LEDGER-PoV`.

Read src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md and trace the ENTITIES-wdrls-bounded and SUBENTITIES-wdrls-bounded parameters through the withdrawal premises and running state. Choose either the per-step premise or the batch-threading invariant, prove the bounds, discharge both parameters, and remove them from LEDGER-PoV.

Written by the indexing model from the issue text.