CI: build with warnings as errors, axiom audit, zizmor; style rules

[MarcIlunga]

The repository had no CI. This adds it, secures the workflows, and records the style rules in AGENTS.md. It touches only .github/, scripts/ and AGENTS.md, so the open stack (#3 ← #4 ← #21 ← #22) picks it up on its next rebase without conflicts.

Units

• .github/workflows/ci.yml: on pull requests (any base, so stacked PRs are checked) and on main:
  1. scripts/check-sources.sh;
  2. lake build --wfail through leanprover/lean-action with the Mathlib cache (any warning fails, including declaration uses 'sorry');
  3. scripts/check-axioms.sh.
• scripts/check-sources.sh: no axiom declarations, no native_decide/bv_decide/Lean.ofReduceBool, no @[implemented_by]/@[extern], no maxHeartbeats/maxRecDepth/synthInstance.maxSize.
• scripts/check-axioms.sh: runs every file under src/Tests containing #print axioms (10 files, 490 endpoints on main) and fails on any axiom outside propext, Classical.choice, Quot.sound, sorryAx included. It finds the audit files itself, so new audits are covered without editing the script.
• .github/workflows/zizmor.yml: zizmor 1.30.1 on the workflows; findings fail the job.
• .github/dependabot.yml: weekly updates of the pinned actions, grouped, with a seven-day cooldown.
• AGENTS.md: a Style section (Mathlib's style guide and naming conventions, with this repository's exceptions; lines of at most 100 characters; new and changed code passes Mathlib's standard linter set). The Verification section now lists the CI steps.

Workflow hardening: top-level permissions: {}, per-job contents: read (CI) or none (zizmor); actions pinned to commit hashes (actions/checkout v7.0.1, leanprover/lean-action v1.6.1, zizmorcore/zizmor-action v0.6.4); persist-credentials: false; no pull_request_target; concurrency groups; timeouts.

Review checks

• Local: scripts/check-sources.sh passes on main.
• Local: lake build --wfail on main: 2873 jobs, no warnings.
• Local: scripts/check-axioms.sh on main: 490 endpoints, all within the envelope; a probe theorem probeSorry : False := sorry with #print axioms makes it fail with sorryAx.
• Local: shellcheck scripts/*.sh clean; zizmor 1.30.1 reports nothing at the regular, pedantic and auditor personas.
• CI on this PR: both workflows green.

Not in this PR

• Enabling weak.linter.mathlibStandardSet in the lakefile, and the cleanup it needs (on Distinguisher behaviors and absorption; the AE proof in Banfi's steps #3's tree: 589 long lines, 78 #print/#eval in tests, 65 open Classical, 39 show, 22 multiGoal, 22 flexible, 25 unused Fintype/DecidableEq arguments, 6 other). A separate PR after the stack lands.
• A ruleset on main (require a pull request and this CI, block force-pushes and deletion). Repository settings, applied by an admin.
• leanchecker and a downstream build of cbc-mac-cc / chachapoly-cc.

🤖 Generated with Claude Code

https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9