chore: Cleanup and linting after the initial Clean changes

[dtumad]

Summary

This branch began as a proof/lemma cleanup pass after the initial Clean-native refactor and
grew to also restructure and harden CI. The two halves are independent and neither changes any
declarations or mathematical content.

CI

The CI workflow (.github/workflows/lean_action_ci.yml) went from a single build job to four
jobs, and the project now has lake test / lake lint drivers plus lightweight compiler trust guards.

Job graph

• guards — source-policy gates on a standard runner, in parallel with the heavy build so a
  forbidden pattern fails the PR in seconds without a Lean build:
  • scripts/check_no_skipkerneltc.sh — no set_option (debug.)skipKernelTC in source (it bypasses
    the kernel type-check re-run, the trust anchor for axiom-clean proofs).
  • scripts/check_no_native_decide.sh — no native_decide in the main SP1Clean/ library (it trusts
    the whole compiler via Lean.ofReduceBool/Lean.trustCompiler).
• build — the heavy project build, now also publishing the freshly-built .lake/build oleans to a
  commit-keyed cache (lake-build-${{ github.sha }}) for the downstream jobs. lean-action's own cache
  only covers dependencies (keyed on the manifest), not the per-commit project build.
• lint (needs: build) — lake lint (the new sp1Lint driver) split into its own job so it shows
  up as an independent check. Restores the commit-keyed cache so it reads the already-built oleans instead
  of rebuilding.
• test (needs: build, parallel with lint) — lake test (the new SP1CleanTest library: the
  witness-generation + whole-trace native_decide conformance anchors, checked against batteries dumped
  from SP1's real Rust prover). Restores the same cache and only elaborates the test modules. Split out so
  the trusted-compiler checks are clearly independent in the checks list.

Test / lint drivers and the test-library split

• Added a top-level SP1CleanTest library (glob SP1CleanTest.+) holding all witness/trace
  conformance anchors — the only place native_decide is allowed. It imports SP1Clean but is never
  imported by it, so the default lake build SP1Clean stays native_decide-free (now enforced by the
  guards job). Wired as the testDriver in lakefile.toml.
• Added scripts/sp1Lint.lean + a sp1Lint lean_exe, wired as the lintDriver. A thin custom driver
  over the Batteries #lint framework running a curated subset of linters over the hand-written
  SP1Clean.* declarations only, excluding the auto-generated Extracted/ + *Vectors code (the stock
  runLinter scopes by namespace root and can't make that exclusion). Residual suppressions live in
  scripts/nolints.json.
• Moved the Mathlib syntactic style linters from package scope to per-lib moreLeanArgs on every
  hand-written pillar (SP1Math/SP1Model/SP1FormalModel/SP1Native/SP1Proofs + SP1CleanTest),
  which keeps the auto-gen SP1Extracted library out of the linter set. All eight flags are at zero
  violations.
• scripts/run_audit.sh now invokes both guard scripts as gates and reports the native_decide count
  from SP1CleanTest/ rather than SP1Clean/.

Cleanup

• DivRem soundness tail extraction — factored the ~267-line, byte-identical soundness tail that was
  duplicated across all nine DivRemChip/Soundness/*.lean variant files into a single shared
  DivRemChip/Soundness/Tail.lean helper (Already in perf: optimize the expensive portions of DivRem proofs #103 so could either merge that first or just close it).
• Golfed proofs throughout the chip layer (Bridge/Formal/Core/Math files across Bitwise, Lt, Jal,
  Addw, Shift, Store*, Load* chips, …) and extracted shared helper lemmas into Math/Gate.lean and
  Math/Word.lean.
• Fixed all errors from now-enforced syntactic style linters.
• Refreshed docs (AGENTS.md, docs/agents/proof-patterns.md, docs/architecture.md, docs/roadmap.md,
  docs/release-audit.md) and the audit snapshots (axiom-census.txt, axiom-ledger.md,
  compile-profile.md) to match the new layout and CI, plus minor generator tweaks
  (update_extracted.py, scripts/gen_axiom_probe.py).