docs: S5 step 4 landed; attention predicates in the test record (P4b S5)

The As-built block records step 4 built after U0b, its two items and
their tests; docs/testing.md names them and what P12 must mutate (the
number exemption, the open/partial check, sends.is_empty(), the two day
comparisons with their checked date arithmetic, the last-send max);
docs/parity.md says sent tracking also feeds Needs attention.

plan/served.md

@@ -1339,8 +1339,9 @@ Each unit follows the 8.0.4 template. "A-n" is an owner answer numbered in 8.3.1
 5. **Files:** owns the `Sent` types and `Ledger::mark_sent`, the `invoice.sent` arms, `books.mark_sent`; touches the 8.0.3 files.
 6. **Tests and proofs:** named above; no kernel change, no Lean change (a send moves no money). 8.0.6 items 1-4, 6.
 7. **Done when:** (1) the tests pass; (2) a send on a fixture book changes no report and no `DocState` (`a_send_changes_no_figure`); (3) an older version stops at the `invoice.sent` line with `NewerJournal` (the `tests/format.rs` arm); (4) `just check` green; (5) attention parity holds.
-8. **As built** (2026-10-27, branch `S5`): Build steps 1-3 and 5 are done; **step 4 (the two attention items) is deferred until U0b lands** (8.0.5 R-F: no attention item before it), as the EM directed. Departures:
+8. **As built** (2026-10-27, branch `S5`): Build steps 1-5 are done. ~~step 4 (the two attention items) is deferred until U0b lands~~ → built after U0b landed (`cc4f104f`), on main `ed637f0e` (D-55). Departures:
    - ~~no Lean change (a send moves no money)~~ → AGENTS.md's formal-methods bar (I-13) wins: `Ledger::mark_sent` is a new `Ledger` command, so `verify/lean/Wanderbooks/Documents.lean` gains `sends` on `Books`, `Step.markSent` and `Step.markSent_changes_no_figure` (no axioms), listed in `Audit.lean` and in `docs/verification.md` rule 34.
+   - Step 4: `ledger-package::attention` gains `Target::Invoice` and two items, `invoice_never_sent` (an issued invoice still Open or Partial, no send, past `invoicing.unsent_days`; a legacy invoice with no number is exempt) and `invoice_not_reminded` (overdue, last send older than `invoicing.reminder_days`); both are Todo, open the invoice, and offer `books.mark_sent` with the invoice. The viewer maps the target (one line in its Target→Route table; it owns no item) and draws them; `books.start` turns them into next steps from the one function. Tests: `an_unsent_invoice_is_listed_until_a_send_clears_it` (`attention-unsent-invoice.png`), `a_legacy_invoice_with_no_number_is_never_listed_as_unsent`, `an_overdue_invoice_with_an_old_send_is_asked_to_remind`, `an_unsent_invoice_is_on_both_lists`; `the_viewer_and_books_start_see_the_same_attention` stays green.
    - The MCP parameter for the recipients is `recipients`, not `to`: `no_tool_takes_a_path` refuses a parameter named `to` (a whole-word path-name rule, I-2). The journal event and the result keep the plan's `to`.
    - `Ledger::mark_sent` also passes `note` through `parties::check_text`, beside `to` and `reference`: a note must not carry a full TIN (I-7).
    - `LedgerError::DocumentVoid` (the plan's name) and `LedgerError::InvalidSend` (the text refusals) are new variants.