Formalize normal-class rank and complete count/price bounds in Lean

.github/workflows/lean-normal-class-rank.yml

@@ -0,0 +1,41 @@
+name: Lean normal-class rank bound
+on:
+  pull_request:
+    paths:
+      - 'research/lean-normal-class-rank/**'
+      - '.github/workflows/lean-normal-class-rank.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'research/lean-normal-class-rank/**'
+      - '.github/workflows/lean-normal-class-rank.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Download checksum-pinned official Lean
+        shell: bash
+        run: |
+          curl --fail --location --retry 3 https://github.com/leanprover/lean4/releases/download/v4.33.0-rc1/lean-4.33.0-rc1-linux.tar.zst -o "$RUNNER_TEMP/lean.tar.zst"
+          echo "25e7b3e18ec75a4e2529fc23194be8e3cc3183df99b553f870d8a111c7488210  $RUNNER_TEMP/lean.tar.zst" | sha256sum --check
+          tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP"
+      - name: Build local proofs and check actual Lean rejection controls
+        shell: bash
+        run: |
+          python -I -O -B research/lean-normal-class-rank/verify.py \
+            --lake "$RUNNER_TEMP/lean-4.33.0-rc1-linux/bin/lake" \
+            --work-dir "$RUNNER_TEMP/normal-class-rank-build" \
+            --fetch-cache --out "$RUNNER_TEMP/normal-class-rank-result.json"
+      - name: Source and receipt failure controls
+        run: python -I -O -B research/lean-normal-class-rank/test_package.py
+      - run: git diff --exit-code