From d0d1a96669e18e952562526723b73a88c373f697 Mon Sep 17 00:00:00 2001 From: Shay Date: Fri, 22 May 2026 06:28:51 -0700 Subject: [PATCH] docs: mark ADR 0097 accepted --- ...cs-logic-reasoning-capable-ratification.md | 130 +++++++----------- 1 file changed, 47 insertions(+), 83 deletions(-) diff --git a/docs/decisions/ADR-0097-mathematics-logic-reasoning-capable-ratification.md b/docs/decisions/ADR-0097-mathematics-logic-reasoning-capable-ratification.md index f7eab761..266a636b 100644 --- a/docs/decisions/ADR-0097-mathematics-logic-reasoning-capable-ratification.md +++ b/docs/decisions/ADR-0097-mathematics-logic-reasoning-capable-ratification.md @@ -1,37 +1,42 @@ # ADR-0097 — Mathematics-Logic Reasoning-Capable Ratification -**Status:** Proposed +**Status:** Accepted **Date:** 2026-05-21 +**Accepted:** 2026-05-22 **Author:** CORE agents + reviewers **Depends on:** ADR-0091, ADR-0092, ADR-0093, ADR-0096 --- +## Acceptance evidence + +Accepted after `mathematics_logic` became a mechanically ratified `reasoning-capable` ledger row: + +- `language_packs/data/en_mathematics_logic_v1/manifest.json` carries Domain Pack Contract v1 fields. +- `teaching/domain_chains/mathematics_logic_chains_v1.jsonl` supplies reviewed active chains. +- `core/capability/domain_contract_predicates.py` verifies all nine ADR-0091 predicates. +- `tests/test_adr_0097_mathematics_logic_ratification.py` pins: + - all nine predicates pass for `en_mathematics_logic_v1` + - the ledger row status is `reasoning-capable` + - provenance points at `adr-0097:reviewed:*` + - `expert_demo` remains false + - declared lanes include `elementary_mathematics_ood`, `inference_closure`, and `fabrication_control` + +--- + ## Context -The mathematics/logic substrate is more complete than recent planning -documents acknowledged: +The mathematics/logic substrate is structurally complete: - `language_packs/data/en_mathematics_logic_v1/` ships with manifest, lexicon, glosses. - `teaching/domain_chains/mathematics_logic_chains_v1.jsonl` exists. - `evals/elementary_mathematics_ood/` exists. -- `docs/gaps.md` marks every mathematics-logic gap closed: - `gap:mathematics_logic_pack_absent`, - `gap:mathematics_logic_transitive_chains_below_threshold`, - `gap:mathematics_logic_proof_chain_chains_below_threshold`, - `gap:mathematics_logic_contradiction_chains_below_threshold`, - `gap:mathematics_logic_intent_shapes_below_threshold` — all `[x]`. - -What is missing is the formal ratification step under ADR-0091. The -pack manifest does not yet carry `domain_contract_version: 1` fields; -the validator (ADR-0093) cannot run against it yet; the reviewer -registry (ADR-0092) was empty until that ADR. +- `docs/gaps.md` marks mathematics-logic gaps closed. This ADR is the first concrete domain claim under the Domain Pack -Contract. It is small on purpose: content already exists, infrastructure -already exists, and this is the wiring that turns existing artifacts -into a ratified `reasoning-capable` ledger row. +Contract. It turns existing artifacts into a ratified +`reasoning-capable` ledger row. --- @@ -39,7 +44,7 @@ into a ratified `reasoning-capable` ledger row. Ratify `en_mathematics_logic_v1` as `reasoning-capable` under ADR-0091 by emitting the contract fields into its manifest and passing -`core capability domain-contract validate en_mathematics_logic_v1`. +domain-contract validation. ### Manifest additions @@ -51,21 +56,9 @@ ADR-0091 by emitting the contract fields into its manifest and passing "rules": null, "teaching_chains": ["mathematics_logic_chains_v1"], "eval_lanes": [ - { - "lane": "elementary_mathematics_ood", - "version": "v1", - "splits": ["dev", "public", "holdout"] - }, - { - "lane": "inference_closure", - "version": "v1", - "splits": ["dev", "public", "holdout"] - }, - { - "lane": "fabrication_control", - "version": "v1", - "splits": ["dev", "public", "holdout"] - } + {"lane": "elementary_mathematics_ood", "version": "v1", "splits": ["dev", "public", "holdout"]}, + {"lane": "inference_closure", "version": "v1", "splits": ["dev", "public", "holdout"]}, + {"lane": "fabrication_control", "version": "v1", "splits": ["dev", "public", "holdout"]} ], "reviewers": ["shay-j"], "known_gaps": [], @@ -74,31 +67,20 @@ ADR-0091 by emitting the contract fields into its manifest and passing ``` `axioms` and `rules` stay `null` at v1. The pack proves reasoning -through chain composition (modus ponens, modus tollens, contradiction -detection, transitivity), not through declarative axioms. A future -ADR may add explicit axioms; this one does not. +through chain composition, not through declarative axioms. A future ADR +may add explicit axioms; this one does not. -### Required existing evidence (no new content) +### Required evidence -- `mathematics_logic_chains_v1.jsonl` must contain ≥ 8 reviewed - chains per operator family it claims (per ADR-0091 predicate #5). - If it does not, ratification is blocked. Block is content, not - contract — close the chain corpus first, ratify second. -- ≥ 3 intent shapes present (per predicate #6). The cognition lane's - intent coverage (DEFINITION, RECALL, CAUSE, VERIFICATION, - COMPARISON, PROCEDURE, CORRECTION, NARRATIVE, EXAMPLE) already - exceeds this on the cognition pack; this ADR audits that the - math/logic chain corpus exercises at least three. -- Three-split eval lane referenced. `elementary_mathematics_ood` - exists; `inference_closure` exists; ADR-0096 introduces - `fabrication_control`. Holdout paths verified non-empty. +- `mathematics_logic_chains_v1.jsonl` contains ≥ 8 reviewed chains per claimed operator family. +- ≥ 3 intent shapes are present. +- Three-split eval lane references exist for positive coverage, composition, and negative control. ### What this ADR does not do - Does not introduce new lemmas, chains, or evals. -- Does not promote to `expert-demo`. That requires audit-tour-equivalent - reports — separate ADR. -- Does not modify the runtime. Pack mounting behavior is unchanged. +- Does not promote to `expert-demo`. +- Does not modify runtime mount behavior. --- @@ -106,50 +88,32 @@ ADR may add explicit axioms; this one does not. `mathematics_logic_reasoning_capable_ledger_row` — running `core capability ledger` emits a row for `domain_id: mathematics_logic` -with `status: reasoning-capable`, with provenance pointing at this -ADR, and refuses to advance to `expert-demo` until a future ADR -attaches the required reports. +with `status: reasoning-capable`, provenance pointing at this ADR, and +`expert_demo: False` until a future ADR attaches audit-tour-equivalent +reports. --- ## Lane -No new lane. Existing lanes carry the evidence: +Existing lanes carry the evidence: -- `elementary_mathematics_ood/` (positive coverage) -- `inference_closure/` (composition) -- `fabrication_control/` (negative control, ADR-0096) -- `evals/domain_contract_validation/` (ADR-0093 confirms predicates fire) - -CLAIMS.md Tier 2 gains one row pointing at the four lanes and this -ADR. +- `elementary_mathematics_ood/` — positive coverage +- `inference_closure/` — composition +- `fabrication_control/` — negative control +- `evals/domain_contract_validation/` — predicate validation --- ## Trust Boundary -Manifest edit is a reviewed proposal. Checksum refresh per -ADR-0027/0029 discipline. No runtime mount path changes. No new -filesystem writes outside the manifest and its checksum companion. +Manifest edit is a reviewed proposal. Checksum refresh follows pack discipline. +No runtime mount path changes. No new filesystem writes outside the manifest and its checksum companion. --- ## Consequences -- First `reasoning-capable` row in the capability ledger backed by an - ADR-0091-validated pack. -- Sibling ratifications (systems-software, physics, hebrew/greek) - become mechanical follow-ups using the same template. Each one is - its own ADR but each is small. -- The public showcase demo (ADR-0099) gains a real domain to draw - Scene 4 from. - ---- - -## PR Checklist - -- Capability added: first ratified `reasoning-capable` domain claim. -- Invariant proved: `mathematics_logic_reasoning_capable_ledger_row`. -- Lanes proving it: four existing lanes plus ADR-0093 contract validator. -- Hidden normalization / stochastic fallback / approximate recall / unreviewed mutation: none. Ratification is the reviewed proposal. -- Trust boundary: manifest edit through reviewed flow; checksums refreshed. +- First `reasoning-capable` row in the capability ledger backed by an ADR-0091-validated pack. +- Sibling ratifications become mechanical follow-ups using the same template. +- The public showcase demo (ADR-0099) gains a real domain to draw Scene 4 from.