feat(deduction-serve): Band v2-EN — natural-English argument serving, earned licenses (ADR-0257) #107

Merged

core-labs merged 1 commit from feat/english-argument-band into main

2026-07-23 22:14:55 +00:00

core-labs commented

2026-07-23 22:14:43 +00:00

Owner

generate/proof_chain/english.py (new): closed function-word grammar
over OPAQUE clause-atoms (minted ids); if/then, [either] or, and,
three negation forms (leading not / sentential / copular incl.
contractions); typed refusals; honesty caps. Soundness: positive
verdicts are substitution-closed; UNKNOWN is scoped + guarded
(quantifier-led, is-a membership, unnormalizable negation refuse
out of the opaque band).
render_entailment_english: verdicts quoted back verbatim; UNKNOWN
phrasing explicitly scoped to the opaque reading.
chat/deduction_surface.py: v2-EN fallback tier AFTER v1/v1b —
monotone widening, byte-identical on previously-served arguments.
Four en_* shape-bands EARN SERVE via the ADR-0199 arena (720/band,
wrong=0, reliability 0.99087 >= 0.99); 9-band ledger re-sealed.
evals/deduction_serve/v2_en: 26 hand-authored real-English cases
(content disjoint from the synthetic lexicon), wrong=0; report
re-pinned.
realizer guard (ADR-0075): deduction surfaces exempt — quoted
templates are not slot-composed articulations (pack 'open'=VERB
was rejecting an honest quoted 'the door is not open'); pinned
cold+warm in e2e.

[Verification]: deductive 84 passed; smoke 180 passed; cognition 122
passed 1 skipped; arena 9x720 wrong=0 all SERVE; lanes v1 28/28,
v2_en 26/26.

What this ships

CORE now decides natural-English deductive arguments end-to-end through core chat:

> If it rains then the ground is wet. It rains. Therefore the ground is wet.
Given: if it rains then the ground is wet; it rains. Your premises entail: the ground is wet.

> If the seal is broken then the tank is empty. If the tank is empty then the pump is dry.
  The pump is not dry. Therefore the seal is not broken.
Given: … Your premises entail: the seal is not broken.          (two-hop modus tollens)

> Either the door is open or the window is open. The door isn't open. Therefore the window is open.
Given: … Your premises entail: the window is open.              (disjunctive syllogism)

> If the pump runs then the tank fills. If the valve opens then the tank fills.
  The pump runs or the valve opens. Therefore the tank fills.
Given: … Your premises entail: the tank fills.                  (constructive dilemma)

> If it rains then the ground is wet. The ground is wet. Therefore it rains.
Given: … Reading each clause as one indivisible claim, your premises don't settle
whether it rains — it holds in some cases and fails in others.  (honest UNKNOWN, scoped)

Every one of these declined before this PR. Both boundary cases ADR-0256's completion
doc recorded as "the future acceptance tests" — the multiword conditional
(reserved_word_in_np) and nested-negation contraposition (If p then q. Therefore if not q then not p.) — are now decided; their v1 lane gold is promoted declined → entailed.

Governing decision: docs/adr/ADR-0257-english-clause-argument-band.md (Proposed).

How it works

generate/proof_chain/english.py (new) — a dedicated English argument reader used
ONLY by the deduction serving path. Whole English clauses become opaque atoms (minted
ids a0, a1, …; identity = normalized exact text); structure is recognized by a closed
function-word grammar: if <A> then <B> (junctions on both sides), [either] <A> or <B>
(n-ary), top-level and (premise-splitting / conjunctive conclusions), and three negation
forms — leading not, sentential it is not the case that, copular <L> is|are|was|were not <R> (contractions isn't/aren't/wasn't/weren't expanded). Clause content is never
interpreted — only quoted back.
Same verified ROBDD engine decides (generate/proof_chain/entail.py, sound+complete);
render_entailment_english renders verdicts over the user's own clause text.
Composer fallback tier (chat/deduction_surface.py::_english_band_surface) — tried
strictly AFTER Band v1 (single-token propositional) and v1b (categorical). Everything
previously served is served byte-identically; this band only widens. The shared
7-lane comprehension reader is untouched (its guards are load-bearing elsewhere).

