fix: drop widget rendering from public proof states

[ejgallego]

Summary

• remove Lean.Widget.goalToInteractive from the public proof-state path
• render Goal / GoalHyp directly as plain strings from proof snapshots
• keep the public JSON shape while removing widget-tag complexity we do not expose

Why

• the public runAt proof-state payload only exposes plain strings
• the old widget rendering path added complexity and surfaced transport internalError under repeated proof-handle workload pressure
• direct plain-string rendering is both simpler and more robust for the current API

Testing

• lake build RunAt:shared runAt-search-workload-report runAt-test
• ./.lake/build/bin/runAt-test tests/interactive/proofConstructorBoundary.lean
• loaded runAt-search-workload-report 48 20260321 batch: 5/5 success under 24-core synthetic load

Notes

• this intentionally keeps the current public JSON shape
• widget-based rendering is no longer used for public proof-state construction