[LLF1-2] Leios voting crypto: port the abstract-interface polish onto the core BLS primitives

**Re-scoped 2026-08-31**.

The fork trial's `LeiosAbstract` record (williamdemeo/formal-ledger-specifications#16) is superseded by the BLS primitives #1300 adds to `Ledger.Core.Specification.Crypto` (`BlsVKey`, `BlsSig`, `BlsPoP`, `isValidPoP`, `isSignedByAggregate` over `Ser`, the key-hash order `_<ᵏʰ_`, and the `BlsKeyMaxAgeᶜ` genesis constant).

Core placement was this plan's follow-up destination anyway, and it dissolves the `GovStructure` threading together with the naming concern raised against it.

What remains is the port of the interface polish:

- [ ] Single-vote verification: `isSignedBy` for one BLS key over `Ser` (the message is the announcing RB header hash), with a decidability instance; `validateVote`'s ledger half needs it, and `isSignedByAggregate` does not subsume it.
- [ ] Confirm decidability and `DecEq` coverage on all new crypto fields, and the no-signing-side discipline (only verification enters the rules), recorded in module prose.
- [ ] Module prose: the BLS12-381 MinSig instantiation (96-byte keys, 48-byte signatures and proofs of possession), the rogue-key rationale for the mandatory proof of possession, and the Peras-sharing intent of the core placement.
- [ ] Retire the fork module: close williamdemeo/formal-ledger-specifications#16 with a pointer here; `EBHash`, `TxRefHash`, and `hashEBRefs` move to [LLF1-3].

These items can be done either as review suggestions on #1300 or as a small PR on top of it.

Subissue of #1295.

Review the BLS primitives added by #1300 in Ledger.Core.Specification.Crypto and compare them with the four remaining checklist items. Confirm single-vote verification, decidability and DecEq coverage, and the requested module prose; then handle retirement of williamdemeo/formal-ledger-specifications#16 while leaving EBHash, TxRefHash, and hashEBRefs for LLF1-3.

Written by the indexing model from the issue text.