Why the opaque reading is sound (ADR-0257 §3)

Propositional entailment is closed under uniform substitution, so ENTAILED / REFUTED /
inconsistent-premises verdicts over opaque clause-atoms remain true under ANY deeper reading
of the clauses — served at full strength. UNKNOWN is the one non-substitution-safe verdict,
so it gets (a) explicitly scoped phrasing ("Reading each clause as one indivisible claim…"),
and (b) structural guards: quantifier-led categorical clauses, is a/an membership
clauses, and unnormalizable negation (never, doesn't, …) refuse OUT of the opaque band
with typed reasons — a genuine syllogism can never be flattened into a misleading "doesn't
follow". Ambiguous scope (mixed top-level and+or, nested conditionals) refuses rather
than guesses. Honesty caps (16 premises / 24 atoms) refuse rather than truncate.

Earned, not granted (ADR-0256 machinery, zero changes needed)

Four new shape-bands — en_conditional_single, en_conditional_chain, en_disjunctive,
en_atomic — each earned Action.SERVE through the ADR-0199 practice arena:
720 cases/band, wrong=0, reliability 0.99087 ≥ θ_SERVE=0.99; 9-band ledger re-sealed
(chat/data/deduction_serve_ledger.json, self-verifying content_sha256).
Arena gold is authored by construction and cross-checked against the independent
truth-table oracle with no reader in the loop (the template's intended logical form is
checked directly) — stronger independence than the v1 path; INV-25 preserved.
Anti-overfit guard: the arena lexicon is synthetic copular clauses ON PURPOSE (the reader
is content-blind; the license certifies structural fidelity). The new eval lane
evals/deduction_serve/v2_en/ (26 hand-authored REAL-English cases, content disjoint
from the synthetic lexicon) keeps that claim honest: 26/26, wrong=0.
Unlicensed band ⇒ automatically hedged (tested). Flag posture unchanged:
deduction_serving_enabled=False default; no new flag.

Bug found live and fixed: realizer-guard category error

The ADR-0075 C1 slot-type guard was silently replacing a correct entailment with the
disclosure fallback: pack lists open as VERB (its composed sense), so R3 rejected the
honest quoted copular "the door is not open" ("dry"/"broken" passed only by being unknown
to the pack — fail-open). A deduction surface is a fixed, test-audited template quoting the
user's clauses verbatim — not a slot-composed articulation — so C1's pack-POS rules are
out of regime for it. Fix: deduction-grounded surfaces are exempt at both runtime call
sites (QUOTED_TEMPLATE_EXEMPT_VERDICT, mirroring the existing empty-surface exemption);
regression pinned cold AND warm in e2e.

Tri-language posture (ADR-0257 §5, per direction)

The atom table, soundness argument, caps, refusal discipline, license machinery, and engine
are language-neutral; only the structural lexicon is English. A grc_*/he_* band is a
sibling reader module + its own earned licenses via pack ratification (ADR-0253 boundary
respected) — NOT a premature lexicon parameter (ἄρα is postpositive; a lexicon swap alone
cannot read real Greek). The en-band refusal telemetry (internal_negation_unread,
ambiguous_and_or) is the instrumented trigger marking exactly where English is the
bottleneck.

Honest scope-outs (deliberate)

member_chain band — "Socrates is a man. All men are mortal. Therefore Socrates is
mortal." — guarded out (membership_shape_out_of_band); designed next band
(per-individual propositional lowering, same pattern as categorical.py).
Verb-phrase negation de-conjugation ("doesn't start") — refuses today; morphology
work or the tri-language path.
Proof-step recap — verdicts only; unchanged ADR-0256 scope-out.

Files

New: generate/proof_chain/english.py, evals/deduction_serve/v2_en/cases.jsonl,
tests/test_english_argument_reader.py, docs/adr/ADR-0257-english-clause-argument-band.md,
docs/research/english-argument-band-2026-07-23.md
Modified: chat/deduction_surface.py, chat/runtime.py (guard exemption),
generate/proof_chain/{render,shape}.py, generate/realizer_guard.py,
evals/deduction_serve/{runner.py,report.json,v1/cases.jsonl,practice/gold.py},
chat/data/deduction_serve_ledger.json (re-sealed, 9 bands), core/cli_test.py,
scripts/verify_lane_shas.py (deduction_serve_v1 pin), + 4 test files extended

[Verification]: uv run core test --suite deductive -q → 84 passed ·
--suite smoke → 180 passed · --suite cognition → 122 passed, 1 skipped ·
practice arena 9×720 wrong=0, all bands SERVE · lanes v1 28/28, v2_en 26/26 ·
ledger self-verifies content_sha256 · report re-pinned in verify_lane_shas.py

Both are also durably in the repo: the title is commit a83b35de's subject line, and this body tracks docs/research/english-argument-band-2026-07-23.md (with the guard-fix section expanded for the record).

CORE now decides natural-English deductive arguments end-to-end: 'If it rains then the ground is wet. It rains. Therefore the ground is wet.' -> ENTAILED, rendered over the user's own clauses. Both of ADR-0256's documented boundary cases (multiword conditional, nested- negation contraposition) are now decided; their lane gold updated declined->entailed. - generate/proof_chain/english.py (new): closed function-word grammar over OPAQUE clause-atoms (minted ids); if/then, [either] or, and, three negation forms (leading not / sentential / copular incl. contractions); typed refusals; honesty caps. Soundness: positive verdicts are substitution-closed; UNKNOWN is scoped + guarded (quantifier-led, is-a membership, unnormalizable negation refuse out of the opaque band). - render_entailment_english: verdicts quoted back verbatim; UNKNOWN phrasing explicitly scoped to the opaque reading. - chat/deduction_surface.py: v2-EN fallback tier AFTER v1/v1b — monotone widening, byte-identical on previously-served arguments. - Four en_* shape-bands EARN SERVE via the ADR-0199 arena (720/band, wrong=0, reliability 0.99087 >= 0.99); 9-band ledger re-sealed. - evals/deduction_serve/v2_en: 26 hand-authored real-English cases (content disjoint from the synthetic lexicon), wrong=0; report re-pinned. - realizer guard (ADR-0075): deduction surfaces exempt — quoted templates are not slot-composed articulations (pack 'open'=VERB was rejecting an honest quoted 'the door is not open'); pinned cold+warm in e2e. [Verification]: deductive 84 passed; smoke 180 passed; cognition 122 passed 1 skipped; arena 9x720 wrong=0 all SERVE; lanes v1 28/28, v2_en 26/26. --- ## What this ships CORE now decides **natural-English deductive arguments** end-to-end through `core chat`: ``` > If it rains then the ground is wet. It rains. Therefore the ground is wet. Given: if it rains then the ground is wet; it rains. Your premises entail: the ground is wet. > If the seal is broken then the tank is empty. If the tank is empty then the pump is dry. The pump is not dry. Therefore the seal is not broken. Given: … Your premises entail: the seal is not broken. (two-hop modus tollens) > Either the door is open or the window is open. The door isn't open. Therefore the window is open. Given: … Your premises entail: the window is open. (disjunctive syllogism) > If the pump runs then the tank fills. If the valve opens then the tank fills. The pump runs or the valve opens. Therefore the tank fills. Given: … Your premises entail: the tank fills. (constructive dilemma) > If it rains then the ground is wet. The ground is wet. Therefore it rains. Given: … Reading each clause as one indivisible claim, your premises don't settle whether it rains — it holds in some cases and fails in others. (honest UNKNOWN, scoped) ``` Every one of these **declined before this PR**. Both boundary cases ADR-0256's completion doc recorded as "the future acceptance tests" — the multiword conditional (`reserved_word_in_np`) and nested-negation contraposition (`If p then q. Therefore if not q then not p.`) — are now decided; their v1 lane gold is promoted `declined → entailed`. Governing decision: **`docs/adr/ADR-0257-english-clause-argument-band.md`** (Proposed). ## How it works - **`generate/proof_chain/english.py` (new)** — a dedicated English argument reader used ONLY by the deduction serving path. Whole English clauses become **opaque atoms** (minted ids `a0, a1, …`; identity = normalized exact text); structure is recognized by a **closed function-word grammar**: `if <A> then <B>` (junctions on both sides), `[either] <A> or <B>` (n-ary), top-level `and` (premise-splitting / conjunctive conclusions), and three negation forms — leading `not`, sentential `it is not the case that`, copular `<L> is|are|was|were not <R>` (contractions `isn't/aren't/wasn't/weren't` expanded). Clause *content* is never interpreted — only quoted back. - **Same verified ROBDD engine decides** (`generate/proof_chain/entail.py`, sound+complete); `render_entailment_english` renders verdicts over the user's own clause text. - **Composer fallback tier** (`chat/deduction_surface.py::_english_band_surface`) — tried strictly AFTER Band v1 (single-token propositional) and v1b (categorical). Everything previously served is served **byte-identically**; this band only widens. The shared 7-lane comprehension reader is **untouched** (its guards are load-bearing elsewhere). ## Why the opaque reading is sound (ADR-0257 §3) Propositional entailment is **closed under uniform substitution**, so ENTAILED / REFUTED / inconsistent-premises verdicts over opaque clause-atoms remain true under ANY deeper reading of the clauses — served at full strength. UNKNOWN is the one non-substitution-safe verdict, so it gets (a) explicitly scoped phrasing ("Reading each clause as one indivisible claim…"), and (b) **structural guards**: quantifier-led categorical clauses, `is a/an` membership clauses, and unnormalizable negation (`never`, `doesn't`, …) refuse OUT of the opaque band with typed reasons — a genuine syllogism can never be flattened into a misleading "doesn't follow". Ambiguous scope (mixed top-level `and`+`or`, nested conditionals) refuses rather than guesses. Honesty caps (16 premises / 24 atoms) refuse rather than truncate. ## Earned, not granted (ADR-0256 machinery, zero changes needed) - Four new shape-bands — `en_conditional_single`, `en_conditional_chain`, `en_disjunctive`, `en_atomic` — each earned `Action.SERVE` through the ADR-0199 practice arena: **720 cases/band, wrong=0, reliability 0.99087 ≥ θ_SERVE=0.99**; 9-band ledger re-sealed (`chat/data/deduction_serve_ledger.json`, self-verifying `content_sha256`). - Arena gold is authored **by construction** and cross-checked against the independent truth-table oracle with **no reader in the loop** (the template's intended logical form is checked directly) — stronger independence than the v1 path; INV-25 preserved. - Anti-overfit guard: the arena lexicon is synthetic copular clauses ON PURPOSE (the reader is content-blind; the license certifies structural fidelity). The new eval lane **`evals/deduction_serve/v2_en/` (26 hand-authored REAL-English cases, content disjoint from the synthetic lexicon)** keeps that claim honest: 26/26, wrong=0. - Unlicensed band ⇒ automatically hedged (tested). Flag posture unchanged: `deduction_serving_enabled=False` default; no new flag. ## Bug found live and fixed: realizer-guard category error The ADR-0075 C1 slot-type guard was **silently replacing a correct entailment** with the disclosure fallback: pack lists `open` as VERB (its composed sense), so R3 rejected the honest quoted copular "the door is not open" ("dry"/"broken" passed only by being unknown to the pack — fail-open). A deduction surface is a fixed, test-audited template quoting the user's clauses **verbatim** — not a slot-composed articulation — so C1's pack-POS rules are out of regime for it. Fix: deduction-grounded surfaces are exempt at both runtime call sites (`QUOTED_TEMPLATE_EXEMPT_VERDICT`, mirroring the existing empty-surface exemption); regression pinned **cold AND warm** in e2e. ## Tri-language posture (ADR-0257 §5, per direction) The atom table, soundness argument, caps, refusal discipline, license machinery, and engine are language-neutral; only the structural lexicon is English. A `grc_*`/`he_*` band is a sibling reader module + its own earned licenses via pack ratification (ADR-0253 boundary respected) — NOT a premature lexicon parameter (ἄρα is postpositive; a lexicon swap alone cannot read real Greek). The en-band refusal telemetry (`internal_negation_unread`, `ambiguous_and_or`) is the instrumented trigger marking exactly where English is the bottleneck. ## Honest scope-outs (deliberate) 1. **`member_chain` band** — "Socrates is a man. All men are mortal. Therefore Socrates is mortal." — guarded out (`membership_shape_out_of_band`); designed next band (per-individual propositional lowering, same pattern as `categorical.py`). 2. **Verb-phrase negation de-conjugation** ("doesn't start") — refuses today; morphology work or the tri-language path. 3. **Proof-step recap** — verdicts only; unchanged ADR-0256 scope-out. ## Files - New: `generate/proof_chain/english.py`, `evals/deduction_serve/v2_en/cases.jsonl`, `tests/test_english_argument_reader.py`, `docs/adr/ADR-0257-english-clause-argument-band.md`, `docs/research/english-argument-band-2026-07-23.md` - Modified: `chat/deduction_surface.py`, `chat/runtime.py` (guard exemption), `generate/proof_chain/{render,shape}.py`, `generate/realizer_guard.py`, `evals/deduction_serve/{runner.py,report.json,v1/cases.jsonl,practice/gold.py}`, `chat/data/deduction_serve_ledger.json` (re-sealed, 9 bands), `core/cli_test.py`, `scripts/verify_lane_shas.py` (deduction_serve_v1 pin), + 4 test files extended [Verification]: `uv run core test --suite deductive -q` → 84 passed · `--suite smoke` → 180 passed · `--suite cognition` → 122 passed, 1 skipped · practice arena 9×720 wrong=0, all bands SERVE · lanes v1 28/28, v2_en 26/26 · ledger self-verifies `content_sha256` · report re-pinned in `verify_lane_shas.py` Both are also durably in the repo: the title is commit a83b35de's subject line, and this body tracks docs/research/english-argument-band-2026-07-23.md (with the guard-fix section expanded for the record).

core-labs added 1 commit 2026-07-23 22:14:44 +00:00

feat(deduction-serve): Band v2-EN — natural-English argument serving, earned licenses (ADR-0257) a83b35de07

CORE now decides natural-English deductive arguments end-to-end:
'If it rains then the ground is wet. It rains. Therefore the ground
is wet.' -> ENTAILED, rendered over the user's own clauses. Both of
ADR-0256's documented boundary cases (multiword conditional, nested-
negation contraposition) are now decided; their lane gold updated
declined->entailed.

