Merge math-first tooling guardrails

.github/workflows/math-check.yml

@@ -0,0 +1,177 @@
+name: Math-First Checks
+
+on:
+  pull_request:
+    paths:
+      - '0-Core-Formalism/lean/Semantics/**'
+      - '6-Documentation/docs/distilled/**'
+      - 'shared-data/artifacts/deepseek_review/**'
+      - 'shared-data/data/stack_solidification/**'
+      - 'shared-data/schemas/**'
+      - 'scripts/math-first/**'
+      - 'claims.yaml'
+      - '.pre-commit-config.yaml'
+      - '.github/workflows/math-check.yml'
+  push:
+    branches:
+      - main
+      - distilled
+    paths:
+      - '0-Core-Formalism/lean/Semantics/**'
+      - '6-Documentation/docs/distilled/**'
+      - 'shared-data/artifacts/deepseek_review/**'
+      - 'shared-data/data/stack_solidification/**'
+      - 'shared-data/schemas/**'
+      - 'scripts/math-first/**'
+      - 'claims.yaml'
+      - '.pre-commit-config.yaml'
+      - '.github/workflows/math-check.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pull-requests: write
+
+concurrency:
+  group: math-check-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  validate-schemas:
+    name: Validate DeepSeek receipts and claims registry
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          submodules: false
+
+      - name: Setup Python 3.11
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.11'
+
+      - name: Install validator dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install "jsonschema>=4.21" "rfc3339-validator" "PyYAML"
+
+      - name: Validate JSON Schema files compile
+        run: |
+          python - <<'PY'
+          import json, sys
+          from pathlib import Path
+          from jsonschema import Draft202012Validator
+          for path in sorted(Path("shared-data/schemas").glob("*.schema.json")):
+              schema = json.loads(path.read_text())
+              Draft202012Validator.check_schema(schema)
+              print(f"OK   {path}")
+          PY
+
+      - name: Validate all tracked DeepSeek review receipts
+        run: |
+          python3 scripts/math-first/validate_deepseek_receipts.py
+
+      - name: Self-tests for receipt validator
+        run: |
+          python3 scripts/math-first/test_validate_deepseek_receipts.py
+
+      - name: Validate claims registry
+        run: |
+          python3 scripts/math-first/validate_claims_registry.py
+
+      - name: Verify receipt SHA-256 integrity against answer files
+        # Re-run the canonical emitter in --verify-only mode against every
+        # tracked receipt. This is the AGENTS.md contract for promoted
+        # Ollama/DeepSeek review receipts: answer_sha256 must match the bytes
+        # of the answer file on disk.
+        run: |
+          set -euo pipefail
+          shopt -s nullglob
+          emitter="5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py"
+          if [ ! -x "$emitter" ] && [ ! -f "$emitter" ]; then
+            echo "skip: $emitter not present (nothing to verify)"
+            exit 0
+          fi
+          receipts=(shared-data/artifacts/deepseek_review/*.receipt.json)
+          if [ "${#receipts[@]}" -eq 0 ]; then
+            echo "no receipts to verify"
+            exit 0
+          fi
+          failures=0
+          for receipt in "${receipts[@]}"; do
+            if python3 "$emitter" --verify-only "$receipt"; then
+              echo "OK   $receipt"
+            else
+              echo "FAIL $receipt"
+              failures=$((failures + 1))
+            fi
+          done
+          if [ "$failures" -gt 0 ]; then
+            echo "$failures receipt(s) failed --verify-only" >&2
+            exit 1
+          fi
+
+  require-evidence:
+    name: Require math evidence on math-track PRs
+    runs-on: ubuntu-latest
+    if: github.event_name == 'pull_request'
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Setup Python 3.11
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.11'
+
+      - name: Require receipt or Lean change alongside math-track edits
+        run: |
+          python3 scripts/math-first/require_math_evidence.py \
+            --from-git-diff origin/${{ github.base_ref }}
+
+  pre-commit:
+    name: Run pre-commit hooks on changed files
+    runs-on: ubuntu-latest
+    if: github.event_name == 'pull_request'
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          # We deliberately do not smudge LFS pointers here -- the pre-commit
+          # hooks never need the actual binary content, and pulling LFS would
+          # add noise. The next step disables the LFS smudge filters locally
+          # so pre-commit's stash/pop cycle does not trip over pointer files.
+          lfs: false
+
+      - name: Disable LFS filters for pre-commit
+        # pre-commit stashes unstaged changes before running hooks and pops
+        # them back after. When the working tree contains LFS pointer files
+        # but Git's LFS smudge filter is configured (per .gitattributes), the
+        # stash/pop cycle reports a phantom diff against the binary content
+        # Git thinks it should smudge, and the pop fails. Clearing the
+        # filters locally for this job removes the disagreement without
+        # mutating the repository or any LFS-tracked files.
+        run: |
+          git config --local filter.lfs.smudge ""
+          git config --local filter.lfs.clean ""
+          git config --local filter.lfs.process ""
+          git config --local filter.lfs.required false
+
+      - name: Setup Python 3.11
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.11'
+
+      - name: Install pre-commit
+        run: python -m pip install --upgrade pip "pre-commit>=3.7"
+
+      - name: Run pre-commit on changed files
+        run: |
+          base="origin/${{ github.base_ref }}"
+          head="HEAD"
+          pre-commit run --from-ref "$base" --to-ref "$head" --show-diff-on-failure

.mcp.json

@@ -0,0 +1,49 @@
+{
+  "$schema": "https://modelcontextprotocol.io/schemas/2025-03-26/client-config.json",
+  "_comment": "Math-first MCP server declarations for Research Stack. Each server below is gated on a runtime environment variable so the config never embeds secrets and so contributors who have not provisioned a given backend simply skip it. See docs/math-first-tooling.md for setup instructions.",
+  "mcpServers": {
+    "filesystem": {
+      "_comment": "Read/write proof artifacts, Lean kernels, and DeepSeek receipts. Scope is the repository root so review tooling cannot escape the project tree.",
+      "command": "npx",
+      "args": [
+        "-y",
+        "@modelcontextprotocol/server-filesystem",
+        "."
+      ],
+      "env": {}
+    },
+    "sympy": {
+      "_comment": "Local SymPy bridge for symbolic verification of arithmetic claims that appear in distilled docs and ArithmeticSpec. Backed by sympy-mcp upstream; see https://github.com/sdiehl/sympy-mcp.",
+      "command": "uv",
+      "args": [
+        "tool",
+        "run",
+        "--from",
+        "sympy-mcp",
+        "sympy-mcp"
+      ],
+      "env": {}
+    },
+    "wolfram-alpha": {
+      "_comment": "Wolfram Alpha symbolic verification. Required to discharge the `Verified with Wolfram Alpha` comments enforced by .github/workflows/wolfram-verification.yml. Provide a Short Answers API key via WOLFRAM_ALPHA_APPID at runtime; the server is otherwise dormant.",
+      "command": "npx",
+      "args": [
+        "-y",
+        "@wolfram-alpha/mcp-server"
+      ],
+      "env": {
+        "WOLFRAM_ALPHA_APPID": "${WOLFRAM_ALPHA_APPID}"
+      }
+    },
+    "lean": {
+      "_comment": "Lean 4 / Mathlib typecheck bridge. Targets 0-Core-Formalism/lean/Semantics/ via the existing lakefile. Requires `elan` on PATH; see GETTING_STARTED.md for the lean-toolchain pin (leanprover/lean4:v4.30.0-rc2).",
+      "command": "uvx",
+      "args": [
+        "lean-mcp",
+        "--lakefile",
+        "0-Core-Formalism/lean/Semantics/lakefile.toml"
+      ],
+      "env": {}
+    }
+  }
+}

.pre-commit-config.yaml

@@ -0,0 +1,88 @@
+# Research Stack pre-commit configuration
+# -----------------------------------------------------------------------------
+# Math-first guardrails that run on every commit. See docs/math-first-tooling.md
+# for the contract and rationale.
+#
+# Install once per clone:
+#   uv tool install pre-commit
+#   pre-commit install
+#
+# Run against the full tree:
+#   pre-commit run --all-files
+# -----------------------------------------------------------------------------
+
+default_install_hook_types: [pre-commit]
+fail_fast: false
+
+repos:
+  # --- Generic hygiene -------------------------------------------------------
+  - repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v5.0.0
+    hooks:
+      - id: check-json
+        # Schemas, MCP config, package.json, VS Code config, and JSON receipts.
+        files: '\.json$'
+        # Skip Lean editor metadata and Lake-managed lockfiles.
+        exclude: '\.(lean\.pist\.meta|lake)/'
+      - id: check-yaml
+        # Validate YAML at the syntactic level. The claims registry gets a
+        # stronger semantic check below.
+        files: '\.(ya?ml)$'
+      - id: end-of-file-fixer
+        # Force a trailing newline only on text files the math-first scripts
+        # actually own. Avoid sweeping the rest of the tree (see AGENTS.md).
+        files: '^(scripts/math-first/|shared-data/schemas/|claims\.yaml$|docs/math-first-tooling\.md$|\.mcp\.json$|\.pre-commit-config\.yaml$|\.github/workflows/math-check\.yml$)'
+      - id: trailing-whitespace
+        files: '^(scripts/math-first/|shared-data/schemas/|claims\.yaml$|docs/math-first-tooling\.md$|\.mcp\.json$|\.pre-commit-config\.yaml$|\.github/workflows/math-check\.yml$)'
+      - id: detect-private-key
+
+  # --- Math-first guardrails -------------------------------------------------
+  - repo: local
+    hooks:
+      - id: deepseek-receipt-schema
+        name: Validate DeepSeek review receipts
+        description: >-
+          Validates every tracked *.receipt.json under
+          shared-data/artifacts/deepseek_review/ against
+          shared-data/schemas/deepseek-review-receipt.schema.json.
+        entry: scripts/math-first/validate_deepseek_receipts.py
+        language: python
+        additional_dependencies:
+          - "jsonschema>=4.21"
+          - "rfc3339-validator"
+        files: '^shared-data/artifacts/deepseek_review/.*\.receipt\.json$'
+        # Pass matched files explicitly so partial commits still get a check
+        # but stay scoped to the changed receipts.
+        require_serial: true
+        types_or: [file]
+
+      - id: claims-registry-schema
+        name: Validate claims.yaml registry
+        description: >-
+          Validates claims.yaml against
+          shared-data/schemas/claims-registry.schema.json and asserts every
+          referenced repo-relative path exists on disk.
+        entry: scripts/math-first/validate_claims_registry.py
+        language: python
+        additional_dependencies:
+          - "jsonschema>=4.21"
+          - "PyYAML"
+        files: '^claims\.yaml$'
+        pass_filenames: false
+        require_serial: true
+
+      - id: receipt-required-for-math-content
+        name: Require a DeepSeek receipt or Lean proof for math-track content
+        description: >-
+          If a commit touches a file under one of the math-track surfaces
+          (Lean Semantics kernels, ArithmeticSpec docs, stack solidification
+          receipts), require that at least one file under
+          shared-data/artifacts/deepseek_review/ or
+          0-Core-Formalism/lean/Semantics/ is also part of the commit. This
+          enforces the math-first contract at commit time; the same check
+          runs in CI for PR-scope coverage.
+        entry: scripts/math-first/require_math_evidence.py
+        language: python
+        files: '^(0-Core-Formalism/lean/Semantics/|6-Documentation/docs/distilled/|shared-data/data/stack_solidification/).*$'
+        pass_filenames: true
+        require_serial: true

claims.yaml

@@ -0,0 +1,46 @@
+# Research Stack Mathematical Claim Registry
+# -----------------------------------------------------------------------------
+# Single source of truth for tracked mathematical claims and their current
+# rigor level. See docs/math-first-tooling.md for the math-first contract.
+#
+# Schema (per entry):
+#   id:            slug, kebab-case, stable across renames.
+#   title:         one-line natural-language statement of the claim.
+#   status:        one of:
+#                    conjecture          - asserted, no machine evidence yet
+#                    verified-by-ai      - has at least one DeepSeek review
+#                                          receipt and human spot-check
+#                    formally-proven     - Lean proof builds in lake
+#                    published           - peer-reviewed publication exists
+#   lean:          (optional) repo-relative Lean source or `theorem` symbol
+#                  that carries the proof obligation.
+#   review_receipts:
+#                  (optional) list of repo-relative `*.receipt.json` paths
+#                  emitted by ollama_deepseek_review_emitter.py.
+#   sources:       (optional) list of repo-relative supporting docs, scripts,
+#                  or external citations.
+#   notes:         (optional) free-form prose; keep short.
+#
+# The math-check CI workflow validates this file against the corresponding
+# JSON Schema at shared-data/schemas/claims-registry.schema.json (see
+# docs/math-first-tooling.md).
+# -----------------------------------------------------------------------------
+
+claims:
+  - id: prime-gap-entropy-collapse
+    title: >-
+      The prime-gap entropy-collapse detector rarely survives the corrected
+      K=21 selective braid threshold.
+    status: verified-by-ai
+    lean: 0-Core-Formalism/lean/Semantics/Semantics/HCMMR/Kernels/EntropyCollapseDetector.lean
+    review_receipts:
+      - shared-data/artifacts/deepseek_review/prime_gap_entropy_collapse_deepseek_deepseek-v3.2_20260512T033551Z.receipt.json
+      - shared-data/artifacts/deepseek_review/prime_gap_entropy_collapse_deepseek_deepseek-v4-flash_continuation_20260512T033849Z.receipt.json
+    sources:
+      - 6-Documentation/docs/distilled/ArithmeticSpec_Corrected_2026-05-11.md
+      - shared-data/data/stack_solidification/prime_gap_k21_rerun_receipt_2026-05-11.md
+    notes: >-
+      Continuation receipt covers the truncated tail of the primary review.
+      K=21 is the selective braid crossing threshold, not an entropy
+      threshold. The Lean kernel proves the discrete arithmetic fixture, and
+      the prime-gap rerun receipt records the surviving rare strict fires.

docs/math-first-tooling.md

@@ -0,0 +1,254 @@
+# Math-First Tooling
+
+This document codifies the "math first" contract for the Research Stack: every
+mathematical claim that ships from this repository must carry machine-checkable
+evidence — a Lean proof, a DeepSeek review receipt with SHA-256 integrity, or
+both — and the development environment must make it harder to bypass that
+contract than to honour it.
+
+It is the human-readable companion to:
+
+| Artifact | Path |
+|----------|------|
+| Receipt schema | [`shared-data/schemas/deepseek-review-receipt.schema.json`](../shared-data/schemas/deepseek-review-receipt.schema.json) |
+| Claim registry schema | [`shared-data/schemas/claims-registry.schema.json`](../shared-data/schemas/claims-registry.schema.json) |
+| Claim registry | [`claims.yaml`](../claims.yaml) |
+| Receipt validator | [`scripts/math-first/validate_deepseek_receipts.py`](../scripts/math-first/validate_deepseek_receipts.py) |
+| Registry validator | [`scripts/math-first/validate_claims_registry.py`](../scripts/math-first/validate_claims_registry.py) |
+| Evidence gate | [`scripts/math-first/require_math_evidence.py`](../scripts/math-first/require_math_evidence.py) |
+| Pre-commit config | [`.pre-commit-config.yaml`](../.pre-commit-config.yaml) |
+| CI workflow | [`.github/workflows/math-check.yml`](../.github/workflows/math-check.yml) |
+| MCP server registry | [`.mcp.json`](../.mcp.json) |
+
+Read [`AGENTS.md`](../AGENTS.md) and
+[`6-Documentation/wiki/DeepSeek-Review-Process.md`](../6-Documentation/wiki/DeepSeek-Review-Process.md)
+first — this document layers tooling on top of those contracts and does not
+restate them.
+
+## Philosophy
+
+1. **Lean is the source of truth.** Anything that can be stated as a Lean
+   `theorem` or kernel obligation should live under
+   `0-Core-Formalism/lean/Semantics/`. Other evidence (DeepSeek reviews,
+   SymPy/Wolfram cross-checks, hardware receipts) is a witness, not a proof.
+2. **Every claim has a status.** The states are
+   `conjecture → verified-by-ai → formally-proven → published`. Movement only
+   ever travels in that direction, and every transition is accompanied by a
+   change to `claims.yaml`.
+3. **Receipts pin model output to disk.** DeepSeek answers and their
+   `*.receipt.json` siblings carry `prompt_sha256` and `answer_sha256` so a
+   review can be re-validated without re-running the model.
+4. **CI enforces the contract.** Anything humans are expected to remember is
+   re-checked by a workflow that fails the PR if the contract is broken.
+5. **AI assistants get tool access, not trust.** The `.mcp.json` registry
+   gives Claude / Devin / Codex the Wolfram, SymPy, and Lean bridges they need
+   to discharge proof obligations — and nothing else. DeepSeek review remains
+   available through the canonical CLI emitter until a real MCP wrapper exists.
+
+## Repository Layout (math-first surfaces)
+
+```
+0-Core-Formalism/lean/Semantics/      # Lean source of truth (lakefile.toml)
+shared-data/schemas/                   # JSON Schemas for every receipt format
+shared-data/artifacts/deepseek_review/ # Promoted DeepSeek review receipts
+shared-data/data/stack_solidification/ # Stack receipts (math-track)
+6-Documentation/docs/distilled/        # Distilled math specs (math-track)
+scripts/math-first/                    # Validators + evidence gate
+claims.yaml                            # Single source of truth for claims
+.pre-commit-config.yaml                # Local guardrail
+.github/workflows/math-check.yml       # CI guardrail
+.mcp.json                              # AI-assistant tool registry
+```
+
+## Receipt Schema (`ollama_deepseek_review_receipt_v1`)
+
+The schema at
+[`shared-data/schemas/deepseek-review-receipt.schema.json`](../shared-data/schemas/deepseek-review-receipt.schema.json)
+formalises the contract that the canonical emitter
+[`5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py`](../5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py)
+already writes. It validates two receipt flavours:
+
+* **Primary review** (`ollama_deepseek_review_receipt_v1`) — requires
+  `schema`, `created_at`, `model`, `endpoint`, `prompt_sha256`,
+  `answer_sha256`, `usage.{prompt_tokens,completion_tokens,total_tokens}`,
+  `context_files` (non-empty), and `answer_path`.
+* **Continuation review** (`ollama_deepseek_review_continuation_receipt_v1`)
+  — replaces `context_files` with `previous_answer_path` and optionally
+  reports the `message_keys` returned by the continuation endpoint.
+
+Both flavours pin SHA-256 hashes as the literal string `sha256:<64 hex>`,
+require token counts to be non-negative integers, and require paths to be
+repo-relative POSIX strings ending in `.md` for answer paths. Additional
+fields are rejected so receipts stay shaped exactly as the emitter writes
+them.
+
+### Re-validate locally
+
+```bash
+uv run --python 3.11 \
+  --with "jsonschema>=4.21" --with "rfc3339-validator" \
+  python3 scripts/math-first/validate_deepseek_receipts.py
+```
+
+To validate a single receipt:
+
+```bash
+python3 scripts/math-first/validate_deepseek_receipts.py \
+  shared-data/artifacts/deepseek_review/<topic>_<model>_<ts>.receipt.json
+```
+
+The validator has its own self-tests:
+
+```bash
+python3 scripts/math-first/test_validate_deepseek_receipts.py
+```
+
+## Mathematical Claim Registry
+
+[`claims.yaml`](../claims.yaml) is the single source of truth for the rigor
+level of every tracked mathematical claim. The schema accepts these fields:
+
+| Field | Required | Notes |
+|-------|----------|-------|
+| `id` | yes | Stable kebab-case slug. |
+| `title` | yes | One-line natural-language statement of the claim. |
+| `status` | yes | `conjecture` \| `verified-by-ai` \| `formally-proven` \| `published`. |
+| `lean` | conditional | Required when `status == formally-proven`. Repo-relative Lean source path. |
+| `review_receipts` | conditional | Required when `status == verified-by-ai`. Repo-relative `*.receipt.json` paths. |
+| `sources` | no | Supporting docs, scripts, or external citations. |
+| `notes` | no | Free-form context. |
+
+```bash
+uv run --python 3.11 \
+  --with "jsonschema>=4.21" --with "PyYAML" \
+  python3 scripts/math-first/validate_claims_registry.py
+```
+
+The validator enforces the JSON Schema, asserts every `id` is unique, and
+asserts every repo-relative path referenced from `lean`, `review_receipts`,
+or `sources` exists on disk.
+
+## Pre-Commit Hooks
+
+`.pre-commit-config.yaml` wires four guardrails:
+
+* `pre-commit-hooks` — `check-json`, `check-yaml`, EOF / trailing whitespace
+  scoped to math-first files only (see [`AGENTS.md`](../AGENTS.md) "Do Not
+  Sweep"), and `detect-private-key`.
+* `deepseek-receipt-schema` — runs the receipt validator on every staged
+  `*.receipt.json` under `shared-data/artifacts/deepseek_review/`.
+* `claims-registry-schema` — runs the registry validator whenever
+  `claims.yaml` is staged.
+* `receipt-required-for-math-content` — invokes
+  `scripts/math-first/require_math_evidence.py`. If a commit touches a
+  math-track surface (`0-Core-Formalism/lean/Semantics/`,
+  `6-Documentation/docs/distilled/`,
+  `shared-data/data/stack_solidification/`), the same commit must also touch
+  a math-evidence surface (a DeepSeek receipt, a Lean kernel, or
+  `claims.yaml`).
+
+### Install
+
+```bash
+uv tool install pre-commit          # one-time, per machine
+pre-commit install                  # one-time, per clone
+pre-commit run --all-files          # smoke-test
+```
+
+## CI Workflow
+
+[`.github/workflows/math-check.yml`](../.github/workflows/math-check.yml)
+runs on every PR and on pushes to `main` or `distilled` that touch a
+math-first surface. It has three jobs:
+
+1. **`validate-schemas`** — compiles every schema under
+   `shared-data/schemas/`, validates every tracked DeepSeek receipt, runs the
+   validator's own self-tests, validates `claims.yaml`, and finally re-runs
+   the canonical emitter in `--verify-only` mode against every receipt to
+   re-check `answer_sha256` against the answer file bytes on disk. This is
+   the AGENTS.md contract for promoted Ollama/DeepSeek review receipts.
+2. **`require-evidence`** — runs only on PRs and invokes
+   `scripts/math-first/require_math_evidence.py --from-git-diff
+   origin/<base>` to enforce the same evidence rule at PR scope that the
+   pre-commit hook enforces at commit scope.
+3. **`pre-commit`** — runs every pre-commit hook against the PR's range of
+   changed files (`pre-commit run --from-ref <base> --to-ref HEAD`), so the
+   guardrails are honoured even when a contributor has not installed the
+   hooks locally.
+
+The pre-existing `wolfram-verification.yml` workflow continues to police
+mathematical formulas inside Lean source for missing Wolfram Alpha
+verification comments; nothing here replaces it.
+
+## MCP Servers for AI-Assisted Math
+
+[`.mcp.json`](../.mcp.json) declares the math-first tool surface that
+Claude Desktop, Devin, and other MCP-aware clients should advertise when
+working in this repo. Each server is intentionally **gated on a runtime
+environment variable**, so the config itself never carries secrets and
+contributors who have not provisioned a backend simply skip it.
+
+| Server | Purpose | Runtime requirement |
+|--------|---------|---------------------|
+| `filesystem` | Read/write proof artifacts, Lean kernels, receipts. | `npx`, scope pinned to repo root. |
+| `sympy` | Local SymPy bridge for symbolic verification of arithmetic claims. | `uv tool run sympy-mcp` (`sympy-mcp` upstream). |
+| `wolfram-alpha` | Wolfram Alpha verification for the formulas policed by `wolfram-verification.yml`. | `WOLFRAM_ALPHA_APPID`. |
+| `lean` | Lean 4 / Mathlib typecheck bridge against `0-Core-Formalism/lean/Semantics/lakefile.toml`. | `elan` on PATH with `leanprover/lean4:v4.30.0-rc2`. |
+| DeepSeek review | Use `5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py` directly; no MCP server is currently advertised for it. | `OLLAMA_API_KEY` for non-local endpoints. |
+
+To use these from Claude Desktop, point its `claude_desktop_config.json` at
+the repo root or copy the relevant entries verbatim. Secrets live in the
+shell/env, never in the config.
+
+## Workflow: adding a new claim
+
+1. Land the natural-language claim in `claims.yaml` with `status: conjecture`.
+2. Produce a DeepSeek review via the canonical emitter. Commit both the
+   answer markdown and `*.receipt.json`; promote `status` to
+   `verified-by-ai` in the same commit. The pre-commit `require-evidence`
+   gate now finds a receipt alongside any math-track edit, and the schema
+   validator confirms the receipt parses.
+3. When a Lean proof lands under `0-Core-Formalism/lean/Semantics/`, promote
+   `status` to `formally-proven` and set `lean:` to the proof's source path.
+4. On external publication, promote `status` to `published` and add the
+   citation to `sources:`.
+
+## Workflow: editing a math-track file
+
+The math-first surfaces are:
+
+* `0-Core-Formalism/lean/Semantics/...`
+* `6-Documentation/docs/distilled/...`
+* `shared-data/data/stack_solidification/...`
+
+Any commit touching one of these surfaces must, in the same commit, touch
+one of:
+
+* `shared-data/artifacts/deepseek_review/...` (new receipt + answer file)
+* `0-Core-Formalism/lean/Semantics/...` (Lean change in the same commit
+  counts as evidence — Lean is the source of truth)
+* `claims.yaml` (registry update)
+
+The pre-commit hook and CI both enforce this. To bypass intentionally — for
+example, a typo fix in a distilled doc with no semantic change — commit with
+`git commit --no-verify` and explain the bypass in the PR description; CI
+will still flag the PR and the maintainer can apply the
+`math-first-exempt` label (one-off override).
+
+## Verifying everything in one shot
+
+```bash
+# Schemas + receipts + claims + emitter --verify-only
+uv run --python 3.11 \
+  --with "jsonschema>=4.21" --with "rfc3339-validator" --with "PyYAML" \
+  bash -c '
+    python3 scripts/math-first/validate_deepseek_receipts.py \
+      && python3 scripts/math-first/test_validate_deepseek_receipts.py \
+      && python3 scripts/math-first/validate_claims_registry.py \
+      && for r in shared-data/artifacts/deepseek_review/*.receipt.json; do \
+           python3 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py --verify-only "$r"; \
+         done
+  '
+```
+
+If any of the above fails, the corresponding PR will not merge.

scripts/math-first/require_math_evidence.py

@@ -0,0 +1,146 @@
+#!/usr/bin/env python3
+"""Require math evidence alongside math-track edits.
+
+When a commit (or PR) touches files under one of the math-track surfaces,
+this script asserts that at least one file under a math-evidence surface is
+also part of the same change set. The two surfaces are configurable -- the
+defaults below match ``docs/math-first-tooling.md`` and the pre-commit hook
+declared in ``.pre-commit-config.yaml``.
+
+Math-track surfaces (need evidence):
+  - 0-Core-Formalism/lean/Semantics/...
+  - 6-Documentation/docs/distilled/...
+  - shared-data/data/stack_solidification/...
+
+Math-evidence surfaces (accepted as evidence):
+  - shared-data/artifacts/deepseek_review/*.receipt.json
+  - 0-Core-Formalism/lean/Semantics/...   (a Lean change in the same commit
+                                            counts because Lean is the source
+                                            of truth per AGENTS.md)
+  - claims.yaml                            (registry update)
+
+Usage:
+    scripts/math-first/require_math_evidence.py [FILES ...]
+    scripts/math-first/require_math_evidence.py --from-git-diff BASE_REF
+
+If neither files nor ``--from-git-diff`` is supplied the script exits 0 with
+a noop. Pre-commit invokes it with the staged file list, CI invokes it with
+``--from-git-diff origin/<base>``.
+
+Exit code:
+    0  evidence present, nothing to do, or no math-track files changed.
+    1  math-track files changed without accompanying evidence.
+"""
+from __future__ import annotations
+
+import argparse
+import subprocess
+import sys
+from pathlib import Path
+
+REPO_ROOT = Path(__file__).resolve().parents[2]
+
+MATH_TRACK_PREFIXES: tuple[str, ...] = (
+    "0-Core-Formalism/lean/Semantics/",
+    "6-Documentation/docs/distilled/",
+    "shared-data/data/stack_solidification/",
+)
+
+EVIDENCE_PREFIXES: tuple[str, ...] = (
+    "shared-data/artifacts/deepseek_review/",
+    "0-Core-Formalism/lean/Semantics/",
+)
+
+EVIDENCE_FILES: tuple[str, ...] = (
+    "claims.yaml",
+)
+
+
+def _normalise(path: str) -> str:
+    return path.replace("\\", "/")
+
+
+def _is_math_track(path: str) -> bool:
+    norm = _normalise(path)
+    return any(norm.startswith(prefix) for prefix in MATH_TRACK_PREFIXES)
+
+
+def _is_evidence(path: str) -> bool:
+    norm = _normalise(path)
+    if norm in EVIDENCE_FILES:
+        return True
+    if any(norm.startswith(prefix) for prefix in EVIDENCE_PREFIXES):
+        # A *new or updated* receipt counts. A bare Lean kernel edit also
+        # counts because Lean is treated as the source of truth -- the change
+        # itself is the evidence.
+        if norm.startswith("shared-data/artifacts/deepseek_review/"):
+            return norm.endswith(".receipt.json") or norm.endswith(".md")
+        return True
+    return False
+
+
+def _files_from_git_diff(base_ref: str) -> list[str]:
+    cmd = ["git", "diff", "--name-only", f"{base_ref}...HEAD"]
+    try:
+        result = subprocess.run(cmd, capture_output=True, text=True, check=True, cwd=REPO_ROOT)
+    except subprocess.CalledProcessError as exc:
+        print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr)
+        raise SystemExit(2)
+    return [line.strip() for line in result.stdout.splitlines() if line.strip()]
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument(
+        "files",
+        nargs="*",
+        help="Explicit list of files to check (typically supplied by pre-commit).",
+    )
+    parser.add_argument(
+        "--from-git-diff",
+        metavar="BASE_REF",
+        help="Compute the file list from `git diff --name-only BASE_REF...HEAD`.",
+    )
+    args = parser.parse_args(argv)
+
+    if args.from_git_diff:
+        files = _files_from_git_diff(args.from_git_diff)
+    else:
+        files = list(args.files)
+
+    if not files:
+        return 0
+
+    math_track = sorted({f for f in files if _is_math_track(f)})
+    evidence = sorted({f for f in files if _is_evidence(f)})
+
+    if not math_track:
+        return 0
+
+    if evidence:
+        print("math-evidence check: OK")
+        print("  math-track files:")
+        for path in math_track:
+            print(f"    - {path}")
+        print("  evidence files:")
+        for path in evidence:
+            print(f"    - {path}")
+        return 0
+
+    print("math-evidence check: FAIL", file=sys.stderr)
+    print("  math-track files changed without accompanying evidence:", file=sys.stderr)
+    for path in math_track:
+        print(f"    - {path}", file=sys.stderr)
+    print(
+        "\n  Add at least one of:\n"
+        "    - a DeepSeek review receipt under shared-data/artifacts/deepseek_review/\n"
+        "    - a Lean change under 0-Core-Formalism/lean/Semantics/\n"
+        "    - a claims.yaml update\n"
+        "  See docs/math-first-tooling.md.",
+        file=sys.stderr,
+    )
+    return 1
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/math-first/test_validate_deepseek_receipts.py

@@ -0,0 +1,134 @@
+#!/usr/bin/env python3
+"""Self-checks for ``validate_deepseek_receipts.py``.
+
+Run with::
+
+    uv run --python 3.11 --with "jsonschema>=4.21" --with "rfc3339-validator" \
+        python3 scripts/math-first/test_validate_deepseek_receipts.py
+
+The test builds positive and negative receipt fixtures in a temporary
+directory, invokes the validator as a subprocess, and asserts the exit code
+matches the expected outcome. The fixtures are derived from
+``shared-data/artifacts/deepseek_review/`` so they exercise the same shape
+that ships in the repo.
+"""
+from __future__ import annotations
+
+import json
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+REPO_ROOT = Path(__file__).resolve().parents[2]
+VALIDATOR = REPO_ROOT / "scripts" / "math-first" / "validate_deepseek_receipts.py"
+
+GOOD_PRIMARY = {
+    "schema": "ollama_deepseek_review_receipt_v1",
+    "created_at": "2026-05-12T03:35:51+00:00",
+    "model": "deepseek-v3.2",
+    "endpoint": "https://ollama.com/v1/chat/completions",
+    "prompt_sha256": "sha256:" + "a" * 64,
+    "answer_sha256": "sha256:" + "b" * 64,
+    "usage": {"prompt_tokens": 1, "completion_tokens": 1, "total_tokens": 2},
+    "context_files": ["docs/example.md"],
+    "answer_path": "shared-data/artifacts/deepseek_review/example.md",
+}
+
+GOOD_CONTINUATION = {
+    "schema": "ollama_deepseek_review_continuation_receipt_v1",
+    "created_at": "2026-05-12T03:38:49+00:00",
+    "model": "deepseek-v4-flash",
+    "endpoint": "https://ollama.com/v1/chat/completions",
+    "prompt_sha256": "sha256:" + "c" * 64,
+    "answer_sha256": "sha256:" + "d" * 64,
+    "usage": {"prompt_tokens": 1, "completion_tokens": 1, "total_tokens": 2},
+    "previous_answer_path": "shared-data/artifacts/deepseek_review/example.md",
+    "answer_path": "shared-data/artifacts/deepseek_review/example_continuation.md",
+    "message_keys": ["role", "content", "reasoning"],
+}
+
+
+def _write(tmp: Path, name: str, payload: dict | str) -> Path:
+    path = tmp / name
+    if isinstance(payload, str):
+        path.write_text(payload, encoding="utf-8")
+    else:
+        path.write_text(json.dumps(payload), encoding="utf-8")
+    return path
+
+
+def _run(path: Path) -> subprocess.CompletedProcess[str]:
+    return subprocess.run(
+        [sys.executable, str(VALIDATOR), str(path)],
+        capture_output=True,
+        text=True,
+        check=False,
+    )
+
+
+def main() -> int:
+    failures: list[str] = []
+
+    with tempfile.TemporaryDirectory() as raw:
+        tmp = Path(raw)
+
+        cases: list[tuple[str, dict | str, int]] = [
+            ("good_primary.receipt.json", GOOD_PRIMARY, 0),
+            ("good_continuation.receipt.json", GOOD_CONTINUATION, 0),
+            (
+                "bad_sha256.receipt.json",
+                {**GOOD_PRIMARY, "prompt_sha256": "not-a-hash"},
+                1,
+            ),
+            (
+                "bad_schema_id.receipt.json",
+                {**GOOD_PRIMARY, "schema": "made_up_schema_id"},
+                1,
+            ),
+            (
+                "bad_missing_usage.receipt.json",
+                {k: v for k, v in GOOD_PRIMARY.items() if k != "usage"},
+                1,
+            ),
+            (
+                "bad_negative_tokens.receipt.json",
+                {**GOOD_PRIMARY, "usage": {"prompt_tokens": -1, "completion_tokens": 1, "total_tokens": 0}},
+                1,
+            ),
+            (
+                "bad_answer_path_ext.receipt.json",
+                {**GOOD_PRIMARY, "answer_path": "shared-data/artifacts/deepseek_review/example.txt"},
+                1,
+            ),
+            (
+                "bad_extra_field.receipt.json",
+                {**GOOD_PRIMARY, "stray": 1},
+                1,
+            ),
+            ("bad_not_json.receipt.json", "{not json}", 1),
+        ]
+
+        for name, payload, expected in cases:
+            path = _write(tmp, name, payload)
+            result = _run(path)
+            if result.returncode != expected:
+                failures.append(
+                    f"{name}: expected exit {expected}, got {result.returncode}\n"
+                    f"  stdout: {result.stdout.strip()}\n"
+                    f"  stderr: {result.stderr.strip()}"
+                )
+            else:
+                print(f"OK   {name} (exit {result.returncode})")
+
+    if failures:
+        print("\nFailures:")
+        for line in failures:
+            print(line)
+        return 1
+    print("\nAll validator self-checks passed.")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/math-first/validate_claims_registry.py

@@ -0,0 +1,178 @@
+#!/usr/bin/env python3
+"""Validate ``claims.yaml`` against the claims-registry JSON Schema.
+
+Usage:
+    scripts/math-first/validate_claims_registry.py [PATH]
+
+When no PATH is provided, the registry at the repo root (``claims.yaml``) is
+validated. The script enforces:
+
+  * the YAML parses and conforms to
+    ``shared-data/schemas/claims-registry.schema.json``;
+  * every ``id`` is unique across the registry;
+  * every repo-relative path referenced from ``lean``, ``review_receipts``,
+    and ``sources`` resolves to a tracked file on disk (external citations
+    that do not look like repo paths -- e.g. ``http`` URLs, ``arXiv:...`` --
+    are skipped).
+
+Exit code:
+    0  registry valid.
+    1  registry invalid (schema, duplicate id, or missing referenced file).
+    2  schema malformed, dependencies missing, or registry file not found.
+
+See ``docs/math-first-tooling.md`` for the math-first tooling contract.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+import re
+import sys
+from pathlib import Path
+from typing import Any
+
+REPO_ROOT = Path(__file__).resolve().parents[2]
+SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "claims-registry.schema.json"
+DEFAULT_REGISTRY = REPO_ROOT / "claims.yaml"
+
+# Anything matching one of these prefixes is treated as an external citation
+# rather than a repo-relative path, and is therefore not required to resolve
+# to a file on disk.
+_EXTERNAL_PREFIXES = ("http://", "https://", "arXiv:", "arxiv:", "doi:", "DOI:")
+_EXTERNAL_RE = re.compile(r"^[A-Za-z]+:")
+
+
+def _load_schema(schema_path: Path) -> dict[str, Any]:
+    try:
+        from jsonschema import Draft202012Validator
+    except ImportError as exc:
+        print(
+            "error: jsonschema>=4.18 is required (Draft 2020-12). "
+            "Install via `uv pip install jsonschema>=4.21 PyYAML`.",
+            file=sys.stderr,
+        )
+        raise SystemExit(2) from exc
+
+    try:
+        schema = json.loads(schema_path.read_text(encoding="utf-8"))
+    except FileNotFoundError:
+        print(f"error: schema not found at {schema_path}", file=sys.stderr)
+        raise SystemExit(2)
+    except json.JSONDecodeError as exc:
+        print(f"error: schema {schema_path} is not valid JSON: {exc}", file=sys.stderr)
+        raise SystemExit(2)
+
+    Draft202012Validator.check_schema(schema)
+    return schema
+
+
+def _load_registry(registry_path: Path) -> dict[str, Any]:
+    try:
+        import yaml
+    except ImportError as exc:
+        print(
+            "error: PyYAML is required. Install via `uv pip install PyYAML`.",
+            file=sys.stderr,
+        )
+        raise SystemExit(2) from exc
+
+    try:
+        text = registry_path.read_text(encoding="utf-8")
+    except FileNotFoundError:
+        print(f"error: registry not found at {registry_path}", file=sys.stderr)
+        raise SystemExit(2)
+
+    data = yaml.safe_load(text)
+    if not isinstance(data, dict):
+        print(f"error: registry {registry_path} did not parse as a mapping", file=sys.stderr)
+        raise SystemExit(1)
+    return data
+
+
+def _is_external(reference: str) -> bool:
+    if reference.startswith(_EXTERNAL_PREFIXES):
+        return True
+    return bool(_EXTERNAL_RE.match(reference))
+
+
+def _check_path(reference: str) -> tuple[bool, str]:
+    if _is_external(reference):
+        return True, ""
+    if reference.startswith("/"):
+        return False, "must be repo-relative (no leading '/')"
+    candidate = REPO_ROOT / reference
+    if not candidate.exists():
+        return False, f"path does not exist on disk: {reference}"
+    return True, ""
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument(
+        "path",
+        nargs="?",
+        type=Path,
+        default=DEFAULT_REGISTRY,
+        help=f"Registry file to validate (default: {DEFAULT_REGISTRY.relative_to(REPO_ROOT)}).",
+    )
+    parser.add_argument(
+        "--schema",
+        type=Path,
+        default=SCHEMA_PATH,
+        help=f"Path to the JSON Schema (default: {SCHEMA_PATH.relative_to(REPO_ROOT)}).",
+    )
+    args = parser.parse_args(argv)
+
+    schema = _load_schema(args.schema)
+    registry = _load_registry(args.path)
+
+    from jsonschema import Draft202012Validator
+
+    validator = Draft202012Validator(schema)
+    errors = sorted(validator.iter_errors(registry), key=lambda e: list(e.absolute_path))
+    if errors:
+        print(f"FAIL {args.path}")
+        for err in errors:
+            location = "/".join(str(p) for p in err.absolute_path) or "<root>"
+            print(f"  - {location}: {err.message}")
+        return 1
+
+    failures: list[str] = []
+    seen_ids: dict[str, int] = {}
+    for index, entry in enumerate(registry.get("claims", [])):
+        cid = entry.get("id", f"<index {index}>")
+        if cid in seen_ids:
+            failures.append(
+                f"duplicate id '{cid}' (also defined at index {seen_ids[cid]})"
+            )
+        seen_ids[cid] = index
+
+        for key in ("lean",):
+            value = entry.get(key)
+            if not value:
+                continue
+            # Lean entries may be either a file path or a theorem symbol; only
+            # validate the file path form, which contains a `/` or ends in `.lean`.
+            if "/" in value or value.endswith(".lean"):
+                ok, msg = _check_path(value)
+                if not ok:
+                    failures.append(f"claim '{cid}': {key}: {msg}")
+
+        for key in ("review_receipts", "sources"):
+            for value in entry.get(key, []) or []:
+                ok, msg = _check_path(value)
+                if not ok:
+                    failures.append(f"claim '{cid}': {key}: {msg}")
+
+    if failures:
+        print(f"FAIL {args.path}")
+        for line in failures:
+            print(f"  - {line}")
+        return 1
+
+    print(f"OK   {args.path} ({len(registry.get('claims', []))} claim(s))")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/math-first/validate_deepseek_receipts.py

@@ -0,0 +1,136 @@
+#!/usr/bin/env python3
+"""Validate DeepSeek review receipts against the repo JSON Schema.
+
+Usage:
+    scripts/math-first/validate_deepseek_receipts.py [PATH ...]
+
+When no PATH is provided, every tracked ``*.receipt.json`` under
+``shared-data/artifacts/deepseek_review/`` is validated. Otherwise the named
+paths are validated directly (files are checked as receipts; directories are
+walked for ``*.receipt.json``).
+
+Exit code:
+    0  every receipt validates against
+       ``shared-data/schemas/deepseek-review-receipt.schema.json``.
+    1  one or more receipts failed schema validation.
+    2  the schema itself is malformed or ``jsonschema`` is missing.
+
+This script is the single source of truth shared by the pre-commit hook in
+``.pre-commit-config.yaml`` and the ``math-check`` GitHub Actions workflow in
+``.github/workflows/math-check.yml``. See ``docs/math-first-tooling.md`` for
+the math-first tooling contract.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+import sys
+from pathlib import Path
+from typing import Iterable, Iterator
+
+REPO_ROOT = Path(__file__).resolve().parents[2]
+SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "deepseek-review-receipt.schema.json"
+DEFAULT_ROOT = REPO_ROOT / "shared-data" / "artifacts" / "deepseek_review"
+RECEIPT_SUFFIX = ".receipt.json"
+
+
+def _iter_receipts(paths: Iterable[Path]) -> Iterator[Path]:
+    for path in paths:
+        if path.is_dir():
+            yield from sorted(p for p in path.rglob(f"*{RECEIPT_SUFFIX}") if p.is_file())
+        elif path.is_file():
+            yield path
+        else:
+            print(f"warning: skipping missing path {path}", file=sys.stderr)
+
+
+def _load_validator(schema_path: Path):
+    try:
+        from jsonschema import Draft202012Validator, FormatChecker
+    except ImportError as exc:
+        print(
+            "error: jsonschema>=4.18 is required (Draft 2020-12). "
+            "Install via `uv pip install jsonschema>=4.21 rfc3339-validator`.",
+            file=sys.stderr,
+        )
+        raise SystemExit(2) from exc
+
+    try:
+        schema = json.loads(schema_path.read_text(encoding="utf-8"))
+    except FileNotFoundError:
+        print(f"error: schema not found at {schema_path}", file=sys.stderr)
+        raise SystemExit(2)
+    except json.JSONDecodeError as exc:
+        print(f"error: schema {schema_path} is not valid JSON: {exc}", file=sys.stderr)
+        raise SystemExit(2)
+
+    try:
+        Draft202012Validator.check_schema(schema)
+    except Exception as exc:  # noqa: BLE001 - surface schema errors verbatim
+        print(f"error: schema {schema_path} is invalid: {exc}", file=sys.stderr)
+        raise SystemExit(2)
+
+    return Draft202012Validator(schema, format_checker=FormatChecker())
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument(
+        "paths",
+        nargs="*",
+        type=Path,
+        help="Receipt files or directories. Defaults to the tracked review artifact root.",
+    )
+    parser.add_argument(
+        "--schema",
+        type=Path,
+        default=SCHEMA_PATH,
+        help=f"Path to the JSON Schema (default: {SCHEMA_PATH.relative_to(REPO_ROOT)}).",
+    )
+    args = parser.parse_args(argv)
+
+    validator = _load_validator(args.schema)
+
+    if args.paths:
+        candidates = list(_iter_receipts(args.paths))
+    elif DEFAULT_ROOT.exists():
+        candidates = list(_iter_receipts([DEFAULT_ROOT]))
+    else:
+        candidates = []
+
+    receipts = [p for p in candidates if p.name.endswith(RECEIPT_SUFFIX)]
+    skipped = [p for p in candidates if not p.name.endswith(RECEIPT_SUFFIX)]
+    for path in skipped:
+        print(f"skip: {path} (not a *{RECEIPT_SUFFIX} file)")
+
+    if not receipts:
+        print("no DeepSeek review receipts to validate")
+        return 0
+
+    failed = 0
+    for path in receipts:
+        try:
+            data = json.loads(path.read_text(encoding="utf-8"))
+        except json.JSONDecodeError as exc:
+            print(f"FAIL {path}: invalid JSON ({exc})")
+            failed += 1
+            continue
+
+        errors = sorted(validator.iter_errors(data), key=lambda e: list(e.absolute_path))
+        if errors:
+            print(f"FAIL {path}")
+            for err in errors:
+                location = "/".join(str(p) for p in err.absolute_path) or "<root>"
+                print(f"  - {location}: {err.message}")
+            failed += 1
+        else:
+            print(f"OK   {path}")
+
+    if failed:
+        print(f"\n{failed} receipt(s) failed validation", file=sys.stderr)
+        return 1
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

shared-data/schemas/claims-registry.schema.json

@@ -0,0 +1,82 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://github.com/allaunthefox/Research-Stack/shared-data/schemas/claims-registry.schema.json",
+  "title": "Research Stack Mathematical Claim Registry",
+  "description": "Schema for claims.yaml at the repo root. Tracks the rigor level of every mathematical claim the stack stands behind, plus the Lean proof and/or DeepSeek review receipts that back it. See docs/math-first-tooling.md.",
+  "type": "object",
+  "required": ["claims"],
+  "additionalProperties": false,
+  "properties": {
+    "claims": {
+      "type": "array",
+      "minItems": 1,
+      "items": { "$ref": "#/$defs/claim" }
+    }
+  },
+  "$defs": {
+    "claim": {
+      "type": "object",
+      "required": ["id", "title", "status"],
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "string",
+          "pattern": "^[a-z0-9][a-z0-9-]*$",
+          "description": "Stable kebab-case slug. Must remain unique across the registry."
+        },
+        "title": {
+          "type": "string",
+          "minLength": 1,
+          "description": "One-line natural-language statement of the claim."
+        },
+        "status": {
+          "type": "string",
+          "enum": ["conjecture", "verified-by-ai", "formally-proven", "published"],
+          "description": "Current rigor level for the claim."
+        },
+        "lean": {
+          "type": "string",
+          "minLength": 1,
+          "description": "Optional repo-relative Lean source file or `theorem` symbol carrying the proof obligation."
+        },
+        "review_receipts": {
+          "type": "array",
+          "uniqueItems": true,
+          "items": {
+            "type": "string",
+            "pattern": "\\.receipt\\.json$",
+            "description": "Repo-relative path to a DeepSeek review receipt."
+          }
+        },
+        "sources": {
+          "type": "array",
+          "uniqueItems": true,
+          "items": {
+            "type": "string",
+            "minLength": 1,
+            "description": "Repo-relative path or external citation supporting the claim."
+          }
+        },
+        "notes": {
+          "type": "string",
+          "description": "Free-form context. Keep short."
+        }
+      },
+      "allOf": [
+        {
+          "if": { "properties": { "status": { "const": "verified-by-ai" } } },
+          "then": {
+            "required": ["review_receipts"],
+            "properties": {
+              "review_receipts": { "minItems": 1 }
+            }
+          }
+        },
+        {
+          "if": { "properties": { "status": { "const": "formally-proven" } } },
+          "then": { "required": ["lean"] }
+        }
+      ]
+    }
+  }
+}

shared-data/schemas/deepseek-review-receipt.schema.json

@@ -0,0 +1,134 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://github.com/allaunthefox/Research-Stack/shared-data/schemas/deepseek-review-receipt.schema.json",
+  "title": "DeepSeek Review Receipt",
+  "description": "Schema for Ollama-compatible DeepSeek review receipts emitted by 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py. Receipts are paired with a sibling markdown answer file and pin the exact model, endpoint, token usage, and SHA-256 hashes needed to re-validate the review without re-running the model. See 6-Documentation/wiki/DeepSeek-Review-Process.md for the human-readable contract.",
+  "type": "object",
+  "oneOf": [
+    { "$ref": "#/$defs/primaryReceipt" },
+    { "$ref": "#/$defs/continuationReceipt" }
+  ],
+  "$defs": {
+    "sha256Hash": {
+      "type": "string",
+      "pattern": "^sha256:[0-9a-f]{64}$",
+      "description": "Lowercase hex SHA-256 digest prefixed with the literal 'sha256:'."
+    },
+    "isoTimestamp": {
+      "type": "string",
+      "format": "date-time",
+      "description": "ISO-8601 UTC timestamp (e.g. 2026-05-12T03:35:51+00:00)."
+    },
+    "endpoint": {
+      "type": "string",
+      "format": "uri",
+      "description": "API endpoint that served the review (e.g. https://ollama.com/v1/chat/completions)."
+    },
+    "model": {
+      "type": "string",
+      "minLength": 1,
+      "description": "Model identifier (e.g. deepseek-v3.2, deepseek-v4-flash)."
+    },
+    "repoRelativePath": {
+      "type": "string",
+      "minLength": 1,
+      "pattern": "^[^/].*",
+      "description": "Repo-relative POSIX path (must not start with '/')."
+    },
+    "usage": {
+      "type": "object",
+      "description": "Token usage as reported by the endpoint.",
+      "required": ["prompt_tokens", "completion_tokens", "total_tokens"],
+      "additionalProperties": false,
+      "properties": {
+        "prompt_tokens": { "type": "integer", "minimum": 0 },
+        "completion_tokens": { "type": "integer", "minimum": 0 },
+        "total_tokens": { "type": "integer", "minimum": 0 }
+      }
+    },
+    "primaryReceipt": {
+      "type": "object",
+      "description": "Primary review receipt: written first, pins context files used to build the prompt.",
+      "required": [
+        "schema",
+        "created_at",
+        "model",
+        "endpoint",
+        "prompt_sha256",
+        "answer_sha256",
+        "usage",
+        "context_files",
+        "answer_path"
+      ],
+      "additionalProperties": false,
+      "properties": {
+        "schema": { "const": "ollama_deepseek_review_receipt_v1" },
+        "created_at": { "$ref": "#/$defs/isoTimestamp" },
+        "model": { "$ref": "#/$defs/model" },
+        "endpoint": { "$ref": "#/$defs/endpoint" },
+        "prompt_sha256": { "$ref": "#/$defs/sha256Hash" },
+        "answer_sha256": { "$ref": "#/$defs/sha256Hash" },
+        "usage": { "$ref": "#/$defs/usage" },
+        "context_files": {
+          "type": "array",
+          "minItems": 1,
+          "uniqueItems": true,
+          "items": { "$ref": "#/$defs/repoRelativePath" },
+          "description": "Repo-relative paths to every file that participated in the review prompt context."
+        },
+        "answer_path": {
+          "allOf": [
+            { "$ref": "#/$defs/repoRelativePath" },
+            { "pattern": "\\.md$" }
+          ],
+          "description": "Repo-relative path to the answer markdown."
+        }
+      }
+    },
+    "continuationReceipt": {
+      "type": "object",
+      "description": "Continuation receipt: emitted when a primary review was truncated and was continued by a separate request.",
+      "required": [
+        "schema",
+        "created_at",
+        "model",
+        "endpoint",
+        "prompt_sha256",
+        "answer_sha256",
+        "usage",
+        "previous_answer_path",
+        "answer_path"
+      ],
+      "additionalProperties": false,
+      "properties": {
+        "schema": { "const": "ollama_deepseek_review_continuation_receipt_v1" },
+        "created_at": { "$ref": "#/$defs/isoTimestamp" },
+        "model": { "$ref": "#/$defs/model" },
+        "endpoint": { "$ref": "#/$defs/endpoint" },
+        "prompt_sha256": { "$ref": "#/$defs/sha256Hash" },
+        "answer_sha256": { "$ref": "#/$defs/sha256Hash" },
+        "usage": { "$ref": "#/$defs/usage" },
+        "previous_answer_path": {
+          "allOf": [
+            { "$ref": "#/$defs/repoRelativePath" },
+            { "pattern": "\\.md$" }
+          ],
+          "description": "Repo-relative path to the answer being continued."
+        },
+        "answer_path": {
+          "allOf": [
+            { "$ref": "#/$defs/repoRelativePath" },
+            { "pattern": "\\.md$" }
+          ],
+          "description": "Repo-relative path to the answer markdown produced by this continuation."
+        },
+        "message_keys": {
+          "type": "array",
+          "uniqueItems": true,
+          "items": { "type": "string", "minLength": 1 },
+          "description": "Field names returned alongside 'content' by the continuation endpoint (e.g. role, content, reasoning)."
+        }
+      }
+    }
+  }
+}