docs: mark ADR 0097 accepted
This commit is contained in:
Shay
parent
852585a83d
commit
d0d1a96669
1 changed files with 47 additions and 83 deletions
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Reference in a new issue