- generate/proof_chain/english.py (new): closed function-word grammar
  over OPAQUE clause-atoms (minted ids); if/then, [either] or, and,
  three negation forms (leading not / sentential / copular incl.
  contractions); typed refusals; honesty caps. Soundness: positive
  verdicts are substitution-closed; UNKNOWN is scoped + guarded
  (quantifier-led, is-a membership, unnormalizable negation refuse
  out of the opaque band).
- render_entailment_english: verdicts quoted back verbatim; UNKNOWN
  phrasing explicitly scoped to the opaque reading.
- chat/deduction_surface.py: v2-EN fallback tier AFTER v1/v1b —
  monotone widening, byte-identical on previously-served arguments.
- Four en_* shape-bands EARN SERVE via the ADR-0199 arena (720/band,
  wrong=0, reliability 0.99087 >= 0.99); 9-band ledger re-sealed.
- evals/deduction_serve/v2_en: 26 hand-authored real-English cases
  (content disjoint from the synthetic lexicon), wrong=0; report
  re-pinned.
- realizer guard (ADR-0075): deduction surfaces exempt — quoted
  templates are not slot-composed articulations (pack 'open'=VERB
  was rejecting an honest quoted 'the door is not open'); pinned
  cold+warm in e2e.

[Verification]: deductive 84 passed; smoke 180 passed; cognition 122
passed 1 skipped; arena 9x720 wrong=0 all SERVE; lanes v1 28/28,
v2_en 26/26.