ci(proofs): gate the Lean 4 verification corpus (verification/proofs/lean4) (#275)

## What

Adds CI coverage for the **Lean 4 trust-pipeline property proofs** under
`verification/proofs/lean4/` — they previously fell through every
proof-CI filter.

- New `verif-lean` job in `dogfood-proofs-ci.yml`, a structural clone of
the existing
`lean` job (elan shim + pinned-toolchain pre-install with retry/backoff,
then `just`),
reading the pin from `verification/proofs/lean4/lean-toolchain` and
running a new
  `just proofs-verif-lean` recipe.
- New Justfile recipe `proofs-verif-lean` = `cd
verification/proofs/lean4 && lake build`,
also added to the `proofs` roll-up so `just proofs` checks it locally
too.
- Path triggers extended to `verification/proofs/lean4/**` (both `push`
and `pull_request`).

## Why

`dogfood-proofs-ci` gated only `proofs/{coq,lean,agda}` + `src/idris`;
the
`idris2-abi-ci` and `agda-meta-checker` workflows are path-filtered to
`src/abi/**`
and `meta-checker/**`. So the five property proofs here
(`ConfidenceLattice`, `ParetoMaximality`, `ParetoStrongMaximality`,
`IntegrityVerification`, `PortfolioCompleteness`) had **no** gate —
regressions would
have landed silently.

## Verification (run locally, not eyeballed)

On **Lean 4.13.0** (installed via the project's pinned tarball, the same
version the
corpus pins):

- Fresh `lake build` with `.lake/build` cleared first → all 5 modules
compile,
  `Build completed successfully`, exit 0 (~24 s).
- `just proofs-verif-lean` → exit 0.
- `grep -nE 'sorry|admit|^\s*axiom |native_decide'` across the corpus →
**none** —
  these are genuine, hole-free proofs.

No mathlib dependency (`lake-manifest` `packages: []`), so the job
builds well under the
20-minute timeout.

## Notes

- No source/proof files changed — CI wiring only.
- Next in the same sweep (separate PRs): gate
`verification/proofs/idris2` (Idris2,
`idris2 --check` per file), and a weekly cron for the heavier
Isabelle/Mizar corpora.

🤖 Generated with [Claude Code](https://claude.com/claude-code)


---
_Generated by [Claude
Code](https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/dogfood-proofs-ci.yml

@@ -18,12 +18,14 @@ on:
     branches: [main]
     paths:
       - 'proofs/**'
+      - 'verification/proofs/lean4/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   pull_request:
     branches: [main]
     paths:
       - 'proofs/**'
+      - 'verification/proofs/lean4/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   workflow_dispatch:
@@ -115,6 +117,56 @@ jobs:
       - name: Build Lean corpus
         run: just proofs-lean
 
+  verif-lean:
+    name: Lean 4 (verification)
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Install elan + pinned Lean toolchain
+        run: |
+          set -euo pipefail
+          # Mirrors the `lean` job: install the elan shim only, then pre-install the
+          # toolchain pinned by verification/proofs/lean4/lean-toolchain with
+          # retry/backoff so the Build step does not lazily resolve it (elan's release
+          # tag lookup against the GitHub API can transiently fail). This corpus has no
+          # mathlib dependency (lake-manifest packages: []), so it builds fast.
+          curl -fsSL --retry 3 \
+            https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          export PATH="$HOME/.elan/bin:$PATH"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          toolchain="$(tr -d '[:space:]' < verification/proofs/lean4/lean-toolchain)"
+          for attempt in 1 2 3 4 5; do
+            if elan toolchain install "$toolchain"; then
+              break
+            fi
+            if [ "$attempt" -eq 5 ]; then
+              echo "elan toolchain install failed after 5 attempts" >&2
+              exit 1
+            fi
+            backoff=$((attempt * 5))
+            echo "elan toolchain install failed (attempt $attempt); retrying in ${backoff}s" >&2
+            sleep "$backoff"
+          done
+          elan default "$toolchain"
+          lean --version
+
+      - name: Install just
+        run: |
+          set -euo pipefail
+          curl -fsSL --retry 3 \
+            "https://github.com/casey/just/releases/download/1.51.0/just-1.51.0-x86_64-unknown-linux-musl.tar.gz" \
+            -o /tmp/just.tar.gz
+          mkdir -p "$HOME/.local/bin"
+          tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Build Lean verification corpus
+        run: just proofs-verif-lean
+
   agda:
     name: Agda
     runs-on: ubuntu-latest

Justfile

@@ -250,7 +250,7 @@ test-s4-loop:
 # exact same commands.
 
 # Type-check the whole dogfood proof corpus across every assistant.
-proofs: proofs-coq proofs-lean proofs-agda proofs-idris
+proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean
 
 # Compile the Coq proof corpus (proofs/coq/**/*.v).
 proofs-coq:
@@ -284,6 +284,14 @@ proofs-agda:
 proofs-idris:
     cd src/idris && idris2 --typecheck echidna-validator.ipkg
 
+# Distinct from proofs-lean: the verification-pipeline *property* proofs
+# (ConfidenceLattice, ParetoMaximality, ParetoStrongMaximality, IntegrityVerification,
+# PortfolioCompleteness) under verification/proofs/lean4, not the dogfood corpus under
+# proofs/lean. No mathlib dependency (lake-manifest packages: []), so the build is light.
+# Build the Lean 4 trust-pipeline property proofs via Lake (verification/proofs/lean4).
+proofs-verif-lean:
+    cd verification/proofs/lean4 && lake build
+
 # Format code
 fmt:
     cargo fmt