chore: sync development to main

.github/workflows/check.yml

@@ -20,16 +20,24 @@ jobs:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
     steps:
-      - name: Check branch name
+      # Enforce branch strategy (ADR 0007):
+      #   PR to main → source must be development
+      #   PR to development → source must be feat/fix/chore/docs/refactor
+      - name: Check branch strategy
         run: |
-          BRANCH="${{ github.head_ref }}"
-          if [[ ! "$BRANCH" =~ ^(feat|fix|chore|docs|refactor)/ ]]; then
-            echo "::error::Branch name '$BRANCH' does not follow the convention."
+          TARGET="${{ github.base_ref }}"
+          SOURCE="${{ github.head_ref }}"
+          if [[ "$TARGET" == "main" && "$SOURCE" != "development" ]]; then
+            echo "::error::PRs to main must come from the development branch."
+            echo "Workflow: feature branch → development → main"
+            exit 1
+          fi
+          if [[ "$TARGET" == "development" && ! "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ ]]; then
+            echo "::error::Branch '$SOURCE' does not follow naming convention."
             echo "Must start with: feat/, fix/, chore/, docs/, or refactor/"
-            echo "Example: fix/42-broken-linter"
             exit 1
           fi
-          echo "✓ branch name OK: $BRANCH"
+          echo "✓ branch strategy OK: $SOURCE → $TARGET"
 
       - name: Check PR title
         run: |

CLAUDE.md

@@ -17,10 +17,11 @@ intervention needed.
 - **No `import Mathlib`** — full import banned; Lean syntax linter
   `Util/Linter/ImportBan.lean` enforces at build time.
 - **Build green** — `lake build` must pass.
-- **Branch protection** — direct push to `main` blocked; PRs only.
-- **CI required** — `lint` and `conventions` jobs must pass before merge.
-- **Branch naming** — must start with `feat/`, `fix/`, `chore/`,
-  `docs/`, or `refactor/`. CI enforces on PRs.
+- **Branch protection** — `main` and `development` both protected;
+  no direct push, PRs only.
+- **Branch strategy** — PRs to `main` must come from `development`.
+  PRs to `development` must come from `feat/`/`fix/`/`chore/`/
+  `docs/`/`refactor/` branches. CI enforces.
 - **PR title** — must match `type(scope): summary` (conventional
   commit format). CI enforces on PRs.
 

README.md

@@ -2,108 +2,60 @@
 
 **Mathematics of the Structure of Mathematics**
 
-A Lean 4 library and toolchain that turns formal proofs into computable
-geometric objects: take any `Lean.Expr`, get back a hypergraph, a metric,
-and a δ-hyperbolicity number — all end-to-end verified.
+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.
 
-🌐 **Live site:** [proof-atlas.vercel.app](https://proof-atlas.vercel.app/)
+## What it does
 
-## What's in the repo
+```lean
+import ProofAtlas
 
-```
-.
-├── lean/        Lean 4 library (proof + compute layers, lake-buildable)
-├── site/        Next.js + MDX documentation site
-├── whitepaper/  Project white paper (en + zh, LaTeX)
-├── docs/        Architecture, ADRs, how-tos
-└── scripts/     CI and audit scripts
+#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
 ```
 
-## The four-step approach
-
-1. **Define the structure.** Encode the BDF (Barkeshli–Douglas–Freedman)
-   hypergraph as a Lean 4 `structure` whose four axioms (directed,
-   ordered, coloured, acyclic) hold by construction. Every Lean
-   declaration's proof term lifts to a BDF hypergraph via
-   `Lean.Expr.toHypergraph` — zero `sorry`s.
-2. **Define geometry and topology.** Formalize an open spec,
-   `IsHypergraphMetric` (four metric-space axioms plus three sensitivity
-   witnesses), against which any candidate distance can register.
-   Currently four metrics ship: **resistance**, **commute time**,
-   **Jensen–Shannon**, **diffusion**.
-3. **Develop the theory.** Prove δ-hyperbolicity, spectral
-   decomposition, Hausdorff and Gromov–Hausdorff distances — all
-   metric-agnostic, taking any `IsHypergraphMetric` as a hypothesis.
-4. **Interpret the structure.** Run the pipeline:
-   `Lean.Environment → IncidenceData → ResistanceMatrix → δ`,
-   producing a `HypergraphReport { n, edges, δ }` end-to-end.
-
-## Quick start
+## What's on `main`
 
-```lean
-import ProofAtlas
+Everything on `main` is sorry-free. `import ProofAtlas` gives you:
 
-#eval geometricProfileOfExprs
-  #[Lean.Expr.app (.const ``id [.zero]) (.const ``Nat []),
-    Lean.Expr.app (.const ``Nat.succ []) (.const ``Nat.zero []),
-    Lean.Expr.app (.const ``id [.zero])
-      (.app (.const ``Nat.succ []) (.const ``Nat.zero []))]
--- HypergraphReport(n=8, edges=4, δ=0.083333)
-```
+- **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.
 
-Triangle = single application (`id Nat`) has resistance 2/3 between
-any pair. Three declarations with shared constants (`id`, `Nat.succ`,
-`Nat.zero`) glue into one 8-vertex hypergraph with non-trivial
-δ = 1/12. Const-sharing across declarations is automatic.
-
-## Status
-
-| Component | State |
-|---|---|
-| `Hypergraph` structure + four axioms | ✅ |
-| `Lean.Expr → Hypergraph` translation | ✅ 0 sorries |
-| `IsHypergraphMetric` spec | ✅ |
-| `resistanceDist_isHypergraphMetric` instance | ✅ 0 sorries (5 hypotheses) |
-| `commuteTimeDist_isHypergraphMetric` | ⚠ stub |
-| `jsDist_isHypergraphMetric`, `diffusionDist_isHypergraphMetric` | ⚠ stub |
-| Spectral decomposition | ✅ |
-| `Hyperbolic/Basic.lean` (4 lemmas) | ⚠ 4 sorries |
-| `Open.lean` (Conjecture 7.3) | 🔓 intentional `sorry` |
-| End-to-end `Pipeline/` (compute layer) | ✅ |
-| CI: `scripts/check_metric_instances.sh` | ✅ |
-
-`lake build` is green (3486 jobs). Total project `sorry` count: 11 +
-the open conjecture.
+Work in progress (on `development` branch): commute time, Jensen–Shannon, diffusion metrics, spectral theory.
 
 ## Build
 
 ```bash
-# Lean library
 cd lean
 lake exe cache get
 lake build
-
-# Docs site
-cd ../site
-npm install
-npm run dev      # http://localhost:3000
-npm run build
 ```
 
-## Documentation
+## Repository structure
+
+```
+.
+├── 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
+```
 
-The full documentation site is live at
-[proof-atlas.vercel.app](https://proof-atlas.vercel.app/) and sourced
-from `site/` (Next.js + MDX). It includes:
+## Contributing
 
-- The four-step architecture
-- BDF hypergraph definition with worked examples (modus ponens,
-  conjunction-intro, two-step derivations as Mermaid diagrams)
-- `IsHypergraphMetric` spec and the four registered instances
-- Live Lean source via `<LeanSource>` — the docs show the actual
-  on-disk Lean and a `sorry`-status badge per anchor
-- Theory page (δ-hyperbolicity, spectral, Hausdorff/GH)
-- End-to-end pipeline
+See [CONTRIBUTING.md](CONTRIBUTING.md). Branch strategy:
+`feat/xxx` → `development` → `main`.
 
 ## License
 

lean/ProofAtlas.lean

@@ -21,15 +21,25 @@ import ProofAtlas.LinearAlgebra.Default
 import ProofAtlas.RandomWalk.FundamentalMatrix
 import ProofAtlas.RandomWalk.KemenySnell
 import ProofAtlas.RandomWalk.CommuteTime
--- RandomWalk.Spectral.Default depends on MCMC; on development branch.
+import ProofAtlas.RandomWalk.Spectral.Default
 
--- Metric: spec + verified MCMC-free instances only
+-- Metric: all instances (development branch — sorry allowed)
 import ProofAtlas.Metric.Default
 import ProofAtlas.Metric.Resistance.Instance
--- CommuteTime.Instance depends on MCMC; on development branch.
+import ProofAtlas.Metric.CommuteTime.Instance
+import ProofAtlas.Metric.JensenShannon.Basic
+import ProofAtlas.Metric.JensenShannon.Instance
+import ProofAtlas.Metric.Diffusion.Basic
+import ProofAtlas.Metric.Diffusion.Instance
 import ProofAtlas.Metric.Hausdorff
 import ProofAtlas.Metric.GromovHausdorff
 
+-- Hyperbolicity + sequences (sorry'd, development only)
+import ProofAtlas.Hypergraph.Sequence
+import ProofAtlas.Hyperbolicity.Default
+import ProofAtlas.Hyperbolicity.Diffusion
+import ProofAtlas.Open
+
 -- Mapping: Expr → Hypergraph
 import ProofAtlas.Mapping.ExprColor
 import ProofAtlas.Mapping.Expr

lean/ProofAtlas/Command/Status.lean

@@ -5,6 +5,9 @@ Authors: MathNetwork
 -/
 import ProofAtlas.Command.Common
 import ProofAtlas.Metric.Resistance.Instance
+import ProofAtlas.Metric.CommuteTime.Instance
+import ProofAtlas.Metric.JensenShannon.Instance
+import ProofAtlas.Metric.Diffusion.Instance
 
 /-!
 # `#atlas.status` — `IsHypergraphMetric` registry lookup

lean/ProofAtlas/Metric/Default.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: MathNetwork
 -/
 import ProofAtlas.Util.Linter.MetricRegistry
+import ProofAtlas.Metric.CommuteTime.KilledChain
+import ProofAtlas.Metric.CommuteTime.HittingTime
 import ProofAtlas.Metric.Axioms
+import ProofAtlas.Metric.CommuteTime.CommuteTime
 import ProofAtlas.Metric.Resistance.Canonical
 import ProofAtlas.Metric.Resistance.HarmonicLaplacian
 import ProofAtlas.Metric.Resistance.Algebraic
@@ -13,6 +16,9 @@ import ProofAtlas.Metric.Resistance.Structural
 import ProofAtlas.Metric.Resistance.Resistance
 import ProofAtlas.Metric.Resistance.Spectral
 import ProofAtlas.Metric.Resistance.Instance
+import ProofAtlas.Metric.CommuteTime.Instance
+import ProofAtlas.Metric.JensenShannon.Instance
+import ProofAtlas.Metric.Diffusion.Instance
 
 /-!
 # BDF commute time metric — facade

lean/ProofAtlas/Util/Linter/MetricRegistry.lean

@@ -50,7 +50,9 @@ private partial def dependsOnSorry (env : Environment) (name : Name)
 (metric name for display, fully qualified instance theorem name). -/
 private def metricRegistry : Array (String × Name) :=
   #[ ("resistanceDist",  `Hypergraph.resistanceDist_isHypergraphMetric)
-   -- commuteTimeDist, jsDist, diffusionDist: on development branch.
+   , ("commuteTimeDist", `Hypergraph.commuteTimeDist_isHypergraphMetric)
+   , ("jsDist",          `Hypergraph.jsDist_isHypergraphMetric)
+   , ("diffusionDist",   `Hypergraph.diffusionDist_isHypergraphMetric)
    ]
 
 /-- **Eng.** Syntax for the compile-time metric registry guard. -/