[LLF1-1] Design note: the Leios Ledger Formalization plan decisions

Two to three page document, `docs/leios/design-note.md`, timeboxed to two days, recording the Leios Ledger Formalization (LLF) plan and the defaults it assumes and builds on, so that every later issue encodes rather than debates.

- [ ] Module placement: the `Leios` subtree of `Ledger.Dijkstra.Specification` (the module map in `docs/GITHUB_PROJECT_6WEEK.md`).
- [ ] Certified application uses the full `LEDGERS` relation; reapply is an implementation optimization to be justified by the follow-up soundness theorem.
- [ ] Environment and ordering: EB transactions apply from the announcing block's post-BBODY state, before any tick to the certifying block's slot; a certificate-bearing block carries no transactions of its own (CIP-164).
- [ ] Certificate failure is the absence of a BBODY transition; no predicate-failure taxonomy in the LLF plan.
- [ ] Committee: epoch-fixed, stake-based truncation over registered voting keys; pinned at announcement; keyless seats hold stake but cannot sign.
- [ ] Parameters: the CIP-164 Table 3 list plus the per-EB reference-script bound from cardano-ledger #5965, with group assignments.
- [ ] Availability: the rules take the EB's transaction closure as input, with a matching premise; no availability obligations.
- [ ] The interface table: each function from the proposed consensus↔ledger interface mapped to its LLF counterpart or marked follow-up/consensus-only.

Amendments (2026-08-19 field review, from the Musashi trace-verifier work):

- [ ] Pending-EB lifetime made explicit: any applied block replaces the pending announcement with its own (possibly absent) one; no announcement survives an intervening block (protocol-level spec: the certifiable EB is the one announced by `currentRB`, the head).
- [ ] Certifiability stated plainly: parameter well-formedness does not imply a reachable quorum; keyless seats hold coverage stake but cannot sign (Musashi 2026-08: 19 of 66 pools keyless, certificates on roughly 3% of blocks).
- [ ] The committee order (descending stake, ties by ascending pool id) is a stated law of the abstract selection function, with determinism required and the byte-exact pool-id comparison flagged upstream.
- [ ] Known constant divergence recorded: prototype `minCertificationGap` = 10 versus the formula's 14 with the Musashi parameters.
- [ ] The EB-identifier hash preimage marked as a conformance cliff (byte-exact preimage to be pinned before conformance testing).
- [ ] Rewards and incentives declared out of scope, with the CIP's own words.

Once it's ready, the doc should be circulated to Dražen, Javier, Nicolas, Alexey, and Polina for comment; feedback is folded in later, never awaited.

Estimated effort: 2 days (joint).

Create docs/leios/design-note.md, using the module map in docs/GITHUB_PROJECT_6WEEK.md and the listed CIP-164, committee, availability, interface, and amendment decisions as the outline. Record each default and follow-up boundary, including the pending-EB lifetime, ordering law, constant divergence, and hash preimage cliff; circulate the finished note to the named reviewers without waiting for feedback.

Written by the indexing model from the issue text.