CI: Palomar structure check per project + palomar-prepare skill

[jleder3]

Adds a fast, toolchain-free Palomar structure check as the first step of the per-project verify job in lean-projects.yml, so a project folder that does not have the layout the Palomar registry requires fails within seconds, before elan, the Mathlib cache or Comparator are touched. Also adds a palomar-prepare skill with the full preparation checklist, and documents both in the README. The detect/select logic, caches, runner variable and the comparator step are unchanged.

What .github/scripts/palomar-structure-check.sh <project> checks

The registry's rules for "the selected project directory" (How to submit; PalomarTemplate; PalomarPolicy CONTRIBUTING.md §2–3). Violations fail the job, warnings are printed (as ::warning:: annotations in CI).

1. Lakefile — exactly one of lakefile.toml / lakefile.lean; lake-manifest.json committed (violation if missing for lakefile.lean, warning for lakefile.toml); every git package in the manifest is a public https://github.com/owner/repo URL pinned to a full 40-character commit SHA.
2. Toolchain — lean-toolchain (project-local, else the repository-root file; the report says which) matches leanprover/lean4:vX.Y.Z or vX.Y.Z-rcN; nightlies / custom toolchains are violations.
3. Challenge module (conventionally Challenge.lean; dotted modules such as Challenge.XiPrime are resolved through the lakefile's source dirs) — exists; ≤ 1000 lines and ≤ 100 KiB (violation), > 300 lines or > 32 KiB (warning: "should be small and readable"); its imports are only Lean core / Mathlib and its dependency closure / TauCeti — importing a project module is a violation; declares at least one theorem/def; contains sorry placeholders (warning if none); no axiom.
4. Solution module (conventionally Solution.lean) — exists; after stripping comments: no sorry, no native_decide / ofReduceBool, no axiom declaration (violations).
5. Comparator configuration (comparator.json; comparator*.json / comparator/config*.json and paths named in formalization.yaml are also picked up, as in comparator-check.sh) — valid JSON object in leanprover/comparator's schema with only the keys challenge_module, solution_module, theorem_names, definition_names (optional), permitted_axioms, enable_nanoda; names ≥ 1 declaration; permitted_axioms ⊆ {propext, Quot.sound, Classical.choice}; challenge ≠ solution module; every named declaration occurs (final name component, comments stripped) in the Challenge source (violation if not) and in the Solution source (warning; violation if none does).
6. formalization.yaml at the project root (violation if absent). Parsed with PyYAML when available (textual key scan otherwise). Violations: missing/empty project.name, project.description (the registry abstract, ≤ 10000 chars), project.authors, project.license, project.responsible_maintainers, classification.arxiv, automation.methods[].method, review.status; a thin wrapper without repository.substantive_formalization.{id,revision}; leftover TEMPLATE: values. Warnings: version ≠ v0.4, licence other than Apache-2.0, sources[] missing or an entry without title / a relationship in formalizes|adapts|independently-proves|background|other, > 2 arXiv categories, missing/odd classification.msc2020, missing status.{scope,sorry_count,axioms}, non-zero sorry_count, missing fidelity.divergences, neither status.main_results nor alignment.statements.
7. Licence — exactly one conventional licence file (LICENSE, LICENCE, COPYING, … optionally .md/.txt) at the repository root, non-empty.
8. Project-wide sweep (warnings): axiom declarations and native_decide/ofReduceBool in any other .lean file of the project (comments stripped) — Comparator remains the real gate; compiled artefacts (.olean, .ilean, .trace, …) outside .lake are a violation.

No network, no Lean; needs bash and python3. Run locally from the repository root: bash .github/scripts/palomar-structure-check.sh <project>.

Skill

.claude/skills/palomar-prepare/SKILL.md (/palomar-prepare): when to use; the layout checklist above and the script; toolchain/Mathlib pinning; how to write Challenge.lean (Mathlib-only, statements with deliberate sorry, size limits), Solution.lean (same names, no sorry/native_decide/axiom; conditional results take hypotheses as explicit arguments or a [LiteratureHypotheses] instance, never axiom) and comparator.json (schema used in this repo); the full formalization.yaml field checklist (name, authors, licence, maintainers, original vs source-based, substantive vs thin wrapper, arXiv/MSC2020, automation methods incl. the role of AI and human review, review status, per-theorem plain-language account, fidelity gaps, sources with formalizes/adapts/independently-proves/background, prior formalizations, acknowledgements); local verification (lake build, #print axioms, comparator-check.sh → Your solution is okay!); hygiene; PR checklist; and a final "Submitting to Palomar (human step)" section (merge → full commit SHA from main → submission form with project path = folder name → GitHub sign-in proves write access → keep the status page URL; machines should not drive the form).

Local test results

• zeta23/ (current main layout): passes, 0 warnings.
• percolation/ as proposed in wip: scaffold #22: passes, 0 warnings (report below). wip: scaffold #22 is open; once this PR is merged, pushes to wip: scaffold #22 run the structure check on percolation/ automatically.
• Negative cases (temporary copies of zeta23/): Solution.lean deleted → fails (comparator.json: Solution module 'Solution' has no source file); lean-toolchain = leanprover/lean4:nightly-2026-08-01 → fails; a copy with lakefile.lean and no manifest, no formalization.yaml, a project import in the Challenge, sorry + native_decide + axiom in the Solution, an extra permitted axiom and a name missing from the Challenge → 8 violations, each reported; pre-Lay out zeta23 as a Palomar template project #20 formalization.yaml (no project.description) with a TEMPLATE: value and an unknown key in comparator.json → fails on exactly those three points.
• Same results with PyYAML hidden from python3 (textual fallback, one extra warning).
• bash -n and shellcheck -S warning clean; workflow YAML parses (yaml.safe_load); the new step runs with working-directory: . right after checkout.

Report for percolation/ (tree of #22)

Palomar structure check: percolation  (repository root: <clone>)
  ok    lakefile: lakefile.toml
  ok    lean-toolchain: leanprover/lean4:v4.32.0 (from percolation/lean-toolchain)
  ok    formalization.yaml: project 'percolation'
  ok    challenge: percolation/Challenge.lean (152 lines, 9174 bytes)
  ok    solution: percolation/Solution.lean
  ok    config: comparator.json -> Challenge / Solution, 2 declaration(s)
  ok    licence: LICENSE (repository root)
Palomar structure check OK for percolation: lakefile, toolchain, Challenge/Solution, 1 comparator configuration(s), formalization.yaml, LICENSE (0 warning(s)).
exit=0

Report for zeta23/

Palomar structure check: zeta23  (repository root: <clone>)
  ok    lakefile: lakefile.toml
  ok    lean-toolchain: leanprover/lean4:v4.33.0-rc2 (from zeta23/lean-toolchain)
  ok    formalization.yaml: project 'Zeta23 — more than two thirds of the zeta zeros are simple and on the critical l...'
  ok    challenge: zeta23/Challenge.lean (231 lines, 13335 bytes)
  ok    solution: zeta23/Solution.lean
  ok    config: comparator.json -> Challenge / Solution, 17 declaration(s)
  ok    challenge: zeta23/Challenge/XiPrime.lean (106 lines, 5468 bytes)
  ok    solution: zeta23/Solution/XiPrime.lean
  ok    config: comparator-xiprime.json -> Challenge.XiPrime / Solution.XiPrime, 6 declaration(s)
  ok    licence: LICENSE (repository root)
Palomar structure check OK for zeta23: lakefile, toolchain, Challenge/Solution, 2 comparator configuration(s), formalization.yaml, LICENSE (0 warning(s)).
exit=0