core/docs/decisions/ADR-0114a.10-pack-provenance-auditor.md

ADR-0114a.10 — Pack-Provenance Auditor (Obligation #10 wired for B3)

Status: Accepted Date: 2026-05-23 Author: CORE main agent (Opus 4.7) Depends on: ADR-0114a (10 anti-overfitting obligations), ADR-0116 (deterministic solver), ADR-0117 (solution-trace verifier), ADR-0131.3 (B3 bounded grammar lane), ADR-0131.4 (composite math-expert gate) Parent: ADR-0114a Sequencing: first of 5 remaining ADR-0114a obligations for mathematics_logic. Subsequent: #2 OOD ratio, #5 perturbation, #6 depth curve, #8 adversarial.

---

Context

ADR-0114a Obligation #10 reads:

Every SolutionTrace.steps[*].pack_lemma_id resolves to a real lexicon entry in the domain's operator pack.

The solver already enforces this at solve time. _resolve_pack_lemmas in generate/math_solver.py (lines 153–190) loads en_arithmetic_v1, looks up the 8 required operation kinds against the pack's lemma surfaces, and refuses to construct a SolutionTrace if any lemma is missing. Every SolutionStep then carries a pack_lemma_id of the form <pack_id>:<lemma>.

ADR-0114a's discipline is anti-overfitting: a guarantee that lives only inside the function that produces traces is one bug away from silently failing. The obligation requires an external audit — independent reading of the pack on disk, independent walk of the trace, byte-level resolution check.

Decision

Implement an external pack-provenance auditor at core/capability/pack_provenance.py:

1. Re-read the pack lexicon from disk (independent of the solver's loader).
2. Re-run the candidate-graph pipeline on each case of a B-lane.
3. Walk every solver step and validate pack_lemma_id parses as <pack_id>:<lemma> AND pack_id == expected AND lemma ∈ pack_lexicon.
4. Per-case + per-lane verdict, deterministic obligation_10_passed: bool.
5. CLI core capability pack-provenance writes a committed audit artifact at evals/obligation_10_pack_provenance/<lane_id>.json.

What's wired (this PR)

B3 (bounded grammar) under en_arithmetic_v1. B3 is the lane whose pipeline (parser → graph → solver → verifier) exercises math_solver end-to-end and produces traces with non-trivial step counts — exactly what obligation #10 is structured around.

What's deferred to follow-up sub-ADRs

• B1 (symbolic equivalence) equivalent. B1's verification path is algebra-based (check_equivalence(A, B)), not arithmetic- step-based. The pack-lemma notion needs reframing — likely "every equivalence check's normalization chain references real algebra-pack lemmas." Separate ADR.
• B2 (teaching corpus) extension. B2 may exercise the same math_solver depending on its corpus contents; the auditor below can be extended once that's confirmed case-by-case. The auditor's validate_lane(lane_id=..., cases_path=...) signature makes that a trivial extension when the time comes.

Empirical verdict on current main

$ python3 -m core.cli capability pack-provenance

lane:                       B3_bounded_grammar
pack_id:                    en_arithmetic_v1
cases_total:                50
cases_validated:            25
cases_skipped_unsolved:     25     (refusal-expected probes — by design)
cases_violated:             0
obligation_10_passed:       True
distinct_lemma_ids_observed:
  - en_arithmetic_v1:add
  - en_arithmetic_v1:compare_additive
  - en_arithmetic_v1:compare_multiplicative
  - en_arithmetic_v1:subtract
  - en_arithmetic_v1:transfer

Obligation #10 passes on B3 — every solver step on every expected-correct case resolves to a real lemma in en_arithmetic_v1. 5 of the 8 operation kinds are exercised by B3's grammar; the other 3 (multiply, divide, apply_rate) are registered in the pack but not in B3's case set — fine, they ratify-at-solve-time via _resolve_pack_lemmas so the obligation holds for them too if a future case exercises them.

What this does NOT do

• Does NOT change the solver. The solver's pack binding is already correct; this PR audits it from outside.
• Does NOT modify any B-lane runner or case set.
• Does NOT change the SolutionTrace schema. The pack_lemma_id field already exists.
• Does NOT promote mathematics_logic to expert. Promotion requires this obligation + 4 others (#2 OOD, #5 perturbation, #6 depth curve, #8 adversarial) + the composite gate from ADR-0131.4 + reviewer signature via ADR-0092.
• Does NOT wire B1 or B2 equivalents. Each is its own follow-up ADR (above).

Trust boundary

• Reads only:
  • language_packs/data/en_arithmetic_v1/lexicon.jsonl (the pack-on-disk; auditor MUST read this independently rather than trusting the solver's loader)
  • evals/math_bounded_grammar/v1/cases.jsonl (the B3 case set)
• Writes only: the path passed to emit_provenance_report (default evals/obligation_10_pack_provenance/B3_bounded_grammar.json).
• No dynamic imports, no shell passthrough, no network.
• Pure deterministic function — verified by test_validate_lane_is_deterministic + test_artifact_emission_byte_equal.

Tests

tests/test_adr_0114a_10_pack_provenance.py — 19 tests:

Group	Count	What it pins
lemma-id parser	8	well-formed accepted; malformed rejected
lexicon loader	4	real pack loads; missing/invalid file refuses
lane validator	5	passes on real B3; observes expected lemma surface shape; refuses on missing pack/cases; skips refusal-expected cases without false violation
determinism	2	report identical across two calls; artifact byte-equal

All pass in 0.27s.

Composition with ADR-0131.4

A future full ADR-0120 wire-up would consume both evaluate_composite_math_gate() (composite benchmark verdict) AND validate_lane() (obligation #10 verdict) — plus the four remaining obligation auditors when they land — and emit a single signed expert_claims artifact for ledger promotion.

The composite gate doesn't change. The evaluate_composite_math_gate function in ADR-0131.4 (PR #188) gates the math-specific benchmark portion of the contract; this auditor gates the math-specific obligation #10 portion. They're orthogonal and compose multiplicatively.

CLAUDE.md PR-checklist

• Capability added: external pack-provenance auditor for obligation #10; makes the solver's pack-binding externally-falsifiable per ADR-0114a's audit discipline.
• Invariant proving field validity: obligation_10_passed on B3; 0 violations across 25 validated cases; 5 distinct lemma_ids all resolve.
• CLI/eval proving the lane: python3 -m core.cli capability pack-provenance + pytest tests/test_adr_0114a_10_pack_provenance.py.
• Avoided hidden normalization / stochastic / approximate / unreviewed mutation: Yes. Pure deterministic auditor.
• Trust boundary: read-only inputs from documented paths; single deterministic write to documented artifact path; no dynamic imports.