docs: ADR-0114a — anti-overfitting proof obligations for expert promotion

Documentation-only amendment to ADR-0114. Locks in the 10-point
falsifiable proof framework that any future `expert` ledger-tier
promotion (ADR-0120+) MUST require.

The obligations:

  1.  Sealed-holdout discipline
  2.  OOD surface variation ≥ 0.95 of public
  3.  Every correct answer ships with replay-equal trace
  4.  Refusal is first-class; misparse rate zero; zero `wrong` answers
  5.  Reasoning-isolation perturbation suite (invariance + predictable change)
  6.  Compositional-depth curve flat within documented ε
  7.  Frontier-baseline comparison on identical items, published
  8.  Adversarial generation; misparse rate zero
  9.  Determinism across release boundaries
  10. Operation provenance via the pack (not hardcoded strings)

Each obligation is load-bearing and falsifiable: a domain that
cannot satisfy any one stays at `audit-passed`. ADR-0114a binds
ADR-0116..ADR-0120 to carry the obligations into implementation;
ADR-0120 finally invokes all ten as hard gates.

The audit-passed tier (ADR-0106/0109/0113) is unaffected. The two
tiers measure orthogonal properties: audit-passed verifies CORE
claim-shape compliance (transformer-unreachable invariants); expert
verifies capability with anti-overfitting proof.

No code change. Pure forward contract for the next phase of work.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

docs/decisions/ADR-0114a-anti-overfitting-proof-obligations.md

