The account export names repositories the account can no longer read #185

OpenAgents.DataRights.AccountExport states one policy and applies two.

repository_work_export/1 documents and enforces that a record authored in a
repository the account can no longer read is not returned: it joins
OpenAgents.Repositories.readable_by/2 and filters the authoring column, and
both halves are proven separately (#165, 2498ecf).

Three other collections in the same module reach a repository with no read
predicate at all, joined only by the account's own rows:

• push_receipts_export/1 — left_join on repository.storage_key == receipt.repo, selecting repository.name and repository.owner
• deployments_export/1 — two left_joins on repository.id, selecting
  repository.owner and repository.name

Each then renders owner <> "/" <> name through repository_path/2.

The records themselves are the account's own, so this is not another account's
data. What it discloses is the repository's current owner and name — for a
private repository the account was removed from, or one renamed after they
left. The export tells them what it is called now.

Found while enumerating REPOSITORY-001 (#175). It is the residue class that
enumeration cannot catch: the joins name no visibility terms and call no
resolver, so neither the predicate scan nor the caller sets see them. It is
recorded in REPOSITORY-001 and in docs/2026-08-23-invariant-proof-audit.md.

The decision this needs

Not obviously a straight bug fix. Two defensible answers, and the module should
apply one of them everywhere rather than one silently per collection:

1. Withhold the path, keep the record. The account keeps its own receipt —
   storage_key, wal_seq, refs, timestamps — and repository is null
   when the repository is not currently readable. Their data survives; the
   current name does not leak.
2. Withhold the record. Matches repository_work exactly, at the cost of
   dropping receipts for work the account really did.

Prefer 1 unless there is a reason not to: a push receipt is the account's own
evidence, and #167/#169 just made it the thing they hold to verify the log.

Done when

• All four collections apply the same stated rule, and the module's own prose
  says which rule that is.
• A proof asserts it for each collection: an account that pushed to a
  repository it can no longer read gets its receipt without the path.
• The REPOSITORY-001 residue note is updated to say this instance is closed.