CI + CLAUDE.md: shake unused-import baseline gate

Adds a `lake exe shake OpenGALib --no-downstream` step in CI that
counts flagged files and fails the build on growth. Baseline `35`
captures the current import-hygiene debt remaining after the two
recent shake-pass commits (60 → 45 → 35).

Discipline mirrors `EXPECTED_SORRY` and the three linter baselines:
the count only ever decreases. To shrink, apply shake's suggestion to
the flagged file, add explicit imports to any broken downstream
consumers (Mathlib-standard "every file declares its actual
dependencies"), then drop the EXPECTED_SHAKE value.

CLAUDE.md grows a "Unused-import hygiene" section documenting the
tool, the noshake.json baseline, and the known `--fix` quirk
(over-applies on our codebase, so manual / scripted apply with
full-build verification is the supported workflow).

Author: Xinze-Li-Moqian

.claude/CLAUDE.md

@@ -166,6 +166,14 @@ CI implementation (`.github/workflows/ci.yml`): the build job greps `lake build`
 
 Adding a new linter: drop `OpenGALib/Util/Linter/<Name>.lean` (template: `MathTag.lean`), add the option to the `register_linter_set` in `Util/Linter.lean`, add a `#guard_msgs` test in `Tests/Linter/<Name>.lean`, add the baseline check in `ci.yml`. The `Util/Linter/README.md` walks the full template.
 
+## Unused-import hygiene (`shake`)
+
+`lake exe shake OpenGALib --no-downstream` (from the `batteries` package) detects unused imports and missing transitive-relied-on imports. False positives (tactic / notation / instance side-effect modules) are filtered via `scripts/noshake.json` — Mathlib's universal `ignoreImport` baseline plus OpenGALib-specific side-effect modules.
+
+CI baselines the count (currently `35`); growth fails the build. Cleanup is gradual: each PR either holds the count or reduces it. To reduce, apply shake's suggestion (`remove [old]`, `add [new]`) to the flagged file; if the full build then breaks downstream, add the right explicit imports to the broken consumer file (the Mathlib-standard "make every file declare its actual dependencies" pattern) and re-verify.
+
+Shake's `--fix` flag is known to over-apply (removes more than reported) on our codebase, so manual / scripted apply with full-build verification is the supported workflow.
+
 ## Sorry discipline
 
 Every sorry / opaque / placeholder is categorized:

.github/workflows/ci.yml

@@ -124,3 +124,18 @@ jobs:
             FAIL=1
           fi
           exit $FAIL
+
+      - name: Shake — unused-import baseline
+        run: |
+          # `lake exe shake` flags files with unused imports (and missing
+          # transitive-relied-on imports). Baseline is current debt; CI
+          # fails on growth, mirrors Mathlib's `noshake.json` discipline.
+          ACTUAL=$(lake exe shake OpenGALib --no-downstream 2>&1 | grep -c "^/.*\.lean:$" || echo 0)
+          EXPECTED_SHAKE=35
+          echo "Shake suggestions: $ACTUAL (expected ≤ $EXPECTED_SHAKE; gradually reduce)"
+          if [ "$ACTUAL" -gt "$EXPECTED_SHAKE" ]; then
+            echo "::error::Shake regression: $ACTUAL > $EXPECTED_SHAKE"
+            echo "Add the missing import to the consumer file, or update EXPECTED_SHAKE only when reducing."
+            echo "Run \`lake exe shake OpenGALib --no-downstream\` locally to see the suggestions."
+            exit 1
+          fi