v1.18.0 — stranded-proof recovery tool + fuller browser surfaces

Headline: recovery tooling and fuller browser surfaces — a tools/repo/reroute_stranded.py maintainer tool re-routes a stranded direct proof PR onto the accepted queued path without re-proving (the dispatcher re-packages it; Gate A re-verifies from scratch) — the recovery engine behind "the ruv sledgehammer fix" (#1904). On the browser side, the leaderboard gains a Sourcing tab that finally surfaces the already-generated sourcing board, and the proof graph now renders every goal — standalone goals fold into one collapsed summary cluster per status that expands on click, instead of being omitted so the diagram looked nearly empty.

Added

• Added tools/repo/reroute_stranded.py, a maintainer tool that re-routes a stranded direct proof PR through the accepted queued path (ADR-058) without re-proving. Direct prove(...) PRs are no longer accepted (the queued-proof cutover), and pre-cutover ones strand with gate-a-audit/gate-a-replay perpetually queued. Since the dispatcher only re-packages an existing branch (Gate A re-verifies from scratch), the tool copies a stranded PR's proof files onto a fresh queued/prove/<goal>/… branch off current origin/main, Gate-B-validates it, and (with --push) pushes it so the dispatcher meters it into CI. Self-contained proofs re-route cleanly; one importing a now-archived Unsorry.* module fails Gate A on dispatch (the safe outcome). Built to recover @ruvnet's stranded proofs (issue #1904, "the ruv sledgehammer fix").
• Added a Sourcing view to the leaderboard page (ADR-060): a fourth toggle that surfaces the sourcing leaderboard (docs/metrics/sourcing-leaderboard.json) in the browser — who sourced each goal, ranked by goals sourced with a proved/open/difficulty split. The data was already generated by python3 -m tools.leaderboard --sourcing but had no browser surface; it is now one click from the contributor leaderboard, lazily fetched the first time the tab is opened.

Changed

• The proof-graph page now shows every goal, not just the ~7% that sit in decomposition forests. Standalone goals (no parent→sub lineage) are folded into one collapsed summary cluster per status alongside the forest (ADR-032 amendment / SPEC-032-A); on the interactive page a cluster expands on click into its individual, clickable goals and collapses again (the client rebuilds the Mermaid source from the embedded model, byte-identical to the server render when collapsed), while the static markdown shows the collapsed clusters and the full per-goal list stays in the table. Previously standalone goals were omitted from the diagram entirely, so it read as if most of the 762 goals were missing.