# HighDimProb Visualizations

This directory contains a lightweight visualization layer for humans and agents
working on HighDimProb. The diagrams are documentation artifacts only: they do
not promote modules, prove theorems, or change theorem meanings.

## Files

| File | Format | Source | Purpose |
|---|---|---|---|
| `roadmap.html` | Interactive HTML | curated from the repository status, task, API, and source ledgers | Leaf-level status, dependencies, source ownership, filtering, and export. |
| `module_tree.mmd` | Mermaid | curated from `docs/architecture/ModuleTree.md` and `docs/architecture/BranchRegistry.md` | Root-to-branch-to-leaf structure and stability status. |
| `lake_import_graph.dot` | Graphviz DOT | generated by upstream `importGraph` via `lake exe graph --to HighDimProb` | Lightweight tracked Lean import graph output for auditing module imports. |
| `scalar_concentration_spine.mmd` | Mermaid | curated from source/tests | Main scalar concentration implication spine. |
| `hoeffding_path.mmd` | Mermaid | curated from source/tests | Rademacher and bounded-variable Hoeffding theorem paths. |
| `bernstein_path.mmd` | Mermaid | curated from `docs/archive/BernsteinPlan.md` | Scalar Bernstein and weighted Bernstein proof path. |
| `random_matrix_branch.mmd` | Mermaid | curated from `docs/archive/MatrixConcentrationPlan.md` | Random matrix infrastructure and statement status. |

## Viewing Mermaid

Mermaid files can be viewed directly in GitHub, VS Code extensions, or any
Mermaid renderer. They are written as standalone `flowchart TD` diagrams.

## Viewing The Interactive Roadmap

Open `roadmap.html` in a browser. It provides a zoomable task graph with status
colors, dependency edges, source ownership, detail panels, and export controls.
The Lean source and the current status/theorem ledgers remain authoritative.

## Rendering DOT

If Graphviz is installed, render the official import graph with:

```bash
dot -Tsvg docs/visualizations/lake_import_graph.dot -o docs/visualizations/lake_import_graph.svg
```

Graphviz is optional and is not a project dependency.

## Updating The Import Graph

Regenerate the official upstream `importGraph` output with:

```powershell
.\tools\build_import_graph.ps1
```

Or from Bash/Git Bash:

```bash
./tools/build_import_graph.sh
```

## Status Policy

- `stable` means reachable through `import HighDimProb`.
- `experimental` means reachable through `import HighDimProb.Experimental`.
- `typed Prop` means proof-ready or proof-planning statement vocabulary, not a
  proved theorem.
- `TODO` nodes are documentation-only unless a Lean declaration is named
  explicitly in the owning source file and theorem atlas.