chore: sync development with main

.github/workflows/check.yml

@@ -20,24 +20,32 @@ jobs:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
     steps:
-      # 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: |
           TARGET="${{ github.base_ref }}"
           SOURCE="${{ github.head_ref }}"
+          # Feature branches → development only
+          if [[ "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ && "$TARGET" != "development" ]]; then
+            echo "::error::Feature branches must target development, not $TARGET."
+            exit 1
+          fi
+          # PRs to main → must come from development
           if [[ "$TARGET" == "main" && "$SOURCE" != "development" ]]; then
-            echo "::error::PRs to main must come from the development branch."
-            echo "Workflow: feature branch → development → main"
+            echo "::error::PRs to main must come from development."
             exit 1
           fi
-          if [[ "$TARGET" == "development" && ! "$SOURCE" =~ ^(feat|fix|chore|docs|refactor)/ ]]; then
+          echo "✓ branch strategy OK: $SOURCE → $TARGET"
+
+      - name: Check branch naming
+        run: |
+          SOURCE="${{ github.head_ref }}"
+          if [[ "$SOURCE" == "development" ]]; then exit 0; fi
+          if [[ ! "$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/"
             exit 1
           fi
-          echo "✓ branch strategy OK: $SOURCE → $TARGET"
+          echo "✓ branch naming OK: $SOURCE"
 
       - name: Check PR title
         run: |

CLAUDE.md

@@ -5,16 +5,17 @@ enforcement lives in CI and the Lean type system, not here.
 
 ## Enforced automatically
 
-- **Docstring tags** — `**Math.**` / `**Eng.**` / `**Mixed.**`
-  on public declarations (`Util/Linter/MathTag.lean`).
+- **Docstring required** — every public declaration must have a
+  `/-- ... -/` docstring (`Util/Linter/DocstringRequired.lean`).
 - **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** — `main` and `development` both protected;
+- **Branch protection** — `main` and `development` 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.
+- **Branch strategy** — feature branches (`feat/`/`fix/`/`chore/`/
+  `docs/`/`refactor/`) → `development` → `main`. CI enforces.
+- **Branch naming** — branches must start with `feat/`/`fix/`/`chore/`/
+  `docs/`/`refactor/`. CI enforces.
 - **PR title** — must match `type(scope): summary`. CI enforces.
 
 ## Conventions (not yet automated)

lean/ProofAtlas.lean

@@ -3,7 +3,8 @@ Copyright (c) 2026 MathNetwork. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: MathNetwork
 -/
-import ProofAtlas.Util.Linter
+import ProofAtlas.Util.Linter.MathTag
+import ProofAtlas.Util.Linter.ImportBan
 import ProofAtlas.Astrolabe.Nerve
 import ProofAtlas.Astrolabe.Net
 import ProofAtlas.Hypergraph.Basic

lean/ProofAtlas/Astrolabe/Nerve.lean

@@ -3,7 +3,6 @@ Copyright (c) 2026 MathNetwork. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: MathNetwork
 -/
-import ProofAtlas.Util.Linter
 
 /-!
 # AstroNerve — a node in a content-addressable hypergraph
@@ -12,9 +11,9 @@ Identity is computed from record + refs (Merkle property).
 Each reference carries an abstract role tag.
 -/
 
-/-- A node in a content-addressable hypergraph.
-`refs`: ordered references with role tags. `record`: content.
-Identity computed from record + refs via `identify`. -/
+-- Two fields: refs (ordered references with roles) and record (content).
+-- Id, Role, Record are abstract types. identify computes id from
+-- record + refs — content-addressing by construction.
 structure AstroNerve {Id : Type} {Role : Type} {Record : Type}
     (identify : Record → Array (Role × Id) → Id) where
   refs : Array (Role × Id)
@@ -26,42 +25,43 @@ namespace AstroNerve
 variable {Id : Type} {Role : Type} {Record : Type}
     {identify : Record → Array (Role × Id) → Id}
 
-/-- Compute identity from record + refs. Not stored — always derived. -/
+-- Compute identity from record + refs. Not stored — always derived.
 def id (n : AstroNerve identify) : Id := identify n.record n.refs
 
-/-- Number of references this nerve has. -/
+-- Number of references this nerve has.
 def width (n : AstroNerve identify) : Nat := n.refs.size
 
-/-- True if the nerve has no references (an atom / leaf node). -/
+-- True if the nerve has no references (an atom / leaf node).
 def isAtom (n : AstroNerve identify) : Bool := n.refs.isEmpty
 
-/-- All referenced ids, in order, without roles. -/
+-- All referenced ids, in order, without roles.
 def refIds (n : AstroNerve identify) : Array Id := n.refs.map (·.2)
 
-/-- All roles, in order, without ids. -/
+-- All roles, in order, without ids.
 def refRoles (n : AstroNerve identify) : Array Role := n.refs.map (·.1)
 
-/-- Does this nerve reference a given id? -/
+-- Does this nerve reference a given id?
 def containsRef [BEq Id] (n : AstroNerve identify) (i : Id) : Bool :=
   n.refs.any (fun ref => ref.2 == i)
 
-/-- Get the i-th ref. Returns `none` if out of bounds. -/
+-- Get the i-th ref (returns Option to handle out-of-bounds).
 def refAt (n : AstroNerve identify) (i : Nat) : Option (Role × Id) :=
   n.refs[i]?
 
-/-- Add a ref at the end. Returns a new nerve with a new id. -/
+-- Add a ref at the end. Returns a new nerve (new id, Merkle property).
 def pushRef (n : AstroNerve identify) (ref : Role × Id) : AstroNerve identify :=
   { refs := n.refs.push ref, record := n.record }
 
-/-- Remove the last ref. Returns a new nerve with a new id. -/
+-- Remove the last ref. Returns a new nerve (new id).
 def popRef (n : AstroNerve identify) : AstroNerve identify :=
   { refs := n.refs.pop, record := n.record }
 
-/-- Keep only refs matching a predicate. Returns a new nerve. -/
+-- Keep only refs matching a predicate. Returns a new nerve (new id).
 def filterRefs (n : AstroNerve identify) (p : (Role × Id) → Bool) : AstroNerve identify :=
   { refs := n.refs.filter p, record := n.record }
 
-/-- Swap two refs by index. Returns a new nerve with a new id. -/
+-- Swap two refs by index. Returns a new nerve (new id).
+-- Panics if indices out of bounds.
 def swapRefs [Inhabited Role] [Inhabited Id]
     (n : AstroNerve identify) (i j : Nat) : AstroNerve identify :=
   let a := n.refs
@@ -70,17 +70,18 @@ def swapRefs [Inhabited Role] [Inhabited Id]
   let a := a.set! j tmp
   { refs := a, record := n.record }
 
-/-- Reverse the order of all refs. Returns a new nerve. -/
+-- Reverse the order of all refs. Returns a new nerve (new id).
 def reverseRefs (n : AstroNerve identify) : AstroNerve identify :=
   { refs := n.refs.reverse, record := n.record }
 
-/-- Replace ref at position i. Returns a new nerve with a new id. -/
+-- Replace ref at position i. Returns a new nerve (new id).
+-- Panics if index out of bounds.
 def setRef (n : AstroNerve identify) (i : Nat) (ref : Role × Id) : AstroNerve identify :=
   { refs := n.refs.set! i ref, record := n.record }
 
 end AstroNerve
 
-/-- Show nerve as `Nerve(id=..., width=N)`. -/
+-- ToString: show nerve as "Nerve(id=..., width=N)".
 instance {Id Role Record : Type} {identify : Record → Array (Role × Id) → Id}
     [ToString Id] : ToString (AstroNerve identify) where
   toString n := s!"Nerve(id={n.id}, width={n.width})"