Add per-project CI: build + Palomar comparator check (changed projects only)

[jleder3]

Stacked on #18 (base branch move-zeta23-subfolder); GitHub retargets this PR to main automatically once #18 merges.

What it does

Adds .github/workflows/lean-projects.yml (+ .github/scripts/comparator-check.sh) so that every project subfolder is held to the Palomar registry's acceptance bar, and only projects whose files changed are re-verified.

• Triggers: pull_request (any branch), push to main, workflow_dispatch (input projects, default all).
• detect job (ubuntu-latest, seconds): projects = top-level directories containing lakefile.toml or lakefile.lean; selected = exactly those with a file in git diff --name-only base...head (PR: base.sha...head.sha; push: before...after). Changes outside the project directories — CI configuration under .github/**, README.md, LICENSE, .gitignore — select nothing, so a CI/doc-only change runs no verification (verify is skipped and the run is green). A full re-verify of every project is a manual workflow_dispatch run with projects = all (the default; a space-separated list of project names is also accepted). On a push with no usable before commit (first push of a branch, or a before no longer in the history) the diff is taken against the merge-base with main; if even that is impossible, nothing is selected and a warning points at the manual full run. Emits a JSON matrix.
• verify (project) job (matrix, fail-fast: false, runs-on: ${{ vars.LEAN_CI_RUNNER || 'ubuntu-latest' }} — set the repository/organization variable LEAN_CI_RUNNER to a larger-runner label such as ubuntu-latest-16-cores to shorten builds; Lake already uses every core — timeout-minutes: 360, working directory = the project):
  1. elan from the pinned release tarball (v4.2.3, sha256-checked, --default-toolchain none); the toolchain comes from the project's lean-toolchain.
  2. lake exe cache get if lake-manifest.json lists mathlib. On pull requests only, actions/cache then restores the project's most recent .lake/build for the same toolchain / lake-manifest.json / lakefile (key lakebuild-<os>-<project>-<hash>-<sha>, restore-key without the sha), so Lake rebuilds only the modules that changed, and saves the new build; pushes to main and workflow_dispatch runs build from scratch (no restore, no save). .lake/packages is never cached.
  3. lake build (default targets); fails on any declaration uses 'sorry' outside the trusted comparator statement files Challenge.lean / Challenge/<Topic>.lean.
  4. Palomar bar: builds the registry verifier's pinned tools and runs lake env comparator <config> for every configuration the project declares (comparator*.json next to the lakefile, or comparator/config*.json — for zeta23 that is comparator/config.json (17 statements) and comparator/config-xiprime.json (6)). Each run must exit 0 and print Your solution is okay!. As in the registry, permitted_axioms must be within propext / Quot.sound / Classical.choice, and comparator is handed a copy of the config with enable_nanoda forced to true, so the independent nanoda kernel re-check always runs. Comparator sandboxes its lake build Challenge|Solution, lean4export and nanoda invocations with landrun (real landrun, built from the pinned commit, as the registry does on the same hosted runners; the optional systemd-run AF_UNIX guard from the comparator README is not applied).
  5. Build log and per-config comparator logs are uploaded as the logs-<project> artifact.
• ~/.elan and the tool builds (~/.cache/lean-ci-tools) are cached with actions/cache, keyed on the toolchain and the tool pins. Only first-party actions (actions/checkout, actions/cache, actions/upload-artifact), pinned by commit. permissions: contents: read; concurrency: ${{ github.workflow }}-${{ github.ref }} with cancel-in-progress.

The Palomar bar and the tool pins

"Passes the Palomar bar" = the project builds on its pinned toolchain and leanprover/comparator — statement equality of every Solution theorem with its Mathlib-only Challenge namesake, axiom audit, replay in the Lean kernel and in the independent nanoda kernel via lean4export, inside landrun — prints Your solution is okay!.

Pins are copied from the registry's own verifier, PalomarRegistry/PalomarSubmission .github/workflows/submission.yml (at commit e215b18):

tool	pin	source
elan	release v4.2.3, tarball sha256 df0b2b3a…a8b2	submission.yml "Install pinned elan"
comparator	575674928e239f5bc452aab72d1dd7b0f1326494	submission.yml "Build pinned Comparator"
nanoda_lib	68d5ca9db226849b41a6fff59d796ff19d0a8840 (cargo build --release --locked)	submission.yml "Build pinned NanoDa kernel"
landrun	811cfff51ceaf3d9843708aa6d22e9b84ccac8b4 (CGO_ENABLED=0 go install)	submission.yml "Build pinned landrun"
lean4export	the release tag equal to the project's Lean version (for zeta23: v4.33.0-rc2 → 9fb131bb100eb32ccf6836f14e4f8328d13b6792), and its lean-toolchain must equal the project's	submission.yml "Build toolchain-matched lean4export" / verify_submission.py resolve_release_commit

The registry's verifier additionally wraps everything in an outer landrun boundary with confinement probes, a trusted-cache provenance audit and a canonical Challenge compile; those defend the registry against hostile submissions and are not reproduced here — this workflow reproduces the mechanical check (same tools, same pins, same success criterion), which is what a project must pass.

Adding a project

A new top-level directory with lakefile.toml/lakefile.lean, lean-toolchain, lake-manifest.json, a Mathlib-only Challenge module, a Solution module, and at least one comparator config (comparator.json or comparator/config*.json), plus a row in the root README table (the README gains a short "CI" section describing this). Nothing in the workflow names a project.

Known limits / things to decide

• Hosted-runner time. zeta23 is ~100k lines of Lean; on a standard 4-vCPU ubuntu-latest runner the cold lake build plus two comparator runs (each exports and replays the full proof cone in two kernels) may take several hours. The job timeout is the hosted maximum (360 min). If this proves too slow or memory-bound, set the LEAN_CI_RUNNER variable to a larger-runner label available to this repository — no workflow change needed.
• lean4export is resolved from a release tag at run time (the registry's rule), not from a SHA committed here; the resolved commit is printed in the log and is part of the tool-cache key. If a fixed SHA per toolchain is preferred, it is a one-line change in the pins step.
• Projects' own .lake is not cached (Mathlib comes from lake exe cache get; the project itself is rebuilt from source each run, which is the point of the check).
• Local reproduction: cd <project> && bash ../.github/scripts/comparator-check.sh (needs elan, git, go, cargo, jq; Linux for landrun).

This PR touches only .github/**, README.md and .gitignore, so under the rule above its own run selects [] and verify is skipped; the end-to-end exercise of zeta23 (detect → build → both comparator configs) is the manual workflow_dispatch run with projects = all, or the first PR that touches zeta23/.