chore: sync development to main

README.md

@@ -1,61 +1,23 @@
 # ProofAtlas
 
-**Mathematics of the Structure of Mathematics**
+A Lean 4 library that turns formal proofs into computable mathematical objects.
 
-A Lean 4 library that turns formal proofs into computable geometric
-objects: take any `Lean.Expr`, get back a hypergraph, a metric, and
-a δ-hyperbolicity number.
+[Documentation](https://proof-atlas.vercel.app/) · [White Paper](whitepaper/) · [Contributing](CONTRIBUTING.md)
 
-## What it does
-
-```lean
-import ProofAtlas
-
-#atlas.resistance Nat.add_zero Nat.add_comm
--- R(Nat.add_zero, Nat.add_comm) = 1.234567
-
-#atlas.delta Nat.add_zero Nat.add_comm Nat.succ_eq_add_one
--- δ = 0.083333
-
-#atlas.graph Nat.add_zero
--- interactive hypergraph in the infoview
-```
-
-## What's on `main`
-
-Everything on `main` is sorry-free. `import ProofAtlas` gives you:
-
-- **Hypergraph structure** — BDF proof hypergraph with four axioms
-- **`IsHypergraphMetric` spec** — 7-check quality certificate
-- **Resistance distance** — proven `IsHypergraphMetric` instance
-- **Pipeline** — `Lean.Expr → IncidenceData → ResistanceMatrix → δ`
-- **8 commands** — `#atlas.graph`, `#atlas.resistance`, `#atlas.delta`, etc.
-
-Work in progress (on `development` branch): commute time, Jensen–Shannon, diffusion metrics, spectral theory.
-
-## Build
+## Quick start
 
 ```bash
 cd lean
 lake exe cache get
 lake build
 ```
 
-## Repository structure
+```lean
+import ProofAtlas
 
+#atlas.resistance Nat.add_zero Nat.add_comm
+#atlas.graph Nat.add_zero
 ```
-.
-├── lean/        Lean 4 library
-├── site/        Documentation site (proof-atlas.vercel.app)
-├── whitepaper/  Project white paper (en + zh)
-├── docs/        Architecture, ADRs, how-tos
-└── scripts/     CI and quality gate scripts
-```
-
-## Contributing
-
-See [CONTRIBUTING.md](CONTRIBUTING.md). Branch strategy:
-`feat/xxx` → `development` → `main`.
 
 ## License