chore: simplify to feature → main, drop development layer

.github/workflows/check.yml

@@ -20,26 +20,9 @@ jobs:
     if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
     steps:
-      - 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 development."
-            exit 1
-          fi
-          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/"

CLAUDE.md

@@ -10,10 +10,7 @@ enforcement lives in CI and the Lean type system, not here.
 - **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` protected;
-  no direct push, PRs only.
-- **Branch strategy** — feature branches (`feat/`/`fix/`/`chore/`/
-  `docs/`/`refactor/`) → `development` → `main`. 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.