Adds automated guardrails so mathematical rigor is enforced by tooling
instead of by convention. See docs/math-first-tooling.md for the full
contract.
Schemas + registry:
- shared-data/schemas/deepseek-review-receipt.schema.json
Draft 2020-12 schema for the existing ollama_deepseek_review_receipt_v1
and ollama_deepseek_review_continuation_receipt_v1 receipt formats. Pins
sha256:<hex> hashes, non-negative token counts, repo-relative POSIX
paths, and rejects additional fields.
- shared-data/schemas/claims-registry.schema.json
Schema for claims.yaml. Requires review_receipts when status is
verified-by-ai and a lean source when status is formally-proven.
- claims.yaml
Initial registry entry: prime-gap-entropy-collapse (verified-by-ai)
linked to the two existing receipts under
shared-data/artifacts/deepseek_review/.
Validators (scripts/math-first/):
- validate_deepseek_receipts.py: validates tracked or passed receipts
against the JSON Schema; shared by pre-commit and CI.
- test_validate_deepseek_receipts.py: positive + 7 negative fixtures
asserting exit-code behaviour.
- validate_claims_registry.py: schema check + unique id check + on-disk
existence check for every referenced repo-relative path.
- require_math_evidence.py: gate that requires a DeepSeek receipt, a
Lean change, or a claims.yaml update alongside edits to math-track
surfaces (Lean Semantics kernels, ArithmeticSpec docs, stack
solidification receipts).
Pre-commit (.pre-commit-config.yaml):
- check-json, check-yaml, end-of-file-fixer, trim trailing whitespace,
detect-private-key (scoped to math-first files only per AGENTS.md
Do Not Sweep).
- Local hooks wiring all three math-first validators above.
CI (.github/workflows/math-check.yml):
- validate-schemas: compiles every schema, runs both validators, runs
the validator self-tests, then re-invokes the canonical Ollama
emitter in --verify-only mode against every tracked receipt to
re-check answer_sha256 against the answer-file bytes on disk.
- require-evidence: enforces the math-track evidence rule at PR scope.
- pre-commit: runs all pre-commit hooks against the PR diff so the
contract holds even for contributors who skip installing hooks
locally.
MCP (.mcp.json):
- filesystem, sympy, wolfram-alpha, lean, deepseek-review entries
pointing at off-the-shelf upstream servers and at the canonical
ollama_deepseek_review_emitter.py. Secrets stay in the runtime env
(WOLFRAM_ALPHA_APPID, OLLAMA_API_KEY) and are never embedded.
Docs (docs/math-first-tooling.md):
- Philosophy, surfaces, schema reference, registry workflow, hook
catalogue, CI catalogue, MCP catalogue, end-to-end verify command.
shared-data/schemas/*.schema.json and claims.yaml live under paths the
top-level .gitignore would normally exclude; they are force-added via
git add -f the same way existing promoted receipts under
shared-data/artifacts/deepseek_review/ are tracked (per AGENTS.md).
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
