chore: drop development branch, simplify to feature → main

.github/workflows/check.yml

@@ -20,24 +20,15 @@ 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
+      - name: Check branch naming
         run: |
-          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
+          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,14 @@ 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;
-  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 protection** — `main` protected; no direct push, PRs only.
+- **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)