Publish a hosted leanblueprint site with interactive dependency graph

[raphaelrrcoelho]

Context

The repo maintains a blueprint (MathFin/Blueprint.lean + docs/blueprint.md, generated via lake exe blueprint_export + tools/blueprint_render.py) — but only as committed Markdown. The gold-standard Lean formalization projects (Polynomial Freiman–Ruzsa, sphere eversion, etc.) publish an interactive leanblueprint website to GitHub Pages: a LaTeX-rendered statement graph with an interactive dependency diagram and per-node states (stated / proved / ready to formalize). This is the single highest-leverage contributor-recruiting surface a formal-math repo can have.

Task

Stand up a hosted blueprint site:

1. Evaluate adopting leanblueprint (Massot's tool) vs. extending the existing blueprint_export + renderer to emit a static site with an interactive dependency graph (d3/dot).
2. Add a GitHub Pages deploy workflow (.github/workflows/) that rebuilds the blueprint on push to main.
3. Wire stated / proved / ready-to-formalize node states from the existing formalization_status taxonomy.

Acceptance criteria

• A blueprint site is published to GitHub Pages and linked from the README badge row.
• The dependency graph is interactive (clickable nodes → Lean source).
• Node states reflect full / reduced_core / gated.
• The site rebuilds automatically on main (no hand-publishing).
• Decision recorded in docs/ (leanblueprint vs. in-house renderer, with rationale).

Pointers

• MathFin/Blueprint.lean, docs/blueprint.md, docs/blueprint_nodes.json, tools/blueprint_render.py.
• Reference: leanblueprint as used by PFR / sphere-eversion.
• Existing Pages-style workflow precedent: .github/workflows/hf-publish.yml.