@@ -0,0 +1,378 @@
+# ADR-0114a — Anti-Overfitting Proof Obligations for `expert` Promotion
+
+**Status:** Accepted (documentation-only; no code change)
+**Date:** 2026-05-22
+**Author:** CORE agents + reviewers
+**Type:** Amendment to ADR-0114
+**Depends on:** ADR-0091, ADR-0105, ADR-0106, ADR-0109, ADR-0113, ADR-0114, ADR-0115
+
+---
+
+## Context
+
+ADR-0113 reserved the `expert` namespace for a future ledger tier above
+`audit-passed`. ADR-0114 laid out a 7-phase arc toward a first `expert`
+promotion (GSM8K-math), with ADR-0120 designated as the eventual
+"first `expert` promotion contract."
+
+The intervening discussion surfaced a load-bearing question: **how
+does CORE prove a domain's `expert` claim is reasoning from concepts
+rather than pattern-matching from seen examples?** This is *the*
+distinguishing question for any capability claim beyond the structural
+asymmetries `audit-passed` already verifies. An LLM scoring 95% on a
+benchmark may be memorizing or surface-pattern-matching; the claim
+"reasons from concepts" requires structural evidence that cannot be
+faked.
+
+The audit-passed gate does not need this discussion — it verifies
+*claim shapes* (signed digest, replay determinism, typed refusal,
+exact recall) that transformer LLMs structurally cannot produce
+regardless of accuracy. But the moment a domain reaches for `expert`
+on a public benchmark, that's a raw-capability comparison, and the
+"is it actually reasoning?" question is the only credibility-bearing
+question.
+
+ADR-0114a writes down, before any `expert` promotion code is built,
+the 10-point proof framework that ADR-0120's promotion contract must
+enforce.
+
+---
+
+## Decision
+
+The eventual `expert` promotion contract (ADR-0120) MUST require all
+ten obligations below. Each obligation is **load-bearing and
+falsifiable**: a domain that cannot satisfy any one of them stays at
+`audit-passed`.
+
+These obligations apply to every `expert` promotion, not just
+GSM8K-math. Future expert domains (symbolic logic, DSL codegen,
+etc.) inherit the same framework; per-domain specializations may
+add further requirements but cannot weaken these.
+
+### Obligation 1 — Sealed-holdout discipline
+
+**Requirement.** The capability benchmark must include a held-out
+split that is never read by any CORE component during development.
+Holdout sealing per ADR-0105 (age-encrypted, recipient-keyed).
+
+**Falsification.** If commit history shows any access to the
+holdout cases during the window between dev-set authoring and the
+release event, the promotion is invalid.
+
+**Status.** Substrate already in place (ADR-0105 sealed holdouts;
+ADR-0114 §5 GSM8K-test-set-is-holdout commitment). Per-lane
+enforcement lands in ADR-0119.
+
+### Obligation 2 — OOD surface variation must score ≥ 0.95 of dev
+
+**Requirement.** A capability lane that scores `S` on its public
+split must score ≥ `0.95 · S` on a programmatically-derived
+out-of-distribution split that holds the underlying graph constant
+but varies surface form:
+
+- Entity-name renaming
+- Unit relabeling (apples → nebulae, dollars → drachmas)
+- Number-magnitude scaling (multiply all by k; for linear-arithmetic
+  domains, answer must scale by k)
+- Independent-sentence reordering
+
+If CORE handles graph G correctly, it should handle every surface
+that lexes to graph G. A drop > 5% from public to OOD signals
+surface-feature dependence rather than reasoning from concepts.
+
+**Falsification.** Score the same graphs through three surface
+renderings; if the lowest-scoring rendering falls below
+`0.95 · public_score`, the promotion is invalid.
+
+**Status.** OOD generator authoring required. Likely ADR-0118
+(stepped realizer extension can do double duty) or a separate
+ADR-0118a.
+
+### Obligation 3 — Every correct answer ships with a replay-equal trace
+
+**Requirement.** For every problem CORE marks "correct" on the
+public + holdout splits, an inspectable `SolutionTrace` artifact
+exists with:
+
+- Ordered sequence of operations
+- Each operation tagged with the pack-lemma identifier it invokes
+  (operation provenance)
+- A byte-deterministic trace hash
+- Verifier (ADR-0117) re-applies the trace and reproduces the
+  declared answer
+
+**Falsification.** If any "correct" answer cannot be paired with a
+trace whose replay reproduces the answer, the promotion is invalid.
+A trace that reproduces the *wrong* answer is more useful than no
+trace at all — the *wrong* answer is then known to be a real CORE
+mistake, not a fake reasoning artifact.
+
+**Status.** Trace produced by ADR-0116 (solver). Verifier in ADR-0117.
+
+### Obligation 4 — Refusal is a first-class outcome; misparse rate is zero
+
+**Requirement.** Every problem produces exactly one of three
+outcomes:
+
+- `correct` — answer matches ground truth AND trace replays
+- `wrong` — answer differs from ground truth (trace may still replay)
+- `refused` — typed `ParseError` / `SolveError` with a reason naming
+  the unsupported construction
+
+**The `expert` threshold per ADR-0120 must require zero `wrong`
+answers.** A high `refused` rate is acceptable and informative; a
+nonzero `wrong` rate fails the gate. CORE cannot claim to reason if
+it sometimes produces silent confabulations.
+
+The distinction vs. LLMs is intentional: a frontier LLM scoring 95%
+on GSM8K typically has ~5% wrong and ~0% refused (it confabulates
+when uncertain). CORE's expert claim requires the opposite shape:
+high correct + nonzero refused + **zero wrong**.
+
+**Falsification.** Any verified wrong answer on the public or
+holdout split — where "verified wrong" means the trace replays but
+yields a value differing from ground truth — invalidates the
+promotion.
+
+**Status.** Parser (ADR-0115 Phase 1.3) already enforces typed
+refusal; solver (ADR-0116) must enforce the same discipline. The
+zero-wrong-on-public requirement is per-domain calibration; ADR-0120
+sets it.
+
+### Obligation 5 — Reasoning-isolation perturbation suite
+
+**Requirement.** A programmatic perturbation generator produces an
+unbounded test suite by applying invariance-preserving and
+invariance-breaking transforms to dev/holdout cases:
+
+| Transform | Expected behavior |
+|---|---|
+| Rename all entities | Answer unchanged |
+| Rename all units | Answer unchanged |
+| Multiply all numbers by k | Answer × k (linear domains); changes predictably (general) |
+| Reorder independent sentences | Answer unchanged |
+| Swap order of non-commuting operations | Answer changes predictably |
+| Replace verb with synonym in registry | Answer unchanged |
+
+CORE must pass 100% of invariance-preserving perturbations and produce
+the predicted change on every invariance-breaking one. A pattern-matcher
+that learned superficial features fails some perturbations; a system
+reasoning from concepts passes all.
+
+**Falsification.** ≥ 1% perturbation failure on any single transform
+class invalidates the promotion.
+
+**Status.** Generator authoring required. New ADR (likely ADR-0119
+subsidiary or its own).
+
+### Obligation 6 — Compositional-depth curve published
+
+**Requirement.** Score correctness as a function of reasoning depth
+(number of operations in the ground-truth graph). Publish the depth-
+vs-accuracy curve from depth 1 through the maximum depth in the
+benchmark. **The curve must be approximately flat** — accuracy at
+depth N should not drop by more than `1 − (1 − ε)^N` for some
+documented `ε`, where ε represents per-step parser/solver error.
+
+A monotonically-decreasing curve indicates probabilistic
+accumulation of errors; a flat curve indicates the architecture
+handles N-step problems by the same mechanism as 1-step problems.
+
+For comparison, LLM GSM8K curves typically decay sharply past
+depth 4-5. CORE's curve should not.
+
+**Falsification.** If any depth bucket scores below `(1 − ε)^N`
+for the documented `ε`, the promotion is invalid (or `ε` must be
+raised, with justification, in the published curve).
+
+**Status.** Measurement only; no new code. Computed at promotion time.
+
+### Obligation 7 — Frontier-baseline comparison on identical items
+
+**Requirement.** Run the holdout split through at least one frontier
+LLM baseline (citation-only, no live API call) and publish:
+
+- Both raw scores
+- A per-item disagreement matrix (CORE-correct × LLM-correct,
+  -wrong, -refused/n/a; CORE-refused × LLM-correct, -wrong; etc.)
+- Trace replay verification for every CORE-correct answer
+
+The interesting cell — and the honest one to publish — is
+**"LLM correct ∧ CORE refused"**. Those are problems where rule-based
+grammar caps out; refusing them is correct behavior but it leaves
+capability on the table. The size of this cell is a public, durable
+measurement of CORE's current grammar coverage vs. frontier LLM
+breadth. ADR-0120's expert threshold sets a maximum acceptable size.
+
+**Falsification.** If the comparison report cannot demonstrate
+trace replay on every CORE-correct answer, the promotion is invalid.
+
+**Status.** Pattern established by ADR-0045 (long-context comparison);
+GSM8K equivalent landed in ADR-0119.
+
+### Obligation 8 — Adversarial generation; misparse rate zero
+
+**Requirement.** A separate generator produces problems specifically
+designed to exploit weak grammar / solver coverage:
+
+- Edge-case phrasings within the documented grammar
+- Problems combining patterns in untested ways
+- Problems with deceptive surface (e.g. red-herring numbers)
+
+Every adversarial problem must produce one of: `correct`, `refused`,
+or — never — silent misparse. A **misparse** is defined as: parser
+produces a graph that does NOT correspond to the surface meaning AND
+the resulting answer is wrong.
+
+**Misparse rate must be zero on the adversarial suite.** Refused
+rate may be arbitrarily high; that's the safe failure mode.
+
+**Falsification.** Any single observed misparse (graph + answer
+disagreement with the surface) invalidates the promotion.
+
+**Status.** Generator authoring required; likely under ADR-0119.
+
+### Obligation 9 — Determinism across release boundaries
+
+**Requirement.** Same problem text + same pack revision + same
+solver revision → byte-equal trace hash across N runs (N ≥ 100) and
+across at least one re-build of the runtime (proves no
+floating-point-platform drift, no thread-order drift, no random
+seed drift).
+
+**Falsification.** Any non-determinism observation invalidates
+the promotion until the source is identified and eliminated.
+
+**Status.** Already an architectural invariant of CORE
+(versor-closure, replay-determinism). Per-lane test gates run at
+promotion time.
+
+### Obligation 10 — Operation provenance via the pack
+
+**Requirement.** Every operation in every published `SolutionTrace`
+dispatches through a math-pack (or relevant-domain-pack) lemma
+identifier, not a hardcoded string in solver code. The trace
+includes the resolved lemma id for every operation, and changing the
+pack changes the resolved set deterministically.
+
+This obligation makes "reasons from concepts" architecturally true
+rather than rhetorical. Without it, the parser-to-pack binding is
+informal and the claim "the math pack provides the operation
+vocabulary" is decorative.
+
+**Falsification.** If any operation in a published trace cannot
+resolve to a pack-lemma id, the promotion is invalid.
+
+**Status.** Currently informal (parser hardcodes verb→operation-kind
+mapping in ADR-0115 Phase 1.3). **Closing this gap is in-scope for
+ADR-0116 (solver).** ADR-0114a documents the requirement; ADR-0116
+implements the binding.
+
+---
+
+## Acceptance & enforcement
+
+ADR-0114a is a **documentation-only contract**. No code lands with
+this ADR.
+
+It binds future ADRs:
+
+- **ADR-0116 (solver)** — must add operation-provenance binding
+  (#10) and trace shape that supports #3.
+- **ADR-0117 (verifier)** — must produce replay-verdicts that
+  support #3 and #9.
+- **ADR-0118 / ADR-0118a (realizer + OOD surface generator)** —
+  must produce OOD-rendering capability for #2.
+- **ADR-0119 (GSM8K eval lane)** — must wire #1, #6, #7, #8 into
+  the lane runner.
+- **ADR-0120 (first expert promotion contract)** — must require
+  all 10 obligations as hard gates, including the explicit numeric
+  thresholds (zero wrong; ≥ 0.95·S on OOD; flat depth curve within
+  documented ε).
+
+Each downstream ADR cites which obligation it discharges. ADR-0120
+finally invokes all ten.
+
+---
+
+## Invariants
+
+### `adr_0114a_obligations_enumerated`
+
+The 10 obligations above are the complete, ordered list. Adding an
+obligation, removing one, or weakening one requires a numbered
+amendment ADR. The list itself is sticky.
+
+### `adr_0114a_no_silent_overfit`
+
+Any future `expert` promotion ADR that omits one of the ten
+obligations from its acceptance criteria is invalid. Reviewers
+checking promotion ADRs MUST verify the obligations checklist is
+populated. Skipping the checklist is grounds for refusal at review.
+
+### `adr_0114a_audit_passed_unaffected`
+
+ADR-0114a does NOT amend ADR-0106 / ADR-0109 / ADR-0113. The
+`audit-passed` gate continues to verify CORE claim-shape compliance
+(signed digest + replay determinism + typed refusal + exact recall)
+without any of these ten obligations. The two tiers measure
+orthogonal properties.
+
+---
+
+## Out of scope
+
+- Specific numeric thresholds. Those belong to ADR-0120 (e.g. "depth
+  curve ε ≤ 0.02"; "OOD score ≥ 0.95 · public_score"). ADR-0114a
+  documents the *shape* of each obligation, not the numbers.
+- Implementation of the perturbation generator. Future ADR.
+- Implementation of the adversarial generator. Future ADR.
+- LLM-vendor selection for #7 (frontier comparison). ADR-0045 set
+  the convention (citation, not live API); ADR-0119 picks the
+  specific baseline.
+- Domains beyond mathematics_logic. The framework is domain-agnostic;
+  each future expert domain (symbolic logic, DSL codegen, ...)
+  inherits it. Per-domain specializations may add obligations but
+  cannot remove any of these ten.
+- Writing / open-prose capability. Even with all ten obligations
+  satisfied, prose-domain `expert` claims need additional discussion
+  (what "correct" means for prose is fuzzily defined); deferred per
+  ADR-0114 §Phase F.
+
+---
+
+## Consequences
+
+- The repo carries a public, dated commitment to a falsifiable proof
+  framework for any future `expert` claim. The "are you sure you're
+  reasoning, not pattern-matching?" question has a written answer:
+  the 10 obligations, every one checkable.
+- ADR-0116 / ADR-0117 / ADR-0118 / ADR-0119 / ADR-0120 each gain a
+  subset of these obligations as scope items. Each downstream ADR
+  cites which obligations it discharges.
+- The `audit-passed` tier and the `expert` tier remain
+  cleanly distinguished. Audit-passed verifies claim *shapes*
+  (transformer-unreachable invariants); expert verifies *capability*
+  with anti-overfitting proof. A domain can be one without the other,
+  though in practice `audit-passed` is a prerequisite for `expert`.
+- External readers (reviewers, investors, skeptics) now have
+  an enumerated checklist to evaluate any future `expert` claim
+  against. Promotions that omit obligations are easily distinguished
+  from promotions that satisfy them.
+
+---
+
+## Open candidate directions (no ADR yet)
+
+- **Cross-domain transfer probes.** Once two domains land at
+  `expert`, can CORE solve a problem that requires combining
+  operations from both packs (e.g. physics-units-aware arithmetic)?
+  Not part of these 10 obligations but a natural next-tier question.
+- **Adversarial generation budget.** How many adversarial problems
+  is "enough" for #8? Likely answer: keep generating until refused
+  rate stabilizes. ADR-0119 picks the convention.
+- **Frontier baseline freshness.** ADR-0045's citation freezes
+  vendor numbers at a point in time. Frontier scores drift up; CORE's
+  comparison should be re-cited periodically. The cadence is a
+  governance choice deferred to a future ADR.

docs/decisions/README.md

@@ -35,7 +35,8 @@ ADRs record significant architectural decisions: what was decided, why, what alt
 | [ADR-0112](ADR-0112-runnable-expert-demo-showcase.md) | Runnable Audit-Passed Showcase (originally "Expert-Demo") | Accepted (2026-05-22) |
 | [ADR-0113](ADR-0113-rename-expert-demo-to-audit-passed.md) | Rename `expert-demo` → `audit-passed`; Reserve `expert` for Future Capability Tier | Accepted (2026-05-22) |
 | [ADR-0114](ADR-0114-expert-capability-roadmap-gsm8k-first.md) | Expert-Capability Roadmap: GSM8K-Math First | Proposed (2026-05-22) |
-| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1 Accepted (2026-05-22) |
+| [ADR-0114a](ADR-0114a-anti-overfitting-proof-obligations.md) | Anti-Overfitting Proof Obligations for `expert` Promotion | Accepted (2026-05-22) |
+| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1+1.2+1.3 Accepted (2026-05-22) |
 
 ---
 
@@ -67,7 +68,8 @@ The ADR-0091..0114 slate is fully accepted (0091..0113) plus one proposed-roadma
 - Runnable Audit-Passed Showcase (originally "Expert-Demo"; renamed) — ADR-0112 + ADR-0113
 - Rename `expert-demo` → `audit-passed`; reserve `expert` namespace — ADR-0113
 - Expert-Capability Roadmap (GSM8K-Math first); proposed — ADR-0114
-- Math Problem Parser & Typed Graph (Phase 1.1 schema + 5 seed cases); Phase 1.2 (45 more cases) delegated — ADR-0115
+- Math Problem Parser & Typed Graph (Phase 1.1 schema + 5 seeds + Phase 1.2 45 more cases + Phase 1.3 parser engine; 50/50 byte-equal) — ADR-0115
+- Anti-Overfitting Proof Obligations for any future `expert` promotion (10-point falsifiable framework) — ADR-0114a
 
 ADR-0080 has also landed: Contemplation Loop Phase 1 adds a read-only frontier-compare miner that emits `SPECULATIVE` findings only.