Proof & Derivation Forensics — does the written proof hold?

Audit family G (proof & derivation integrity) for: $ARGUMENTS (requires claims.json from /evidence-ledger). A fresh cross-model reviewer reads each theorem/proof and proposes span-anchored findings; this skill writes proof-derivation-forensics.findings.json. The deterministic adjudicator — not this skill — computes the verdict.

🔒 Do not wrap this skill in /loop, /schedule, or CronCreate. It is verdict-bearing input — it proposes the findings the deterministic adjudicator turns into the report. Re-firing it on a wall-clock timer adds no signal: its output changes only when the paper / ledger changes, not with the clock. Schedule the external wait that precedes it — ledger built → audit once. (Mirrors ARIS's external-cadence doctrine.)

Broken math is the single most-cited "obviously machine-written" tell in real reviews ("过不去的步骤用文字糊弄", "车轱辘话复述当证明", "关键公式符号用反"). Unlike the surface signals of family F, family-G flaws are substantive and can be critical: a theorem whose proof is circular, skips a load-bearing obligation, or takes an invalid step does not support its claim. And — crucially — proof validity is decidable from the written proof: we never need the code or results, so family G is verdict-bearing at L1 (the LaTeX source) and can still reach HARD_FLAGS with no repo — but needs that source, because PDF-extracted math is unreliable; at an L0 (PDF-only) run a family-G flaw surfaces as info only. Adapted from ARIS proof-checker (per-obligation ledger + 20-category taxonomy + counterexample red team) and formula-derivation (identity/proposition/approximation/interpretation step typing), reframed from "fix my own proof" to "audit a third party's proof, detect-only." There is no fixing here and no authorship verdict — only "the step shown does not hold," with the exact line quoted.

Why this exists

An autoresearch pipeline (or a rushed human) writes a theorem statement, then a proof, then an abstract that advertises the theorem — in separate passes, never reconciled at the level of the argument. The result is a proof that does not establish its own claim:

• "By compactness a maximizer exists" — but compactness of the domain is never shown (a missing existence obligation invoked as fact);
• "Lemma 3 follows from Theorem 1," whose proof in turn invokes Lemma 3 (circular);
• "By Jensen, $\mathbb{E}[f(X)] \ge f(\mathbb{E}[X])$" for a concave $f$ — the inequality runs the wrong way (an invalid step);
• the definition fixes $\le$, but equation (7) and the proof use $\ge$; or argmin in Def 2 becomes argmax in the proof of Thm 4 (a symbol's meaning drifts);
• a concentration bound uses independence of the $X_i$, but the theorem only assumes they are identically distributed (a stronger assumption smuggled in).

None of this needs the code, the data, or any external fact to detect — only the proof, read against the obligations its own theorem creates. That is why family G is substantive and decided from the written proof (verdict-bearing at L1): a senior area chair reads a proof and decides validity from the page; this tool needs the LaTeX source (L1) to do it reliably, since PDF-extracted math is unreliable — at an L0 PDF-only run it surfaces info only. So does this skill — via a cross-model reviewer, with every finding anchored to a verbatim ledger span and the verdict computed by deterministic code.

Honest recall bound (read this). The evidence ledger (build_claim_ledger.py) has no dedicated theorem/proof/equation extractor: proof text enters claims.json only as the number, scope, citation, caption, and table_cell spans that happen to overlap it (a bound with a constant, a "for all / general" sentence, a \cite{} to an imported result, an equation paragraph carrying a decimal). The reviewer judges from the full proof source, but every finding must anchor to a ledger claim whose text_span verbatim-contains the failing fragment. A pure-symbol step covered by no such claim cannot rise above info — that is the honest outcome, not a defect. Recall is materially higher at L1 (LaTeX: equation paragraphs and theorem-statement sentences are captured with stable line numbers) than at L0 (PDF text). Step 1 pre-computes, per theorem, the exact anchor-candidate claim_ids so the reviewer knows where it can and cannot ground a finding.

Core principle

Ledger-anchored, span-verified, decide-from-the-written-proof, reviewer≠adjudicator. There is no deterministic tool for family G (no arithmetic backbone like consistency-audit's check_numeric_consistency.py) — proof validity is a semantic judgment. So this skill runs exactly one substantive pass:

• a fresh cross-model reviewer pass that reads each theorem + its proof + an extraction-only obligation scaffold (Step 1) and proposes one finding per undischarged obligation / invalid step / drift / smuggle / circularity.

Every above-info finding conforms to schemas/finding.schema.json and cites a ledger claim_id + a verbatim span (references/integrity-forensics-contract.md rules 1–2). The model proposes; tools/adjudicate_findings.py decides (references/reviewer-independence.md Layer 2). This skill computes no verdict, and never edits the audited paper. We never write "fabricated" or "faked" — we write, with the line quoted, the step shown does not hold / the obligation is not discharged / the symbol's meaning drifted.

How this differs from the other auditors (route correctly)

Auditor	Question it answers	Level
proof-derivation-forensics (this)	Does the WRITTEN proof/derivation actually establish its theorem? (gap / circularity / invalid step / symbol drift / smuggled assumption)	L1 — from the written math (LaTeX source), no external lookup
consistency-audit	Does the paper contradict ITSELF (numbers, scope, method)? incl. abstract-general-vs-theorem-narrow (HP-THEOREM-SCOPE-DRIFT)	L0
citation-forensics	Does a cited theorem EXIST and is it cited in a context it supports?	L0
experiment-forensics	Are reported numbers what the code actually computes? (fake GT, self-norm, phantom)	L2
baseline-comparison-audit	Are the right baselines present, tuned, and is "SOTA" earned?	L0 stated / L2 verified
adversarial-case-builder	Strongest evidence-bound rejection memo (no verdict weight)	any

Do NOT raise here (hand off instead):

• abstract/title advertises generality the theorem statement doesn't have → consistency-audit owns HP-THEOREM-SCOPE-DRIFT; the headline framing goes to adversarial-case-builder. This skill owns the proof-internal twin: the proof uses an assumption the theorem statement never lists (HP-ASSUMPTION-SMUGGLE).
• whether a cited result exists or is cited in the right context → citation-forensics. This skill owns the proof-internal twin: a cited theorem is applied without verifying its hypotheses at the point of use (HP-PROOF-OBLIGATION-GAP).
• results-table arithmetic / delta / aggregation / number coherence → consistency-audit. This skill audits the derivation, not results tables.
• code/result-level fraud (fake GT, self-normalization, phantom numbers) → experiment-forensics at L2. Family G never reaches for code; if you think a flaw needs the code to decide, it is not a proof-validity finding.
• "first / SOTA / novel" external truth → emit needs_external_check and hand to baseline-comparison-audit + citation-forensics, never a guess.

Constants & Reviewer Calling Convention

REVIEWER_MODEL          = gpt-5.6-sol                  # different family from executor (Claude)
REVIEWER_REASONING      = xhigh                    # always; effort never lowers reviewer quality
REVIEWER_SANDBOX        = read-only                # detect-only; never mutate the paper
REVIEWER_CWD            = <paper-dir>              # so it can read claims.json + the proof sources directly
THREAD_POLICY           = fresh mcp__codex__codex per run (and per fan-out theorem group);
                          NEVER mcp__codex__codex-reply
TAXONOMY_VERSION        = 0.5                      # references/hack-pattern-taxonomy.md
OWNED_PATTERNS          = HP-PROOF-OBLIGATION-GAP · HP-PROOF-CIRCULARITY ·
                          HP-DERIVATION-INVALID · HP-SYMBOL-SEMANTIC-DRIFT ·
                          HP-ASSUMPTION-SMUGGLE · HP-UNDEFINED-NOTATION   # family G; emit ONLY these
OBLIGATION_SCAFFOLD     = <TRACE_DIR>/obligation-ledger.md   # Step 1 — EXTRACTION ONLY,
                          not a verdict, NOT claims.json, NOT the anchor substrate
FINDINGS                = proof-derivation-forensics.findings.json   # Step 3 — the ONLY
                          findings file (no deterministic tool exists for family G)
TRACE_POLICY            = forensic (never silently dropped)
TRACE_DIR               = .aris/traces/proof-derivation-forensics/<YYYY-MM-DD>_run<NN>/

• Executor (Claude) builds nothing of the judgment: it locates the ledger, extracts the obligation scaffold (structure only, never validity), pre-computes the per-theorem anchor candidates, passes paths + the ledger + the scaffold + the checklist to the reviewer, validates the reviewer's spans, and writes the findings file. It never summarizes the proof, pre-judges soundness, or leaks an opinion into the prompt (reviewer-independence.md).
• Reviewer (codex / gpt-5.6-sol) reads claims.json, the obligation scaffold, and the proof sources; proposes findings; self-reports false_positive_risk. It is the evidence-extractor / candidate-explainer, not the judge.
• Fresh thread per run. If you fan out by theorem for breadth, each theorem is a new mcp__codex__codex call — never codex-reply carrying one theorem's conclusions into another (the bias guard). codex-reply is intentionally absent from allowed-tools.

---

Step 0 — Preconditions: locate the ledger, read the level, confirm proofs exist

The ledger is the only structure this skill anchors to. Resolve it, read the observability level L, paper_id, the claim count, the source files, and whether the paper contains any proof/theorem/derivation to audit (each Bash block is self-contained — shell state does not persist between calls, so re-derive paths every step):

ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd)
# $ARGUMENTS is a paper-dir OR a claims.json path:
LEDGER="$ARGUMENTS"; [ -d "$LEDGER" ] && LEDGER="$LEDGER/claims.json"
# Only the NO-ARGUMENT case defaults to the CWD ledger. An EXPLICIT argument that
# resolves to a missing claims.json must NOT silently fall back to $(pwd) — that
# could audit the wrong paper; let the NO_LEDGER check below fire instead.
[ -z "$ARGUMENTS" ] && LEDGER="$(pwd)/claims.json"
python3 - "$LEDGER" <<'PY'
import json, sys, os, re
p = sys.argv[1]
if not os.path.isfile(p):
    sys.exit("NO_LEDGER: claims.json not found. Run /evidence-ledger FIRST "
             "(it writes artifact_manifest.json + claims.json).")
d = json.load(open(p, encoding="utf-8"))
paper_dir = os.path.dirname(os.path.abspath(p)) or "."
print("LEDGER       =", os.path.abspath(p))
print("PAPER_DIR    =", paper_dir)
print("PAPER_ID     =", d.get("paper_id", "?"))
print("RUN_LEVEL_L  =", d.get("observability_level", 0))
print("CLAIMS       =", len(d.get("claims", [])))
# Does the paper contain proofs/theorems/derivations to audit?
TH  = re.compile(r"\\begin\{(theorem|lemma|proposition|corollary|claim|conjecture|"
                 r"proof|definition|assumption)\*?\}", re.I)
EQ  = re.compile(r"\\begin\{(equation|align|gather|multline|eqnarray)\*?\}|\\\[", re.I)
TXT = re.compile(r"\b(Theorem|Lemma|Proposition|Corollary|Proof|Q\.?E\.?D\.?)\b")
srcs, hits = [], 0
for s in d.get("source_files", []):
    sp = s.get("path", ""); kind = s.get("kind", "")
    cand = sp if os.path.isabs(sp) else os.path.join(paper_dir, sp)
    if not os.path.isfile(cand): cand = sp
    srcs.append((cand, kind))
    try: t = open(cand, encoding="utf-8", errors="replace").read()
    except OSError: continue
    hits += (len(TH.findall(t)) + len(EQ.findall(t))) if kind == "latex" else len(TXT.findall(t))
print("SOURCE_FILES =", " ; ".join(c for c, _ in srcs) or "(none)")
print("HAS_PROOFS   =", ("yes" if hits > 0 else "no"), f"(markers={hits})")
PY

Carry forward the absolute LEDGER / PAPER_DIR, the SOURCE_FILES, plus L and PAPER_ID, into every step below.

Failure / edge handling.

• NO_LEDGER → stop and tell the user to run /evidence-ledger first. This skill never re-reads the raw PDF and invents its own structure (contract rule 1).
• HAS_PROOFS = no (no theorem/lemma/proof/derivation markers) → there is nothing for family G to audit (the proof analog of NOT_APPLICABLE). Write the empty findings file directly — printf '[]\n' > "$(dirname "$LEDGER")/proof-derivation-forensics.findings.json" — record a trace note (Step 5), and stop. Silent skip is forbidden; an empty array is a valid, non-silent output the adjudicator reads as "this dimension found nothing." Do not call the reviewer.
• CLAIMS == 0 → the ledger has no spans to anchor to even if proofs exist; write the empty findings file as above, note it in the trace, and stop.
• RUN_LEVEL_L == 0 (PDF-text only) → proceed, but recall is reduced: equation and theorem-statement spans are poorly captured, so obligation/assumption findings that need the LaTeX source to confirm an obligation is undischarged anywhere will carry observability_level_required: 1, so an L0 run reports them as unconfirmed (honest — you can suspect from PDF text, you cannot confirm). Family G is at full strength at L1.
• RUN_LEVEL_L == 2 → proof checks run identically (they are textual/semantic); the extra L2 power (paper-number↔result-file) belongs to /experiment-forensics.

Step 1 — Build the proof-obligation scaffold (EXTRACTION ONLY — never a verdict)

Create this run's trace dir, then extract — for each theorem/lemma/proposition and its proof — the obligations the theorem creates, without judging whether any is discharged. This adapts proof-checker's Phase 0.5 ledger and formula-derivation's step typing, under one hard rule:

The scaffold EXTRACTS, it does not ADJUDICATE. Inventorying obligations, typing symbols, restating quantifiers, and tagging a step identity / proposition / approximation / interpretation is structural extraction. Whether a step is valid — whether an obligation is actually discharged — is a correctness verdict reserved for the cross-model reviewer (Step 2) and the adjudicator (Step 6). The executor records the obligation and a location pointer to where the paper claims to discharge it (file:line) — never its own judgment that the discharge is sound. "UNCITED" means the paper cites no discharge location, NOT the executor checked the math and it fails. (See acceptance-gate.md: the loop may self-verify that the scaffold is complete, never that the proofs are correct.) The scaffold is not claims.json and not the anchor substrate — findings still anchor to ledger claims in Step 3.

LEDGER="<abs path to claims.json from Step 0>"; D="$(dirname "$LEDGER")"
TBASE="$D/.aris/traces/proof-derivation-forensics/$(date +%F)"
NN=1; while [ -e "${TBASE}_run$(printf '%02d' "$NN")" ]; do NN=$((NN+1)); done
TRACE_DIR="${TBASE}_run$(printf '%02d' "$NN")"; mkdir -p "$TRACE_DIR"
echo "TRACE_DIR = $TRACE_DIR"   # carry this absolute path into Steps 2 and 5

Use Read to open each file in SOURCE_FILES and locate every \begin{theorem|lemma|proposition|corollary|claim|conjecture} … \end{...} block and its matching \begin{proof} … \end{proof} (or the derivation paragraphs that play that role). For each, extract the entries below.

Anchor candidates (the bridge to Step 3's gate). For each theorem, list the ledger claim_ids whose text_span overlaps the theorem+proof line window — these are the only places a finding on that theorem can ground. Run (per theorem block):

LEDGER="<abs path to claims.json>"; FILE="<source file of this theorem>"
START="<thm block start line>"; END="<proof block end line>"
python3 - "$LEDGER" "$FILE" "$START" "$END" <<'PY'
import json, os, sys
ledger, f, a, b = sys.argv[1], sys.argv[2], int(sys.argv[3]), int(sys.argv[4])
d = json.load(open(ledger, encoding="utf-8"))
base = os.path.basename(f)
for c in d.get("claims", []):
    loc = c.get("location", {}) or {}
    ln = loc.get("line")
    same = base == os.path.basename(loc.get("file", "") or "")
    if same and isinstance(ln, int) and a - 2 <= ln <= b + 2:
        prev = " ".join((c.get("text_span", "") or "").split())[:90]
        print(f'{c["claim_id"]:>6}  {c.get("type",""):<10}  L{ln}  "{prev}"')
PY

Then Write the scaffold to $TRACE_DIR/obligation-ledger.md using this template (one block per theorem; record pointers, never verdicts):

# Proof-Obligation Scaffold — <PAPER_ID>   (EXTRACTION ONLY — NO validity verdict)
> Structures the reviewer's per-obligation pass. NOT claims.json, NOT the anchor
> substrate, contains NO "proved / sound / valid" judgments. Soundness is the Step-2
> reviewer's call; the verdict is the Step-6 adjudicator's.

## T1 — <theorem name / \label{...}>   [<file>:<line-range>]
- Statement (verbatim): "<exact theorem statement>"
- Canonical quantified form: ∀… ∃… s.t. …      (or: UNCLEAR — needs disambiguation)
- Stated hypotheses: H1 …; H2 …
- Typed symbols: κ: scalar ∈(0,1), dep (d,Σ); u*: vector ∈ℝ^d; B: matrix, sym PSD …
- Headline-dependent?: yes/no   (does the abstract / main claim rest on T1?)
- Proof location: <file>:<line-range>
- Obligations (every nontrivial step; tag identity|proposition|approximation|interpretation;
  record claimed discharge location — a pointer, NOT a validity judgment):
    - O1 [proposition]   "<step text>"   — claimed discharge: <file>:<line> | UNCITED
    - O2 [identity]      "<step text>"   — …
    - O3 [approximation] "<step text>"   — enters at <line>; later used as exact? pointer
    - O4 [interpretation]"<prose step>"  — presented as derivation? pointer
- Imported results applied: <\cite{} / named thm> @ <line>
  — hypotheses to verify at point of use: …
- Anchor-candidate claim_ids (from the helper above): C0xx, C0yy, …   (statement: C0xx)

Breadth for a large multi-theorem paper (no Agent grant). Scaffold construction is pure structural extraction — walk the theorems sequentially. This skill spawns nothing: allowed-tools grants no Agent (matching the other Anti-Autoresearch auditors, which thread codex calls rather than fork subagents), so there is no executor-side fan-out here. Breadth, when you want it, happens on the reviewer side — issue one fresh mcp__codex__codex call per theorem in Step 2 (never codex-reply). Either way the extraction never adjudicates, and you must merge all theorem blocks into one scaffold before looking for a cross-theorem dependency cycle (semantic circularity for HP-PROOF-CIRCULARITY): a per-theorem view misses exactly the cross-theorem cycles this skill exists to catch.

Step 2 — Cross-model per-obligation review (reviewer ≠ adjudicator)

Open a fresh mcp__codex__codex thread (the Reviewer Calling Convention above) and send it the checklist. The reviewer reads claims.json, the scaffold, and the proof sources from its cwd; it judges from the full proof, but every finding must anchor to a ledger claim_id — an anchor candidate from the scaffold whose text_span verbatim-contains the failing fragment. Send EXACTLY (substitute the absolute PAPER_DIR, the L value, and the scaffold path from Steps 0–1):

mcp__codex__codex:
  model: gpt-5.6-sol
  config: {"model_reasoning_effort": "xhigh"}
  sandbox: read-only
  cwd: <absolute PAPER_DIR from Step 0>
  prompt: |
    You are an integrity-forensics reviewer auditing a THIRD PARTY's PROOFS and
    DERIVATIONS for VALIDITY OF THE WRITTEN ARGUMENT only. You have NO external ground
    truth, you do NOT re-run anything, and you do NOT judge authorship. You decide
    from the WRITTEN proof: does it actually ESTABLISH its theorem? You NEVER assert a
    proof is "fabricated" or "faked" — you assert, with the exact line quoted, that
    THE STEP SHOWN DOES NOT HOLD / THE OBLIGATION IS NOT DISCHARGED / A SYMBOL'S
    MEANING DRIFTED / AN UNSTATED ASSUMPTION IS USED.

    INPUTS (in your working directory, read them directly):
      - claims.json — the evidence ledger: the authoritative, span-anchored list of
        checkable spans. This is the ONLY structure you ANCHOR to. Each claim has
        {claim_id, type, text_span (VERBATIM source text), location}. NOTE: the ledger
        has NO dedicated theorem/proof extractor — proof text appears only inside
        number/scope/citation/caption/table_cell spans that OVERLAP it.
      - obligation-ledger.md (path below) — an EXTRACTION-ONLY scaffold: per theorem,
        its statement, hypotheses, typed symbols, the obligations its proof creates
        (each tagged identity/proposition/approximation/interpretation), and the
        ANCHOR-CANDIDATE claim_ids. It carries NO validity verdicts — judging validity
        is YOUR job. Use it to structure your pass (one finding per failing obligation)
        and to find where you CAN anchor.
      - the proof source files (listed in claims.json source_files) — read them to see
        the FULL proof (ledger spans are fragmentary). You MAY read them freely, but
        you may NOT introduce a finding you cannot anchor to a ledger claim.
    OBLIGATION SCAFFOLD: <abs path to $TRACE_DIR/obligation-ledger.md>
    RUN OBSERVABILITY LEVEL L = <L from Step 0>.