v1.17.1 — the ruv sledgehammer fix + board reconciliation

Headline: maintenance — "the ruv sledgehammer fix" and a board reconciliation — a patch release of fixes only. After a contributor's ~337 direct prove(...) PRs stranded against the queued-proof cutover (#1904), admission control now offers the re-route path when it closes a direct submission, so a flood self-heals into the metered queue instead of stranding, and @ruvnet's two git identities are mapped to the canonical handle so credit attaches. Alongside, the #1888 reconciliation flips two genuinely-proved goals that were still showing as open/translated (proved-status now matches the proof-index count), and the proof-graph page's heading scale and insets are aligned with the shared home/leaderboard card.

Fixed

• When admission control closes a post-cutover direct prove(...) PR, the auto-comment now offers the re-route path as well as the re-prove path, so a contributor's direct-submission campaign self-heals into the metered queue instead of stranding (the failure mode behind #1904, "the ruv sledgehammer fix"). The comment now tells anyone whose branch already holds a verified proof to run python3 -m tools.repo.reroute_stranded --pr <n> --push — the queued dispatcher re-packages it and Gate A re-verifies from scratch — in addition to the existing ./swarm/agent.sh --prove re-prove instructions.
• Fixed two goals that carried a kernel-verified proof index record but whose goal record was never flipped to proved, so they showed as open/translated on the queue and proof graph despite being solved (surfaced by the #1888 reconciliation; the proved-status count now matches the active proof-index count, 286). no-nat-sq-eq-two-mul-sq-s4 — a decomposition sub-lemma whose parent no-nat-sq-eq-two-mul-sq is already proved — was left status≜open/sha≜∅; it now records status≜proved and the proof sha. nat-zero-lt-succ — a grandfathered bootstrap lemma proved manually in Unsorry/Basic.lean with no goals/*.lean stub (the statement-binding generator deliberately skips such entries, ADR-011) — now records status≜proved; its phase≜translate/lean≜∅ are kept intentionally as the grandfathered marker. Statements are unchanged (ADR-018) — only the status/sha metadata is corrected.
• Fixed the proof-graph page's layout drifting from the home and leaderboard pages: its heading scale and section margins now match the shared card (text-5xl md:text-7xl wordmark, px-6 md:px-10 inset — previously text-4xl md:text-6xl / md:px-8), so the three browser surfaces align. Also removed the duplicate Contributor leaderboard header link — the shared top-nav already links the leaderboard.
• Fixed leaderboard attribution for @ruvnet, whose proof contributions carried solver≜ruvnet but were authored under the git identities ruv <ruv@ruv.net> (the proof campaign) and rUv <…ruvnet@users.noreply.github.com> (merged PR #1278), so the ADR-037 provenance audit flagged them as uncorroborated. docs/metrics/contributor-aliases.json now maps both identities to the canonical handle ruvnet, so the credit attaches correctly (issue #1904).