# 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.