chore: add pre-push hook + update CONTRIBUTING.md

.githooks/pre-push

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+# Pre-push hook: runs the same lint.sh that CI runs.
+# Blocks push if any check fails.
+
+echo "Running pre-push lint check..."
+bash "$(git rev-parse --show-toplevel)/scripts/lint.sh"

CONTRIBUTING.md

@@ -1,137 +1,48 @@
 # Contributing to ProofAtlas
 
-## Using ProofAtlas in your own Lean 4 project
+## Setup
 
-Add to your `lakefile.toml`:
-
-```toml
-[[require]]
-name = "proofatlas"
-git = "https://github.com/MathNetwork/ProofAtlas"
-rev = "main"
-subDir = "lean"
+```bash
+git clone https://github.com/MathNetwork/ProofAtlas.git
+cd ProofAtlas
+git config core.hooksPath .githooks
+cd lean
+lake exe cache get
+lake build
 ```
 
-Then in any `.lean` file:
+The `git config` line enables the pre-push hook, which runs
+`scripts/lint.sh` before every push — same checks as CI.
 
-```lean
-import ProofAtlas
+## Branch strategy
 
-#atlas.graph Nat.add_zero
-#atlas.resistance Nat.add_zero Nat.succ_eq_add_one
 ```
-
-`lake update && lake build` and the `#atlas.*` commands work in your
-infoview. Your `lean-toolchain` should match the one in
-`lean/lean-toolchain` of this repo.
-
-For a local checkout, use the path form instead:
-
-```toml
-[[require]]
-name = "proofatlas"
-path = "/absolute/path/to/hypergraph-geo/lean"
+main           ← production, sorry-free, only accepts PRs from development
+development    ← research, sorry allowed, accepts PRs from feature branches
+feat/xxx       ← your work, cut from development
 ```
 
-## Exporting geometric reports
+1. `git checkout development && git checkout -b feat/your-topic`
+2. Write code, commit
+3. `git push origin feat/your-topic`
+4. Open PR → `development` (not main)
+5. CI passes → merge
+6. When development has verified work ready for production: PR `development` → `main`
+
+## Before pushing
 
-For shell pipelines, CI snapshots, or external analysis, dump a
-declaration's geometric report as JSON via the `atlas-export` binary:
+The pre-push hook runs `bash scripts/lint.sh` automatically. You
+can also run it manually:
 
 ```bash
-lake exe atlas-export Nat.add_zero
-lake exe atlas-export Nat.add_zero Nat.add_comm            # glued
-lake exe atlas-export --out report.json Nat.succ_eq_add_one
+bash scripts/lint.sh
 ```
 
-Without `--out` the JSON goes to stdout, so it pipes into
-anything. The schema matches `Pipeline/Export.lean`'s
-`ToJson HypergraphReport`: incidence data, resistance matrix,
-δ-hyperbolicity, and root indices (one per input declaration).
-
-The companion binary `lake exe atlas-export-demos` writes the
-landing-page demo set under `site/data/atlas-demos.json`; re-run
-it whenever the seed declarations or the pipeline change shape.
-
-## Architecture Decision Records
-
-Some choices in the codebase aren't obvious from the diff alone —
-e.g. *why* we picked Mathlib's `Digraph` over `Quiver`, or *which*
-2-section convention `toSimpleGraph` uses. Those choices live in
-`docs/adr/` so they survive a change of maintainer.
-
-You don't need an ADR for every PR. Write one when your change
-involves any of these:
-
-- **Choosing an external dependency or target type** for a new
-  public API (e.g. "use type `X` from package `Y` here").
-- **Defining new public-API semantics** where two reasonable
-  readings exist (e.g. "full 2-section vs input-output 2-section").
-- **Naming or layout conventions** that affect more than one file.
-- **Cross-file architectural decisions** (layer boundaries,
-  spec-vs-instance splits, new directory conventions).
-
-Bug fixes, refactors that preserve the public API, and single-file
-implementations with self-contained reasoning don't need an ADR.
-
-To add one: copy `docs/adr/template.md` to
-`docs/adr/NNNN-your-title.md`, fill it in, link it from the PR. The
-template and the trigger list are explained in detail in
-[`docs/adr/README.md`](docs/adr/README.md).
-
-## Where to read next
-
-- **First-time user?** Run through the
-  [tutorial](docs/tutorial.md) (5 minutes, end-to-end).
-- **Want the big picture?** The
-  [architecture document](docs/architecture.md) explains the four
-  layers and what each one owns.
-- **Want to add a feature?** Two recipes:
-  - [How to add a new mapping](docs/how-to/add-a-mapping.md) —
-    extract a hypergraph from some Lean object.
-  - [How to add a new metric](docs/how-to/add-a-metric.md) —
-    register a new `IsHypergraphMetric` instance.
-- **Want to track progress?** [STATUS.md](docs/STATUS.md) is the
-  transparent checklist; [ROADMAP.md](docs/ROADMAP.md) is the
-  forward direction.
-
-The short version of "how to add a new metric":
-
-1. Define your metric in `ProofAtlas/Metric/YourMetric/Basic.lean`
-2. Prove `IsHypergraphMetric` in `ProofAtlas/Metric/YourMetric/Instance.lean`
-3. Register the metric in `scripts/check_metric_instances.sh`
-4. Run `#atlas.status yourMetricDist` — it should show ✓
-5. CI will check automatically
-
-## Open tasks
-
-For scoped, beginner-friendly entry points, see the
-[good first issue tracker](https://github.com/MathNetwork/ProofAtlas/labels/good%20first%20issue).
-Each one is sized for under a day's work and covers documentation,
-code, or infrastructure.
-
-The list below is the longer-horizon work that doesn't yet have a
-specific issue. Each task is self-contained — pick one and open a
-PR.
-
-### IsHypergraphMetric instances (discharge `sorry`)
-- [ ] `jsDist_isHypergraphMetric` — needs JS triangle inequality (Endres–Schindelin 2003)
-- [ ] `diffusionDist_isHypergraphMetric` — needs diffusion metric axioms
+## Architecture decisions
 
-### Float compute paths (new)
-- [ ] Float commute time in `Pipeline/` — enables `#atlas.commute`
-- [ ] Float JS distance in `Pipeline/` — enables `#atlas.jsd`
-- [ ] Float eigensolver in `Pipeline/` — enables `#atlas.spectrum` and `#atlas.cluster`
+Write an ADR in `docs/adr/` for cross-file architectural changes.
+See [`docs/adr/README.md`](docs/adr/README.md).
 
-### Command language (new)
-- [ ] `#atlas.commute` — compute commute time distance
-- [ ] `#atlas.jsd` — compute JS distance
-- [ ] `#atlas.diffusion` — compute diffusion distance at scale `t`
-- [ ] `#atlas.spectrum` — spectral decomposition of `L_κ`
-- [ ] `#atlas.cluster` — spectral clustering
-- [ ] `#atlas.delta.ns!` — Monte-Carlo δ sampler for large namespaces
+## License
 
-### Documentation
-- [ ] Metrics page: intuition + math + Lean code for each metric
-- [ ] Theory page: δ-hyperbolicity, spectral decomposition, Hausdorff, GH
-- [ ] How-to: fill an open `sorry`
+Apache 2.0 (see `LICENSE`).