[Leios] tracking issue

## Leios and the ledger

Ouroboros Leios ([CIP-164](https://cips.cardano.org/cip/CIP-0164), "Linear Leios") raises throughput by letting each block producer announce an *endorser block* (EB) of transaction references alongside its ranking block. A per-epoch committee of stake pools (stake-based truncation of the stake distribution) votes on the EB; a quorum of votes is aggregated into a certificate; and the immediately following ranking block may carry that certificate, at which point the EB's transactions enter the ledger.

For the ledger this means the following:

+ new block fields (announcement, certificate);
+ new protocol parameters;
+ a BLS voting key with proof of possession in pool registration;
+ an epoch committee derived from the stake distribution;
+ validity predicates for votes and certificates;
+ rules for applying a certified EB's transactions.

Today all of this is enforced by convention in the consensus prototype, while [cardano-ledger#5626](https://github.com/IntersectMBO/cardano-ledger/pull/5626 ) carries data only.

The **Leios Ledger Formalization (LLF)** makes it ledger law, in Agda, on the `leios-main` branch, before/as the implementation migrates it.

## Plan

The design decisions are recorded in the design note (#1297, `docs/leios/design-note.md`). A six-week core plan (three milestones, fourteen issues) targets a coherent, type-checking formalization; the detailed roadmap with dependency graphs lives in [GITHUB_PROJECT_6WEEK.md](https://github.com/williamdemeo/formal-ledger-specifications/blob/1-leios-tracking-issue/docs/GITHUB_PROJECT_6WEEK.md):

1. **Foundations** (weeks 1–2): the design note; abstract voting-crypto interface; EB, vote, and certificate types; protocol parameters (`τ < σ_c` turned out to be a property of the stake distribution, not of the parameters; the lower bound `½ < τ` is a follow-up, below); voting key and proof of possession in pool registration.
2. **Validity** (weeks 3–4): the committee and its quorum arithmetic (order pinned as a law: descending stake, ties by pool id); vote validity; certificate validity; `ValidEB`, the property a certificate certifies.
3. **Integration** (weeks 5–6): block-structure fields; the BBODY certificate check and certified-EB application via `LEDGERS`; CHAIN threading (pending announcement, timing window, epoch pin); a pinned cross-check against the protocol-level Agda spec; a worked example.

Deferred follow-up: metatheory (certified-application soundness, preservation of value, no double application), `Computational` instances, conformance and extraction, the incremental voting-state interface, and feature gating. The roadmap, kept current as PRs merge, is [docs/leios/roadmap.md](https://github.com/IntersectMBO/formal-ledger-specifications/blob/1296-llf-design-note/docs/leios/roadmap.md) (on `leios-main` once #1297 merges).

## Process

Work is trialed in [William's fork](https://github.com/williamdemeo/formal-ledger-specifications) (per-issue draft PRs, CI, review) and migrates here one issue at a time, as sub-issues of this issue with `[LLFN-k]` ids; each upstream PR carries its branch's full history. First pair: #1296, delivered by #1297. Process details: [LEIOS_FORK_WORKFLOW.md](https://github.com/williamdemeo/formal-ledger-specifications/blob/1-leios-tracking-issue/docs/LEIOS_FORK_WORKFLOW.md).

References: [CIP-164](https://cips.cardano.org/cip/CIP-0164); [cardano-ledger# 5626](https://github.com/IntersectMBO/cardano-ledger/pull/5626), [cardano-ledg er#5965](https://github.com/IntersectMBO/cardano-ledger/issues/5965); the Leios design document (`ouroboros-leios`, `docs/leios-design`); the protocol-level Agda spec ([ouroboros-leios-formal-spec](https://github.com/input-output-hk/ouroboros-leios-formal-spec)).

## Follow-ups

- [ ] The quorum threshold's normative lower bound as a conditional well-formedness premise, `τ ≡ 0` or `½ < τ` (zero is the disabled state), after #1317 (its review, note 2).

Start with docs/leios/design-note.md and docs/GITHUB_PROJECT_6WEEK.md, then review the linked roadmap and the [LLFN-k] sub-issues on the leios-main branch. This is a tracking issue rather than a single change; completion means the planned foundations, validity, and integration milestones form a coherent, type-checking Agda formalization.

Written by the indexing model from the issue text.