feat(deduction-serve): Band v5-VP — verb-predicate arguments, decided (ADR-0260)

Generalization arc Phase 1.1 (Tier F, docs/plans/generalization-arc-2026-07-24.md): "All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches." now reads and decides — the ADR-0258 §6.3 verb-predicate scope-out, and the reading gate for Phase 2's subject serving. generate/proof_chain/verb.py extends v3-MEM's per-individual lowering with a second atom family in one shared space: membership atoms (v3-MEM's own parsers reused verbatim) + verb atoms (individual, verb-lemma-group, object-term). Verb universals instantiate as mem(i,C) -> [~]verb(i), so a copula-minted membership fact discharges a verb rule. The ONE new semantic identification is closed 3sg agreement (verb-specific irregular table + the three regular suffix rules — deliberately NOT the noun table, which would misroute "lives"/"leaves"). Scope-tight segmentation: single-token name/class/verb/object shapes only; everything longer refuses typed (tense_out_of_band joins the closed reason vocabulary). Rendered by render_entailment_verb (member surface, UNKNOWN scoping extended to the verb reading). Rides deduction_serving_enabled (default off); pure widening — every previously-served argument byte-identical, no existing lane case changed outcome. Earned: 4 en_verb_* bands x 720 arena wrong=0 (first seal), ledger resealed at 21 bands; corpus soundness asserted against the independent truth-table oracle over each template's intended lowering (15,120 cases, INV-25). Lane: v2_verb 28 hand-authored real cases 28/28 first run; full lane 134/134 wrong=0 across five splits. Surgical single-line pin update + CLAIMS regen. Stacked on feat/generalization-phase0 (merge that first — shared verify_lane_shas.py / CLAIMS.md / generate_claims.py lane-ADR mapping). [Verification]: verb reader tests 34/34; deduction battery 86/86 (surface +5, e2e +1, lane +1) in-worktree; arena seal + oracle cross-check green; smoke + warmed_session via pre-push gate.
2026-07-24 12:51:01 -07:00 · 2026-07-24 12:51:01 -07:00 · d181ae30f9
commit d181ae30f9
parent f95ac26ec0
19 changed files with 1481 additions and 13 deletions
--- a/CLAIMS.md
+++ b/CLAIMS.md
@ -43,7 +43,7 @@ is a CI failure (`.github/workflows/lane-shas.yml`).
 | ADR-0104 | `curriculum_loop_closure` | Curriculum-sourced proposals route through single reviewed teaching path | `evals/curriculum_loop_closure/results/v1_dev.json` | `cb94ca0042d78ec2624129ff6493d52e767b69feea32d2997b85d88f1c0883af` |
 | ADR-0131 | `math_teaching_corpus_v1` | Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0) | `evals/math_teaching_corpus/v1/report.json` | `eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4` |
 | ADR-0206 | `deductive_logic_v1` | Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0 | `evals/deductive_logic/report.json` | `97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f` |
-| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be` |
+| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a` |

 ## Verification

--- a/chat/data/deduction_serve_ledger.json
+++ b/chat/data/deduction_serve_ledger.json
@ -118,9 +118,37 @@
      "t2_agrees_gold": 0,
      "t2_verified": 0,
      "wrong": 0
+    },
+    "en_verb_chain": {
+      "correct": 720,
+      "refused": 0,
+      "t2_agrees_gold": 0,
+      "t2_verified": 0,
+      "wrong": 0
+    },
+    "en_verb_fact": {
+      "correct": 720,
+      "refused": 0,
+      "t2_agrees_gold": 0,
+      "t2_verified": 0,
+      "wrong": 0
+    },
+    "en_verb_negative": {
+      "correct": 720,
+      "refused": 0,
+      "t2_agrees_gold": 0,
+      "t2_verified": 0,
+      "wrong": 0
+    },
+    "en_verb_universal": {
+      "correct": 720,
+      "refused": 0,
+      "t2_agrees_gold": 0,
+      "t2_verified": 0,
+      "wrong": 0
    }
  },
-  "content_sha256": "6285a423957bc9a3a6a562515a338dfd6f36188ac00f45c1a6ea979c4e3cc710",
+  "content_sha256": "b5dd8db3ac4770f229269c16d388325a0763237ff84c21618309468eabf46a77",
  "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.",
  "provenance": "evals.deduction_serve.practice.runner.seal_ledger",
  "schema": "deduction_serve_ledger_v1"
--- a/chat/deduction_surface.py
+++ b/chat/deduction_surface.py
@ -34,6 +34,13 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md):
  space, read by ``generate.proof_chain.cond_member``. Tried strictly AFTER
  v3-MEM (which guards these shapes out via ``mixed_structure_out_of_band``)
  — again a pure widening tier.
+- Band v5-VP (ADR-0260) — verb-predicate arguments ("All philosophers teach.
+  Socrates is a philosopher. Therefore Socrates teaches."), read by
+  ``generate.proof_chain.verb`` via per-individual lowering with a second
+  (individual, verb-group, object) atom family alongside v3-MEM's membership
+  atoms, decided by the same engine. Tried strictly AFTER v4-CM (the earlier
+  bands refuse quantifier-led verb universals, is-a + verb mixes, and
+  ``does not`` negation) — again a pure widening tier.

 Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path
 below returns a committed, honest surface — reader refusal, out-of-band shape,
@ -59,8 +66,10 @@ from generate.proof_chain.render import (
    render_entailment,
    render_entailment_english,
    render_entailment_member,
+    render_entailment_verb,
    render_syllogism,
 )
+from generate.proof_chain.verb import VerbArgument, read_verb_argument
 from generate.proof_chain.shape import CATEGORICAL, classify_deduction_shape

 #: An argument's conclusion clause starts a sentence with "therefore" — the
@ -143,6 +152,9 @@ def deduction_grounded_surface(
        cond_member = _cond_member_band_surface(text, license_lookup)
        if cond_member is not None:
            return cond_member
+        verb = _verb_band_surface(text, license_lookup)
+        if verb is not None:
+            return verb
        return _READER_REFUSAL_SURFACE.format(reason=comp.reason)
    # Band v1 — propositional argument.
    projected = to_deductive_logic(comp)
@ -175,6 +187,10 @@ def deduction_grounded_surface(
    cond_member = _cond_member_band_surface(text, license_lookup)
    if cond_member is not None:
        return cond_member
+    # Band v5-VP fallback — the verb-predicate shapes every earlier band guards out.
+    verb = _verb_band_surface(text, license_lookup)
+    if verb is not None:
+        return verb
    return _OUT_OF_BAND_SURFACE


@ -220,6 +236,21 @@ def _cond_member_band_surface(text: str, license_lookup: _LicenseLookup) -> str
    return _license_gate(surface, arg.band, license_lookup)


+def _verb_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None:
+    """Band v5-VP (ADR-0260): read *text* as a verb-predicate argument
+    (membership atoms + verb atoms over one per-individual space), and decide
+    with the same verified ROBDD engine; ``None`` when the reader refuses (the
+    caller keeps its pre-existing honest surface — this band only ever widens
+    what is decided). Rendered by ``render_entailment_verb``, whose UNKNOWN
+    scoping extends the member phrasing to the verb reading."""
+    arg = read_verb_argument(text)
+    if not isinstance(arg, VerbArgument):
+        return None
+    trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula)
+    surface = render_entailment_verb(trace, arg.premise_texts, arg.query_text)
+    return _license_gate(surface, arg.band, license_lookup)
+
+
 def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str:
    """Serve *surface* authoritatively iff *band* holds a SERVE license; else
    serve the same sound answer DISCLOSED (hedged). The one place the earned-
--- a/core/cli_test.py
+++ b/core/cli_test.py
@ -180,6 +180,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = {
        "tests/test_english_argument_reader.py",
        "tests/test_member_argument_reader.py",
        "tests/test_cond_member_argument_reader.py",
+        "tests/test_verb_argument_reader.py",
        "tests/test_deduction_serve_e2e.py",
    ),
    "full": ("tests/",),
--- a/docs/adr/ADR-0260-verb-predicate-band.md
+++ b/docs/adr/ADR-0260-verb-predicate-band.md
@ -0,0 +1,131 @@
+# ADR-0260 — Band v5-VP: verb-predicate arguments, decided
+
+- **Status:** Proposed
+- **Date:** 2026-07-24
+- **Arc:** deduction-serve (ADR-0256 → 0257 → 0258 → 0259 → this)
+- **Governs:** `generate/proof_chain/verb.py`, the `en_verb_*` shape-bands,
+  their arena templates, the `v2_verb` lane split, and the
+  `_verb_band_surface` serving tier.
+
+## 1. Context
+
+ADR-0258 §6.3 scoped verb predicates out of the member band: v3-MEM reads
+only copula sentences, so "All philosophers teach. Socrates is a
+philosopher. Therefore Socrates teaches." refused — despite being the plain
+English shape in which most non-logic subject matter states its rules
+(physics, biology, and every other domain speak in verb sentences, not is-a
+chains). The generalization arc (docs/plans/generalization-arc-2026-07-24.md
+Phase 1.1) makes this the single highest-leverage reading unlock: Phase 2's
+curriculum-entailment serving is gated on it.
+
+The earlier bands each guard this territory out rather than misreading it:
+v2-EN refuses quantifier-led sentences (`categorical_shape_out_of_band`),
+is-a clauses (`membership_shape_out_of_band`), and unnormalized negation
+(`internal_negation_unread`); v3-MEM/v4-CM refuse copula-free sentences
+(`sentence_shape_out_of_band`). Pure verb-fact restatements with none of
+those triggers are ALREADY decided soundly by v2-EN as opaque clause-atoms —
+so this band's genuine territory is exactly the fall-through: arguments
+mixing verb sentences with quantified rules, membership facts, or `does not`
+negation.
+
+## 2. Decision
+
+Add `generate.proof_chain.verb.read_verb_argument` as the next fallback tier
+(after v1 / v1b / v2-EN / v3-MEM / v4-CM), extending v3-MEM's
+per-individual propositional lowering with a SECOND atom family in one
+shared space:
+
+- **Membership atoms** *(individual, class-group)* — minted by v3-MEM's own
+  `_parse_singular` / `_parse_universal`, reused verbatim (copula sentences
+  keep their exact v3-MEM reading, refusals included).
+- **Verb atoms** *(individual, verb-lemma-group, object-term)* — minted from
+  verb facts (`<name> <verb3sg> [<object>]`, `does not` negation, the
+  sentential-not prefix) and verb universals
+  (`all|every|each|no [the] <class> <verb> [<object>]`).
+
+A verb universal instantiates at every named individual as
+`mem(i, C) -> [~]verb(i)` — so a membership fact minted by a copula sentence
+discharges a verb rule. The same verified ROBDD engine decides.
+
+Bands (priority order): `en_verb_negative` (any negative universal, either
+kind) > `en_verb_chain` (≥2 universals) > `en_verb_universal` (exactly 1) >
+`en_verb_fact` (facts only). Rendered by `render_entailment_verb` — the
+member surface with the UNKNOWN scoping extended to the verb reading. Rides
+`deduction_serving_enabled` (default off); no new flag.
+
+## 3. Why this is sound
+
+1. **Instantiation** — identical to ADR-0258 §3: universal instantiation at
+   named individuals is truth-preserving in every first-order model, and
+   each *(verb-group, object-term)* pair is one opaque unary predicate over
+   the same named-individual domain. ENTAILED / REFUTED / inconsistent
+   verdicts over the lowered premises hold in every model of the original
+   argument; completeness within the fragment lifts the same way (a
+   propositional countermodel's domain is exactly the named individuals).
+2. **Agreement is the ONE new identification** — a universal's base form
+   ("teach") and a singular fact's 3sg form ("teaches") are identified iff
+   related by a CLOSED relation: a verb-specific irregular table (has/have,
+   goes/go, does/do; consulted first, sole authority for its tokens) else
+   the three regular suffix rules (+s, +es after sibilants, y↔ies). The noun
+   table is deliberately NOT reused — it would misroute verb forms like
+   "lives" (noun: life; verb: live). Under-linking costs coverage, never
+   soundness. Object terms link by exact token identity only.
+3. **Scope-tight segmentation** — without a lexicon, an arbitrary
+   copula-free token run cannot be soundly split into subject/verb/object;
+   the band reads single-token name/class/verb/object shapes ONLY, and
+   refuses everything longer, typed. A three-token sentence read as
+   (subject, verb, object) is a disclosed reading, restated verbatim in the
+   surface's "Given:" line.
+4. **Cascade honesty** — every text this band decides was verified to be
+   REFUSED by all four earlier bands (the arena templates and lane cases
+   are constructed on the fall-through path serving actually uses), so this
+   tier is pure widening: every previously-served argument is served
+   byte-identically.
+
+## 4. License and render
+
+The four `en_verb_*` bands earned SERVE through the ADR-0199 arena
+(720/band committed, wrong=0, θ_SERVE=0.99; ledger resealed at 21 bands).
+The arena's by-construction gold is cross-checked template-by-template
+against the independent truth-table oracle over each template's INTENDED
+per-individual lowering, with no reader in the loop (INV-25). Unearned or
+ledger-stripped deployments serve the same sound answer hedged
+(`_UNVERIFIED_SHAPE_DISCLOSURE`), exactly as every earlier band.
+
+## 5. Scope-outs (typed refusals today, future bands' territory)
+
+1. **Connective × verb composition** — "If Socrates teaches then …"
+   refuses `mixed_structure_out_of_band`; fusing v4-CM's connective grammar
+   over verb leaves is the natural next composition.
+2. **Multi-token subjects/objects, PPs, adverbs, ditransitives** —
+   `sentence_shape_out_of_band`. Note one disclosed misreading inside the
+   3-token shape: an adverb in object position ("Lena runs quickly") is
+   read as an object TERM — never unsound (worst case an over-scoped
+   UNKNOWN), documented here rather than guessed at.
+3. **Tense** — `did not` refuses `tense_out_of_band`; bare past forms
+   ("taught") are indistinguishable from lemmas without a lexicon and read
+   as distinct opaque lemmas (under-linking, sound).
+4. **Arity/subsumption** — "teaches" does not entail "teaches logic" (nor
+   vice versa) under the face-value reading; both directions stay UNKNOWN,
+   scoped. Same posture v2-EN already takes for opaque clauses.
+5. **Plural/bare subjects in verb facts** ("dogs bark") — read as an
+   individual named "dogs" (disclosed in the UNKNOWN scoping); the copula
+   analogue is refused by v3-MEM's bare-plural guard, but no copula means no
+   plural signal in the closed grammar.
+6. Existential (`some`) witnesses, identity/co-reference — unchanged
+   scope-outs inherited from ADR-0258 §6 (existentials are the
+   generalization arc's Phase 1.2, assigned to the Opus tier).
+
+## 6. Verification
+
+- `tests/test_verb_argument_reader.py` — 34 tests: gap-is-real cross-check,
+  flagship lowering, every agreement rule, object-in-atom-key, chain
+  discharge, cross-individual non-leakage, family separation
+  (teacher/teaches), 14 typed refusals incl. delegated v3-MEM reasons,
+  honesty caps, determinism.
+- Surface/e2e/lane: `tests/test_deduction_surface.py` (+5),
+  `tests/test_deduction_serve_e2e.py` (+1),
+  `tests/test_deduction_serve_lane.py` (+1 over the 28-case `v2_verb`
+  split) — full lane 134/134, wrong=0, all five splits.
+- Arena: 4 × 720 committed, wrong=0, first seal run; corpus soundness
+  asserted against the independent oracle before sealing (15,120 cases).
--- a/docs/research/verb-predicate-band-2026-07-24.md
+++ b/docs/research/verb-predicate-band-2026-07-24.md
@ -0,0 +1,87 @@
+# Band v5-VP — verb-predicate arguments, decided (ADR-0260)
+
+**Date:** 2026-07-24 · **Branch:** `feat/verb-predicate-band` (stacked on
+`feat/generalization-phase0`) · **Arc:** generalization
+(docs/plans/generalization-arc-2026-07-24.md, Phase 1.1 — Tier F)
+
+## What CORE can now do
+
+```
+> All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches.
+Given: all philosophers teach; socrates is a philosopher.
+Your premises entail: socrates teaches.
+```
+
+Verb sentences — the shape in which every non-logic subject states its
+rules — now read and decide. The cascade's earlier bands each guard this
+territory out (v2-EN refuses quantifier leads / is-a clauses / `does not`;
+v3-MEM and v4-CM refuse copula-free sentences), so the tier is pure
+widening on the fall-through path.
+
+## Mechanism (ADR-0260 §2)
+
+v3-MEM's per-individual lowering, extended with a second atom family in ONE
+shared space: membership atoms *(individual, class-group)* — minted by
+v3-MEM's own parsers reused verbatim — plus verb atoms *(individual,
+verb-lemma-group, object-term)*. A verb universal instantiates at every
+named individual as `mem(i,C) -> [~]verb(i)`, so a copula-minted membership
+fact discharges a verb rule. The ONE new semantic identification is 3sg
+agreement: a closed verb relation (irregular table has/goes/does first, then
+s / +es-after-sibilant / y↔ies) links "teach"↔"teaches". The noun table is
+deliberately NOT reused — it would misroute "lives" (noun: life; verb:
+live). Everything the relation cannot relate stays distinct: under-linking
+costs coverage, never soundness.
+
+Segmentation is scope-tight: single-token name/class/verb/object shapes
+only (`<name> <verb> [<obj>]`, `does not`, sentential-not, `all|every|each|
+no [the] <class> <verb> [<obj>]`); anything longer refuses typed — without a
+lexicon there is no sound split of an arbitrary copula-free run.
+
+## Earned licenses
+
+Four new bands — `en_verb_universal`, `en_verb_chain`, `en_verb_negative`,
+`en_verb_fact` — each 720/720 committed, wrong=0, first seal run; ledger
+resealed at **21 bands** (12,240 + 2,880 committed). The synthetic verb pool
+exercises every rule of the closed agreement relation, so the license
+certifies the linking itself. Corpus soundness asserted case-by-case against
+the independent truth-table oracle over each template's INTENDED lowering
+(no reader in the loop, INV-25) before sealing.
+
+Lane: `evals/deduction_serve/v2_verb` — 28 hand-authored real-English cases
+(11 entailed / 4 refuted / 5 unknown / 8 declined), 28/28 first run; full
+lane now 134/134 wrong=0 across five splits. Gates: verb reader tests 34,
+deduction battery 86, smoke + warmed_session via pre-push.
+
+## Wrinkles worth surfacing
+
+1. **Adverb-as-object misreading (disclosed, not fixed):** "Lena runs
+   quickly" parses as verb+object ("quickly" an opaque term). Never unsound
+   — worst case an over-scoped UNKNOWN — but it is a real misreading the
+   3-token shape cannot detect without a lexicon. ADR-0260 §5.2 documents
+   it; the vocab-boundary instrument (plan Phase 3.1) is where a principled
+   fix would come from.
+2. **Arity subsumption stays UNKNOWN:** "teaches" ⊬ "teaches logic" and
+   conversely — the face-value posture v2-EN already takes, now visible on
+   verbs. A human reads the intransitive as subsuming; the scoped UNKNOWN
+   phrasing carries the honesty.
+3. **Plural verb-fact subjects read as individuals:** "dogs bark" is an
+   individual named "dogs" in this fragment (no copula ⇒ no plural signal in
+   the closed grammar). The membership analogue stays refused by v3-MEM's
+   bare-plural guard.
+4. **`doesn't` is not expanded** by the shared tokenizer's contraction
+   table (only isn't/aren't/wasn't/weren't are) — so "The engine doesn't
+   start" still refuses via the `n't` guard, preserving the e2e
+   out-of-regime test byte-for-byte. Adding verb contractions is a
+   deliberate non-goal until the tense scope-out is faced whole.
+
+## Stacking note
+
+This branch stacks on `feat/generalization-phase0` (merge that PR first):
+both touch `scripts/verify_lane_shas.py` / `CLAIMS.md`, and the claims
+generator's `_LANE_ADR` fix lands there.
+
+## Next (per the plan's tier assignment)
+
+Tier O (Opus): Band v6-EX existential witnesses (Phase 1.2), then the
+Phase-2 physics lane against the §4 curriculum-entailment contract — for
+which this band was the gate.
--- a/evals/deduction_serve/contract.md
+++ b/evals/deduction_serve/contract.md
@ -9,7 +9,8 @@ The **production serving decider** — the exact pipeline
 → `to_syllogism` + the categorical decider (Band v1b, ADR-0256) →
 `read_english_argument` (Band v2-EN, ADR-0257) → `read_member_argument`
 (Band v3-MEM, ADR-0258) → `read_cond_member_argument` (Band v4-CM,
-ADR-0259) — with `evaluate_entailment_with_trace` (the ROBDD engine,
+ADR-0259) → `read_verb_argument` (Band v5-VP, ADR-0260) — with
+`evaluate_entailment_with_trace` (the ROBDD engine,
 ADR-0201/ADR-0218) deciding every band.
 `evals/deduction_serve/runner.py::decide` calls these functions directly
 (typed outcome, not rendered prose) — the same production decision the
@ -29,6 +30,10 @@ against wording-only changes.
  membership sentence reading, incl. genuine universal+connective fusion
  cases (a bare universal's instantiated atom unifying with a connective
  leaf's atom).
+- `v2_verb/` — hand-authored verb-predicate arguments (ADR-0260): verb
+  universals discharged by membership facts across every closed agreement
+  rule (+s, +es, y↔ies, irregular go/goes), transitive objects at face
+  value, and eight typed decline shapes.

 This is **distinct** from two existing lanes that sound similar:

@ -91,12 +96,21 @@ decides for that exact text.
  — the first promotion in this corpus that does not land on `entailed`,
  because the promoted band's own correct answer for THIS text is a
  non-commitment, not a new capability to showcase.
- **Still-open declines** (honest, typed): verb-phrase negation
-  (`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`), nested
-  conditionals (`ds-en-0026`), existential quantifiers / bare plurals /
-  definite descriptions / relative clauses / tense
+- **Verb predicates** — refused by every band until Band v5-VP (ADR-0260)
+  decided them (`v2_verb/`). NO existing case promoted: every remaining
+  decline in the older splits uses contraction negation ("doesn't" — not
+  in the shared tokenizer's expansion table, so v5's `n't` guard refuses
+  identically) or structure v5 also guards out; the full lane's prior
+  splits stayed byte-stable.
+- **Still-open declines** (honest, typed): verb-phrase contraction
+  negation (`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`),
+  nested conditionals (`ds-en-0026`), existential quantifiers / bare
+  plurals / definite descriptions / relative clauses / tense
  (`ds-mem-0020…0023/0025/0026`), a universal clause nested inside a
-  connective, compound conclusions (`ds-cm-0020…0026`).
+  connective, compound conclusions (`ds-cm-0020…0026`), and the verb
+  band's own scope-outs — `did not` tense, multi-token subjects,
+  prepositional/ditransitive shapes, connective×verb composition
+  (`ds-vb-0021…0028`).

 ## Reproduce

--- a/evals/deduction_serve/practice/gold.py
+++ b/evals/deduction_serve/practice/gold.py
@ -37,6 +37,7 @@ from generate.proof_chain.cond_member import CondMemberArgument, read_cond_membe
 from generate.proof_chain.english import EnglishArgument, read_english_argument
 from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
 from generate.proof_chain.member import MemberArgument, read_member_argument
+from generate.proof_chain.verb import VerbArgument, read_verb_argument
 from generate.proof_chain.shape import (
    ATOMIC,
    CATEGORICAL,
@ -56,6 +57,10 @@ from generate.proof_chain.shape import (
    EN_MEMBER_NEGATIVE,
    EN_MEMBER_SINGLE,
    classify_deduction_shape,
+    EN_VERB_CHAIN,
+    EN_VERB_FACT,
+    EN_VERB_NEGATIVE,
+    EN_VERB_UNIVERSAL,
 )

 _DOMAIN_ID = "deductive_logic_serve"
@ -501,13 +506,161 @@ _CM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
 }


+# --- Band v5-VP (ADR-0260): verb-predicate synthetic corpus -------------------
+#
+# Reuses the v3-MEM name/class pools and adds a verb-forms pool that exercises
+# EVERY rule of the reader's closed verb-agreement relation — +s (bark/barks,
+# run/runs, live/lives), +es after sibilants (teach/teaches, push/pushes,
+# watch/watches, mix/mixes), y↔ies (study/studies, carry/carries, fly/flies),
+# and the irregular table (go/goes, have/has) — so the earned license
+# certifies the agreement linking itself, not just the sentence grammar.
+# Content is synthetic ON PURPOSE (same posture as the v2-EN / v3-MEM corpora);
+# hand-authored real-English cases live in ``evals/deduction_serve/v2_verb``.
+
+_VERB_FORMS: tuple[tuple[str, str], ...] = (
+    ("teach", "teaches"), ("bark", "barks"), ("study", "studies"),
+    ("go", "goes"), ("run", "runs"), ("push", "pushes"),
+    ("carry", "carries"), ("watch", "watches"), ("live", "lives"),
+    ("fly", "flies"), ("mix", "mixes"), ("have", "has"),
+)
+_VERB_OBJECTS: tuple[str, ...] = (
+    "logic", "music", "bread", "stones", "rivers", "wool",
+    "grain", "tools", "maps", "songs", "boats", "lamps",
+)
+
+
+def _verb_case(
+    index: int,
+) -> tuple[str, str, tuple[str, str], tuple[str, str], tuple[str, str], tuple[str, str], str]:
+    """Deterministic (name1, name2, class1, class2, verb1, verb2, object) for
+    case ``index`` — names, classes, and verbs are pairwise distinct."""
+    n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)]
+    n2 = _MEM_NAMES[(index * 3 + 1) % len(_MEM_NAMES)]
+    base = (index * 5) % (len(_MEM_CLASSES) - 1)
+    c1, c2 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1]
+    vbase = (index * 7) % (len(_VERB_FORMS) - 1)
+    v1, v2 = _VERB_FORMS[vbase], _VERB_FORMS[vbase + 1]
+    ob = _VERB_OBJECTS[(index * 11) % len(_VERB_OBJECTS)]
+    return n1, n2, c1, c2, v1, v2, ob
+
+
+#: Verb-band templates: (gold, text_builder, intended_premises, intended_query).
+#: Builders take ``(n1, n2, c1, c2, v1, v2, ob)`` from ``_verb_case``; the
+#: INTENDED formulas are the template's per-individual lowering over fixed
+#: placeholder atoms (``ma``… membership, ``va``… verb), cross-checked against
+#: the truth-table oracle with no reader in the loop (INV-25). Every template's
+#: text is a shape the earlier bands REFUSE (quantifier-led verb universal,
+#: is-a + verb mix, or ``does not`` negation), so the arena exercises exactly
+#: the fall-through path serving uses.
+_VERB_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
+    EN_VERB_UNIVERSAL: (
+        # Instantiated modus ponens onto an intransitive verb.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n1} {v1[1]}.",
+         ("ma", "ma implies vb"), "vb"),
+        # "every" spelling, singular class + 3sg verb, transitive.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"Every {c1[0]} {v1[1]} {ob}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.",
+         ("ma implies vb", "ma"), "vb"),
+        # "each" spelling, universal first — order independence.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"Each {c1[0]} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]}.",
+         ("ma implies vb", "ma"), "vb"),
+        # Contradicting the instantiated verb.
+        ("refuted",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("ma", "ma implies vb"), "not vb"),
+        # The universal binds a DIFFERENT named individual than the conclusion's.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n2} {v1[1]}.",
+         ("ma", "ma implies vb", "mc implies vd"), "vd"),
+        # Affirming the consequent — the verb fact does not yield membership.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. All {c1[1]} {v1[0]}. Therefore {n1} is a {c1[0]}.",
+         ("vb", "ma implies vb"), "ma"),
+    ),
+    EN_VERB_CHAIN: (
+        # Membership chain discharging a verb universal.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} {v1[0]}. Therefore {n1} {v1[1]}.",
+         ("ma", "ma implies mb", "mb implies vc"), "vc"),
+        # Transitive, sentence order shuffled.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"All {c1[1]} are {c2[1]}. {n1} is a {c1[0]}. All {c2[1]} {v1[0]} {ob}. Therefore {n1} {v1[1]} {ob}.",
+         ("ma implies mb", "ma", "mb implies vc"), "vc"),
+        # Chain contradiction.
+        ("refuted",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("ma", "ma implies mb", "mb implies vc"), "not vc"),
+        # Broken chain — the subsumption points the wrong way.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c2[1]} are {c1[1]}. All {c2[1]} {v1[0]}. Therefore {n1} {v1[1]}.",
+         ("ma", "mb implies ma", "mb implies vc"), "vc"),
+        # Two verb universals — the wrong verb's rule cannot fire.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. All {c2[1]} {v2[0]}. Therefore {n1} {v2[1]}.",
+         ("ma", "ma implies vb", "mc implies vd"), "vd"),
+    ),
+    EN_VERB_NEGATIVE: (
+        # Instantiated E-form onto an intransitive verb.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("ma", "ma implies not vb"), "not vb"),
+        # A-chain into an E-form verb universal.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. No {c2[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("ma", "ma implies mb", "mb implies not vc"), "not vc"),
+        # Transitive E-form.
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]} {ob}. Therefore {n1} does not {v1[0]} {ob}.",
+         ("ma", "ma implies not vb"), "not vb"),
+        # Contradicting the E-form's instantiation.
+        ("refuted",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} {v1[1]}.",
+         ("ma", "ma implies not vb"), "vb"),
+        # Denied antecedent under an E-form — nothing follows.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is not a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("not ma", "ma implies not vb"), "not vb"),
+    ),
+    EN_VERB_FACT: (
+        # Negated fact restated through the sentential-not spelling (the
+        # ``does not`` form is what makes the earlier bands refuse).
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]}. Therefore it is not the case that {n1} {v1[1]}.",
+         ("not va",), "not va"),
+        # Selection beside an is-a anchor (the anchor forces the fall-through).
+        ("entailed",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]} {ob}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.",
+         ("va", "mb"), "va"),
+        # Contradicting a stated verb fact.
+        ("refuted",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} does not {v1[0]}.",
+         ("va", "mb"), "not va"),
+        # Negated transitive fact contradicted.
+        ("refuted",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]} {ob}. Therefore {n1} {v1[1]} {ob}.",
+         ("not va",), "va"),
+        # Arity is read at face value — intransitive does not yield transitive.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.",
+         ("va", "mb"), "vc"),
+        # Distinct verbs stay distinct.
+        ("unknown",
+         lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]}. Therefore {n1} does not {v2[0]}.",
+         ("not va",), "not vb"),
+    ),
+}
+
+
 #: Ledger band order: the five v1 bands, the four v2-EN bands, the four
-#: v3-MEM bands, then the four v4-CM bands.
+#: v3-MEM bands, the four v4-CM bands, then the four v5-VP bands.
 _ALL_BANDS: tuple[str, ...] = (
    CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL,
    EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC,
    EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC,
    EN_CONDMEM_FUSED, EN_CONDMEM_DISJUNCTIVE, EN_CONDMEM_CHAIN, EN_CONDMEM_CONDITIONAL,
+    EN_VERB_NEGATIVE, EN_VERB_CHAIN, EN_VERB_UNIVERSAL, EN_VERB_FACT,
 )


@ -521,6 +674,25 @@ def generate_problems(band: str, n: int) -> list[Problem]:
    logical form for the reader-independent oracle cross-check.
    """
    problems: list[Problem] = []
+    if band in _VERB_TEMPLATES:
+        templates = _VERB_TEMPLATES[band]
+        for i in range(n):
+            gold, builder, intended_premises, intended_query = templates[i % len(templates)]
+            problems.append(
+                Problem(
+                    problem_id=f"{band}-{i:04d}",
+                    class_name=band,
+                    payload={
+                        "text": builder(*_verb_case(i)),
+                        "gold": gold,
+                        "intended": {
+                            "premises": list(intended_premises),
+                            "query": intended_query,
+                        },
+                    },
+                )
+            )
+        return problems
    if band in _MEM_TEMPLATES or band in _CM_TEMPLATES:
        templates = _MEM_TEMPLATES[band] if band in _MEM_TEMPLATES else _CM_TEMPLATES[band]
        for i in range(n):
@ -644,6 +816,9 @@ class DeductionSolver:
            cond_member = self._attempt_cond_member(problem)
            if cond_member is not None:
                return cond_member
+            verb = self._attempt_verb(problem)
+            if verb is not None:
+                return verb
            return _DeductionAttempt(
                committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}",
                case_id=problem.problem_id, shape=problem.class_name,
@ -683,6 +858,9 @@ class DeductionSolver:
        cond_member = self._attempt_cond_member(problem)
        if cond_member is not None:
            return cond_member
+        verb = self._attempt_verb(problem)
+        if verb is not None:
+            return verb
        return _DeductionAttempt(
            committed=False, answer=None, reason="unprojectable",
            case_id=problem.problem_id, shape=problem.class_name,
@ -733,6 +911,21 @@ class DeductionSolver:
            case_id=problem.problem_id, shape=arg.band,
        )

+    def _attempt_verb(self, problem: Problem) -> _DeductionAttempt | None:
+        """Band v5-VP: the verb-predicate argument path, or ``None`` when the
+        reader refuses (the caller then records the honest decline)."""
+        arg = read_verb_argument(problem.payload["text"])
+        if not isinstance(arg, VerbArgument):
+            return None
+        outcome = evaluate_entailment_with_trace(
+            arg.premise_formulas, arg.query_formula
+        ).outcome
+        return _DeductionAttempt(
+            committed=outcome is not Entailment.REFUSED,
+            answer=_OUTCOME_TO_CLASS[outcome], reason="",
+            case_id=problem.problem_id, shape=arg.band,
+        )
+

@dataclass(frozen=True, slots=True)
 class ConstructionGoldTether:
--- a/evals/deduction_serve/report.json
+++ b/evals/deduction_serve/report.json
@ -1,8 +1,8 @@
 {
  "aggregate": {
-    "correct": 106,
+    "correct": 134,
    "declined": 0,
-    "n": 106,
+    "n": 134,
    "wrong": 0
  },
  "all_correct": true,
@ -97,6 +97,27 @@
        "wrong": 0
      },
      "n": 26
+    },
+    "v2_verb": {
+      "all_cases_correct": true,
+      "by_gold": {
+        "declined": 8,
+        "entailed": 11,
+        "refuted": 4,
+        "unknown": 5
+      },
+      "correct_by_gold": {
+        "declined": 8,
+        "entailed": 11,
+        "refuted": 4,
+        "unknown": 5
+      },
+      "counts": {
+        "correct": 28,
+        "declined": 0,
+        "wrong": 0
+      },
+      "n": 28
    }
  },
  "wrong_is_zero": true
--- a/evals/deduction_serve/runner.py
+++ b/evals/deduction_serve/runner.py
@ -49,6 +49,7 @@ from generate.proof_chain.cond_member import CondMemberArgument, read_cond_membe
 from generate.proof_chain.english import EnglishArgument, read_english_argument
 from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
 from generate.proof_chain.member import MemberArgument, read_member_argument
+from generate.proof_chain.verb import VerbArgument, read_verb_argument

 _ROOT = Path(__file__).resolve().parent

@ -66,6 +67,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = (
    # same content-disjoint discipline (connectives composed over singular-
    # membership clauses, incl. universal+connective fusion cases).
    ("v2_condmem", _ROOT / "v2_condmem" / "cases.jsonl"),
+    # Band v5-VP (ADR-0260) — hand-authored verb-predicate arguments, same
+    # content-disjoint discipline (verb agreement across +s/+es/y↔ies and the
+    # irregular table on real verbs: writes, debates, cries, goes).
+    ("v2_verb", _ROOT / "v2_verb" / "cases.jsonl"),
 )

 _OUTCOME_TO_CLASS = {
@ -142,6 +147,15 @@ def _decide_cond_member(text: str) -> str:
    """Band v4-CM fallback (ADR-0259) — mirrors ``_cond_member_band_surface``."""
    arg = read_cond_member_argument(text)
    if not isinstance(arg, CondMemberArgument):
+        return _decide_verb(text)
+    outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome
+    return _OUTCOME_TO_CLASS[outcome]
+
+
+def _decide_verb(text: str) -> str:
+    """Band v5-VP fallback (ADR-0260) — mirrors ``_verb_band_surface``."""
+    arg = read_verb_argument(text)
+    if not isinstance(arg, VerbArgument):
        return "declined"
    outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome
    return _OUTCOME_TO_CLASS[outcome]
--- a/evals/deduction_serve/v2_verb/cases.jsonl
+++ b/evals/deduction_serve/v2_verb/cases.jsonl
@ -0,0 +1,28 @@
+{"id": "ds-vb-0001", "text": "All poets write. Homer is a poet. Therefore Homer writes.", "gold": "entailed", "class": "verb_universal_modus_ponens"}
+{"id": "ds-vb-0002", "text": "Every senator debates policy. Cicero is a senator. Therefore Cicero debates policy.", "gold": "entailed", "class": "verb_universal_transitive"}
+{"id": "ds-vb-0003", "text": "Anselm is a monk. Each monk prays. Therefore Anselm prays.", "gold": "entailed", "class": "verb_universal_each_spelling"}
+{"id": "ds-vb-0004", "text": "Aristotle is a philosopher. All philosophers are scholars. All scholars read. Therefore Aristotle reads.", "gold": "entailed", "class": "verb_chain_membership"}
+{"id": "ds-vb-0005", "text": "All sparrows are birds. Jack is a sparrow. All birds build nests. Therefore Jack builds nests.", "gold": "entailed", "class": "verb_chain_transitive"}
+{"id": "ds-vb-0006", "text": "Miriam is a nun. No nuns marry. Therefore Miriam does not marry.", "gold": "entailed", "class": "verb_negative_e_form"}
+{"id": "ds-vb-0007", "text": "Felix is a tortoise. All tortoises are reptiles. No reptiles purr. Therefore Felix does not purr.", "gold": "entailed", "class": "verb_negative_chain"}
+{"id": "ds-vb-0008", "text": "Clara paints portraits. Clara is an artist. Therefore Clara paints portraits.", "gold": "entailed", "class": "verb_fact_selection"}
+{"id": "ds-vb-0009", "text": "Boris does not smoke. Therefore it is not the case that Boris smokes.", "gold": "entailed", "class": "verb_fact_negation_restated"}
+{"id": "ds-vb-0010", "text": "Every baby cries. Moses is a baby. Therefore Moses cries.", "gold": "entailed", "class": "verb_universal_ies_agreement"}
+{"id": "ds-vb-0011", "text": "All pilgrims go. Dante is a pilgrim. Therefore Dante goes.", "gold": "entailed", "class": "verb_universal_irregular_agreement"}
+{"id": "ds-vb-0012", "text": "All owls hunt. Hedwig is an owl. Therefore Hedwig does not hunt.", "gold": "refuted", "class": "verb_universal_contradiction"}
+{"id": "ds-vb-0013", "text": "Petra is a judge. No judges gossip. Therefore Petra gossips.", "gold": "refuted", "class": "verb_negative_contradiction"}
+{"id": "ds-vb-0014", "text": "Omar swims. Omar is an athlete. Therefore Omar does not swim.", "gold": "refuted", "class": "verb_fact_contradiction"}
+{"id": "ds-vb-0015", "text": "Ida is a farmer. All farmers are workers. All workers vote. Therefore Ida does not vote.", "gold": "refuted", "class": "verb_chain_contradiction"}
+{"id": "ds-vb-0016", "text": "All monks chant. Basil is a monk. Therefore Gregory chants.", "gold": "unknown", "class": "verb_wrong_individual"}
+{"id": "ds-vb-0017", "text": "Nina sings. All larks sing. Therefore Nina is a lark.", "gold": "unknown", "class": "verb_affirming_consequent"}
+{"id": "ds-vb-0018", "text": "Viktor cooks. Viktor is a chef. Therefore Viktor cooks stew.", "gold": "unknown", "class": "verb_arity_face_value"}
+{"id": "ds-vb-0019", "text": "Rosa is not a lawyer. No lawyers whistle. Therefore Rosa does not whistle.", "gold": "unknown", "class": "verb_negative_denied_antecedent"}
+{"id": "ds-vb-0020", "text": "Edgar does not dance. Therefore Edgar does not skate.", "gold": "unknown", "class": "verb_distinct_lemmas"}
+{"id": "ds-vb-0021", "text": "Caesar did not surrender. Therefore Caesar surrenders.", "gold": "declined", "class": "tense_out_of_band"}
+{"id": "ds-vb-0022", "text": "The old sailor whittles. The old sailor is a craftsman. Therefore the old sailor whittles.", "gold": "declined", "class": "multi_token_subject_out_of_band"}
+{"id": "ds-vb-0023", "text": "Nero fiddles in Rome. Nero is an emperor. Therefore Nero fiddles.", "gold": "declined", "class": "prepositional_out_of_band"}
+{"id": "ds-vb-0024", "text": "Hannah gives Samuel bread. Hannah is a mother. Therefore Hannah gives Samuel bread.", "gold": "declined", "class": "ditransitive_out_of_band"}
+{"id": "ds-vb-0025", "text": "If Noah builds then Noah is a carpenter. Noah builds. Therefore Noah is a carpenter.", "gold": "declined", "class": "verb_connective_out_of_band"}
+{"id": "ds-vb-0026", "text": "Someone sneezes. Ora is a doctor. Therefore Ora sneezes.", "gold": "declined", "class": "quantifier_out_of_band"}
+{"id": "ds-vb-0027", "text": "Jonah preaches. Therefore all prophets preach.", "gold": "declined", "class": "universal_conclusion_out_of_band"}
+{"id": "ds-vb-0028", "text": "The twins do not quarrel. Therefore the twins quarrel.", "gold": "declined", "class": "plural_do_not_out_of_band"}
--- a/generate/proof_chain/render.py
+++ b/generate/proof_chain/render.py
@ -132,6 +132,43 @@ def render_entailment_member(
    return f"Given: {given}. I can't evaluate {query_text} from that as stated."


+def render_entailment_verb(
+    trace: EntailmentTrace, premise_texts: tuple[str, ...], query_text: str
+) -> str:
+    """The user-facing surface for a verb-predicate (Band v5-VP) verdict.
+
+    Same discipline as :func:`render_entailment_member`; the UNKNOWN template
+    additionally scopes the verb reading (ADR-0260 §3): each verb phrase is
+    read at face value — an unlinked agreement form or an unstated relation
+    between a verb and a class word could settle what the lowering leaves
+    open, so the claim is stated of the reading, disclosed as such. ENTAILED /
+    REFUTED / inconsistent survive any such refinement (instantiation is
+    sound and entailment is monotone) and are stated at full strength.
+    """
+    given = "; ".join(premise_texts)
+    if trace.outcome is Entailment.ENTAILED:
+        return f"Given: {given}. Your premises entail: {query_text}."
+    if trace.outcome is Entailment.REFUTED:
+        return (
+            f"Given: {given}. Your premises entail the opposite of "
+            f"{query_text} — it cannot hold."
+        )
+    if trace.outcome is Entailment.UNKNOWN:
+        return (
+            f"Given: {given}. Reading each name as one individual and each "
+            f"class word and verb phrase at face value, your premises don't "
+            f"settle whether {query_text} — it holds in some cases and fails "
+            f"in others."
+        )
+    # REFUSED
+    if trace.reason == INCONSISTENT_PREMISES:
+        return (
+            f"Given: {given}. Those premises are inconsistent — they "
+            f"can't all be true, so I won't assert anything from them."
+        )
+    return f"Given: {given}. I can't evaluate {query_text} from that as stated."
+
+
 def _categorical_clause(prop: dict) -> str:
    """One categorical proposition dict → its English clause."""
    template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}")
@ -169,5 +206,6 @@ __all__ = [
    "render_entailment",
    "render_entailment_english",
    "render_entailment_member",
+    "render_entailment_verb",
    "render_syllogism",
 ]
--- a/generate/proof_chain/shape.py
+++ b/generate/proof_chain/shape.py
@ -95,9 +95,27 @@ EN_CONDMEM_BANDS: tuple[str, ...] = (
    EN_CONDMEM_CONDITIONAL,
 )

+#: Band v5-VP (ADR-0260) — verb-predicate arguments ("All philosophers teach.
+#: Socrates is a philosopher. Therefore Socrates teaches."), read by
+#: ``generate.proof_chain.verb`` via per-individual lowering with a second
+#: (individual, verb-group, object) atom family alongside v3-MEM's membership
+#: atoms. Same ``en_`` license discipline: a different reader must earn its
+#: own per-shape record. Priority order: negative > chain > universal > fact.
+EN_VERB_NEGATIVE = "en_verb_negative"
+EN_VERB_CHAIN = "en_verb_chain"
+EN_VERB_UNIVERSAL = "en_verb_universal"
+EN_VERB_FACT = "en_verb_fact"
+
+EN_VERB_BANDS: tuple[str, ...] = (
+    EN_VERB_NEGATIVE,
+    EN_VERB_CHAIN,
+    EN_VERB_UNIVERSAL,
+    EN_VERB_FACT,
+)
+
 #: Every serving shape-band — the ratified ledger's full key set.
 ALL_SHAPE_BANDS: tuple[str, ...] = (
-    SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS
+    SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS + EN_VERB_BANDS
 )


@ -147,6 +165,11 @@ __all__ = [
    "EN_MEMBER_NEGATIVE",
    "EN_MEMBER_SINGLE",
    "EN_SHAPE_BANDS",
+    "EN_VERB_BANDS",
+    "EN_VERB_CHAIN",
+    "EN_VERB_FACT",
+    "EN_VERB_NEGATIVE",
+    "EN_VERB_UNIVERSAL",
    "SHAPE_BANDS",
    "classify_deduction_shape",
 ]
--- a/generate/proof_chain/verb.py
+++ b/generate/proof_chain/verb.py
@ -0,0 +1,518 @@
+"""Verb-predicate argument reader — Band v5-VP (ADR-0260).
+
+Reads deductive arguments whose facts are VERB sentences — "All philosophers
+teach. Socrates is a philosopher. Therefore Socrates teaches." — by extending
+Band v3-MEM's per-individual propositional lowering with a second atom family:
+one opaque minted atom per *(individual, verb-lemma-group, object-term)*
+triple, alongside v3-MEM's *(individual, class-group)* membership atoms, in
+ONE shared atom space. A verb universal ("all C <verb> [obj]", "no C <verb>
+[obj]") instantiates at every named individual as ``mem(i,C) -> [~]verb(i)``,
+so a membership fact minted by the copula reading can discharge a verb rule —
+the fusion this band exists for. The same verified ROBDD engine decides.
+
+Why this is sound (ADR-0260 §3): identical to ADR-0258 §3's argument.
+Universal instantiation at named individuals is truth-preserving in every
+first-order model; each *(verb-group, object-term)* pair is one opaque unary
+predicate over the same named-individual domain, so ENTAILED / REFUTED /
+inconsistent verdicts over the lowered premises hold in every model of the
+original argument. Completeness within the fragment lifts the same way: a
+propositional countermodel becomes a first-order countermodel whose domain is
+exactly the named individuals. The ONE semantic identification added over
+v3-MEM is third-person-singular agreement — a universal's base verb form
+("teach") and a singular fact's 3sg form ("teaches") are identified iff
+related by a CLOSED relation: a verb-specific irregular table (consulted
+first, sole authority for its tokens) else the three regular suffix rules
+(``+s``, ``+es`` after sibilants, ``y↔ies``). NOUN morphology is deliberately
+NOT reused for verbs — the noun table would misroute forms like "lives"
+(noun: life; verb: live). Anything the relation cannot relate stays distinct:
+under-linking costs coverage, never soundness. Object terms link by exact
+token identity only.
+
+Segmentation is scope-tight by design: without a lexicon there is no sound
+way to split an arbitrary copula-free token run into subject/verb/object, so
+this band reads EXACTLY ``<name> <verb>``, ``<name> <verb> <object>``, their
+``does not`` negations, the sentential-not prefix, and universals
+``all|every|each|no [the] <class> <verb> [<object>]`` — single-token name,
+class, verb, and object. Everything longer or differently shaped refuses,
+typed. Copula sentences delegate VERBATIM to v3-MEM's own ``_parse_singular``
+/ ``_parse_universal`` (membership facts and is-a universals coexist with
+verb sentences in one argument). Connective composition with verb leaves is a
+deliberate scope-out (ADR-0260 §5) — any connective token refuses.
+
+Tried strictly AFTER Bands v1 / v1b / v2-EN / v3-MEM / v4-CM (a fallback
+tier) — pure widening; every previously-served argument is served
+byte-identically. (v2-EN decides pure verb-fact restatements as opaque
+clause-atoms already — soundly — so every argument that reaches this band
+contains a quantifier lead, an is-a shape, or unnormalized negation that made
+the earlier bands refuse.) Refusal-first, closed reason vocabulary:
+
+  ``empty``, ``question_sentence``, ``no_conclusion``,
+  ``multiple_conclusions``, ``conclusion_not_last``, ``no_premises``,
+  ``empty_side``, ``quantifier_out_of_band``, ``bare_plural_out_of_band``,
+  ``definite_description_out_of_band``, ``relative_clause_out_of_band``,
+  ``universal_conclusion_out_of_band``, ``mixed_structure_out_of_band``,
+  ``internal_negation_unread``, ``sentence_shape_out_of_band``,
+  ``tense_out_of_band``, ``structural_leak``, ``too_many_premises``,
+  ``too_many_atoms``.
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+
+# The v2-EN sentence splitter and tokenizer are reused VERBATIM (one
+# normalization discipline across every argument band), and v3-MEM's singular/
+# universal copula parsers, token-run guard, noun-morphology linker, and
+# sibilant set are reused VERBATIM — deliberate private-name imports inside
+# the proof_chain package, same precedent as generate.proof_chain.member and
+# generate.proof_chain.cond_member.
+from generate.proof_chain.english import _SENTENCE_RE, _tokenize
+from generate.proof_chain.member import (
+    _A_LEADS,
+    _COPULA_FORMS,
+    _E_LEAD,
+    _QUANTIFIER_TOKENS,
+    _SENTENTIAL_NOT,
+    _SIBILANT_ENDINGS,
+    _Singular,
+    _Universal,
+    _check_run,
+    _forms_link,
+    _parse_singular,
+    _parse_universal,
+)
+from generate.proof_chain.member import _Reject as _MemberReject
+from generate.proof_chain.shape import (
+    EN_VERB_CHAIN,
+    EN_VERB_FACT,
+    EN_VERB_NEGATIVE,
+    EN_VERB_UNIVERSAL,
+)
+
+#: Connective structure this band does not compose (a future band fuses the
+#: v2-EN/v4-CM connective grammar with verb sentences — ADR-0260 §5).
+_CONNECTIVES = frozenset({"if", "then", "or", "and", "either"})
+
+#: Auxiliary/determiner tokens that can never BE the verb or object of an
+#: in-band sentence. ``does`` is consumed only by the exact ``does not``
+#: negation shape; ``did not`` is past tense (a scope-out); bare ``do not``
+#: with a singular subject is not an in-band agreement pattern.
+_ARTICLES = frozenset({"a", "an", "the"})
+_AUXILIARIES = frozenset({"do", "does", "did"})
+
+#: Closed irregular 3sg table (3sg form → base). Consulted BEFORE the regular
+#: suffix rules; table membership makes it the sole authority for that token.
+#: Deliberately verb-specific — the noun table (member.py) would misroute
+#: forms like "lives" (noun: life; verb: live).
+_VERB_IRREGULAR_3SG: dict[str, str] = {
+    "has": "have",
+    "goes": "go",
+    "does": "do",
+}
+_VERB_TABLE_TOKENS = frozenset(_VERB_IRREGULAR_3SG) | frozenset(
+    _VERB_IRREGULAR_3SG.values()
+)
+
+#: Honesty caps — beyond these the argument is refused, never truncated.
+#: ``MAX_ATOMS`` counts minted atoms of BOTH families, so instantiation
+#: fan-out is capped exactly where it multiplies.
+MAX_PREMISE_SENTENCES = 16
+MAX_ATOMS = 24
+
+
+@dataclass(frozen=True, slots=True)
+class VerbArgument:
+    """A successfully-read verb-predicate argument, engine-ready.
+
+    Same shape as ``MemberArgument``: ``premise_formulas``/``query_formula``
+    are propositional formula strings over minted atom ids; ``atoms[i]``
+    displays the fact behind ``a{i}`` (``individual : class`` for membership
+    atoms, ``individual : verb [object]`` for verb atoms).
+    """
+
+    premise_formulas: tuple[str, ...]
+    query_formula: str
+    premise_texts: tuple[str, ...]
+    query_text: str
+    band: str
+    atoms: tuple[str, ...]
+
+
+@dataclass(frozen=True, slots=True)
+class VerbRefusal:
+    """A typed refusal — the argument is not honestly readable by this band."""
+
+    reason: str
+    detail: str = ""
+
+
+class _Reject(Exception):
+    def __init__(self, reason: str, detail: str = "") -> None:
+        super().__init__(reason)
+        self.refusal = VerbRefusal(reason, detail)
+
+
+@dataclass(frozen=True, slots=True)
+class _VerbFact:
+    """``<NAME> <verb3sg> [<object>]`` (optionally ``does not`` / sentential-
+    not negated) — a verb literal about one individual."""
+
+    ind: tuple[str, ...]
+    verb: str
+    obj: str | None
+    negated: bool
+
+
+@dataclass(frozen=True, slots=True)
+class _VerbUniversal:
+    """``all|every|each|no [the] <class> <verb> [<object>]`` — instantiated
+    per individual at lowering time as ``mem(i, class) -> [~]verb(i)``.
+    ``negative`` marks the E-form (``no``)."""
+
+    subject: tuple[str, ...]
+    verb: str
+    obj: str | None
+    negative: bool
+
+
+_Record = _Singular | _Universal | _VerbFact | _VerbUniversal
+
+
+def _verb_tokens_link(a: str, b: str) -> bool:
+    """True iff single tokens *a* and *b* are agreement forms of one verb
+    lemma under the closed relation (irregular table first, then the three
+    regular 3sg suffix rules)."""
+    if a == b:
+        return True
+    if a in _VERB_TABLE_TOKENS or b in _VERB_TABLE_TOKENS:
+        return _VERB_IRREGULAR_3SG.get(a) == b or _VERB_IRREGULAR_3SG.get(b) == a
+    short, long_ = (a, b) if len(a) <= len(b) else (b, a)
+    if long_ == short + "s" and not short.endswith(_SIBILANT_ENDINGS):
+        return True
+    if long_ == short + "es" and short.endswith(_SIBILANT_ENDINGS):
+        return True
+    if short.endswith("y") and long_ == short[:-1] + "ies":
+        return True
+    return False
+
+
+def _check_verb_token(tok: str, detail: str) -> None:
+    """Guard the verb slot: the shared opaque-run guard plus the aux/article
+    exclusions (an auxiliary or determiner is never an in-band verb lemma)."""
+    _check_run((tok,), detail)
+    if tok in _ARTICLES or tok in _AUXILIARIES:
+        raise _Reject("sentence_shape_out_of_band", detail)
+
+
+def _check_term_token(tok: str, detail: str) -> None:
+    """Guard a name/object slot: the shared opaque-run guard plus a dangling-
+    determiner check."""
+    _check_run((tok,), detail)
+    if tok in _ARTICLES:
+        raise _Reject("sentence_shape_out_of_band", detail)
+
+
+def _parse_verb_fact(toks: list[str], detail: str) -> _VerbFact:
+    """``<name> <verb> [<obj>]`` / ``<name> does not <verb> [<obj>]``."""
+    negated = False
+    if len(toks) >= 3 and toks[1] in _AUXILIARIES and toks[2] == "not":
+        if toks[1] == "did":
+            raise _Reject("tense_out_of_band", detail)
+        if toks[1] == "do":
+            raise _Reject("sentence_shape_out_of_band", detail)
+        negated = True
+        toks = [toks[0], *toks[3:]]
+    if any(t == "not" or t.endswith("n't") for t in toks):
+        raise _Reject("internal_negation_unread", detail)
+    if len(toks) < 2 or len(toks) > 3:
+        raise _Reject("sentence_shape_out_of_band", detail)
+    name, verb = toks[0], toks[1]
+    obj = toks[2] if len(toks) == 3 else None
+    _check_term_token(name, detail)
+    _check_verb_token(verb, detail)
+    if obj is not None:
+        _check_term_token(obj, detail)
+    return _VerbFact((name,), verb, obj, negated)
+
+
+def _parse_verb_universal(toks: list[str], detail: str) -> _VerbUniversal:
+    """``all|every|each|no [the] <class> <verb> [<obj>]`` — no copula form."""
+    negative = toks[0] == _E_LEAD
+    rest = toks[1:]
+    if rest and rest[0] == "the":  # "all the dogs bark" — determiner, dropped
+        rest = rest[1:]
+    if any(t == "not" or t.endswith("n't") for t in rest):
+        # "All men do not teach" — scope-ambiguous (¬∀ vs ∀¬); the E-form
+        # ("no …") is the unambiguous spelling this band reads.
+        raise _Reject("internal_negation_unread", detail)
+    if any(t == "did" for t in rest):
+        raise _Reject("tense_out_of_band", detail)
+    if len(rest) < 2 or len(rest) > 3:
+        raise _Reject("sentence_shape_out_of_band", detail)
+    cls, verb = rest[0], rest[1]
+    obj = rest[2] if len(rest) == 3 else None
+    _check_term_token(cls, detail)
+    _check_verb_token(verb, detail)
+    if obj is not None:
+        _check_term_token(obj, detail)
+    return _VerbUniversal((cls,), verb, obj, negative)
+
+
+def _parse_fact(toks: list[str], detail: str) -> _Singular | _VerbFact:
+    """A non-universal sentence: sentential-not unwraps first (its prefix
+    contains a copula, so it must be checked before copula routing); then a
+    copula routes to v3-MEM's own singular parser (membership fact), else the
+    verb-fact grammar."""
+    if tuple(toks[: len(_SENTENTIAL_NOT)]) == _SENTENTIAL_NOT:
+        inner = _parse_fact(toks[len(_SENTENTIAL_NOT) :], detail)
+        if isinstance(inner, _Singular):
+            return _Singular(inner.ind, inner.cls, negated=not inner.negated)
+        return _VerbFact(inner.ind, inner.verb, inner.obj, negated=not inner.negated)
+    if not toks:
+        raise _Reject("empty_side", detail)
+    if any(t in _COPULA_FORMS for t in toks):
+        return _parse_singular(toks, detail)
+    return _parse_verb_fact(toks, detail)
+
+
+def _parse_sentence(toks: list[str], detail: str) -> _Record:
+    if any(t in _CONNECTIVES for t in toks):
+        raise _Reject("mixed_structure_out_of_band", detail)
+    head = toks[0]
+    if head in _A_LEADS or head == _E_LEAD:
+        if any(t in ("is", "are") for t in toks):
+            return _parse_universal(toks, detail)  # is-a universal (v3-MEM's)
+        return _parse_verb_universal(toks, detail)
+    if head in _QUANTIFIER_TOKENS:
+        raise _Reject("quantifier_out_of_band", detail)
+    return _parse_fact(toks, detail)
+
+
+def read_verb_argument(text: str) -> VerbArgument | VerbRefusal:
+    """Read *text* as a verb-predicate argument, or refuse (typed).
+
+    Deterministic and pure: same text → same ``VerbArgument``. The conclusion
+    is the final sentence, the sole "therefore"-led one, and must be a
+    singular fact (membership or verb); every earlier sentence is a premise.
+    Lowering is two-pass exactly as v3-MEM's — sentences parse first, THEN
+    individuals / class-groups / verb-groups are collected, THEN atoms mint
+    and universals instantiate at every named individual — with premise
+    formulas emitted in sentence order.
+    """
+    if not text or not text.strip():
+        return VerbRefusal("empty")
+    sentences = [
+        (m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip()
+    ]
+    if not sentences:
+        return VerbRefusal("empty")
+
+    premises: list[_Record] = []
+    premise_texts: list[str] = []
+    conclusion: _Singular | _VerbFact | None = None
+    query_text: str | None = None
+
+    try:
+        for idx, (body, terminator) in enumerate(sentences):
+            if terminator == "?":
+                raise _Reject("question_sentence", body)
+            toks = _tokenize(body)
+            if not toks:
+                continue
+            if toks[0] == "therefore":
+                if conclusion is not None:
+                    raise _Reject("multiple_conclusions", body)
+                if idx != len(sentences) - 1:
+                    raise _Reject("conclusion_not_last", body)
+                rest = toks[1:]
+                if not rest:
+                    raise _Reject("empty_side", body)
+                if any(t in _CONNECTIVES for t in rest):
+                    raise _Reject("mixed_structure_out_of_band", body)
+                if rest[0] in _A_LEADS or rest[0] == _E_LEAD:
+                    raise _Reject("universal_conclusion_out_of_band", body)
+                if rest[0] in _QUANTIFIER_TOKENS:
+                    raise _Reject("quantifier_out_of_band", body)
+                conclusion = _parse_fact(rest, body)
+                query_text = " ".join(rest)
+                continue
+            if len(premises) >= MAX_PREMISE_SENTENCES:
+                raise _Reject("too_many_premises", body)
+            premises.append(_parse_sentence(toks, body))
+            premise_texts.append(" ".join(toks))
+
+        if conclusion is None or query_text is None:
+            return VerbRefusal("no_conclusion")
+        if not premises:
+            return VerbRefusal("no_premises")
+
+        records: list[_Record] = [*premises, conclusion]
+
+        # Every argument this band DECIDES contains at least one verb
+        # construct — a pure-copula argument is v3-MEM/v4-CM territory (and
+        # only ever reaches here when those bands refused it, in which case
+        # the delegated parsers above raised the same typed refusal already;
+        # this check is a defensive closure of that invariant).
+        if not any(isinstance(r, (_VerbFact, _VerbUniversal)) for r in records):
+            raise _Reject("sentence_shape_out_of_band", "no verb predicate read")
+
+        # --- lowering (ADR-0260 §2): v3-MEM's two-pass scheme, two families --
+        individuals: list[tuple[str, ...]] = []
+        for rec in records:
+            if isinstance(rec, (_Singular, _VerbFact)) and rec.ind not in individuals:
+                individuals.append(rec.ind)
+
+        # Class groups — the SAME closed noun-morphology relation as v3-MEM.
+        cls_group_of: dict[tuple[str, ...], int] = {}
+        cls_reps: list[tuple[str, ...]] = []
+        for rec in records:
+            forms: list[tuple[str, ...]] = []
+            if isinstance(rec, _Singular):
+                forms = [rec.cls]
+            elif isinstance(rec, _Universal):
+                forms = [rec.subject, rec.predicate]
+            elif isinstance(rec, _VerbUniversal):
+                forms = [rec.subject]
+            for form in forms:
+                if form in cls_group_of:
+                    continue
+                for gi, rep in enumerate(cls_reps):
+                    if _forms_link(form, rep):
+                        cls_group_of[form] = gi
+                        break
+                else:
+                    cls_group_of[form] = len(cls_reps)
+                    cls_reps.append(form)
+
+        # Verb groups — the closed verb-agreement relation (this band's one
+        # new semantic identification).
+        verb_group_of: dict[str, int] = {}
+        verb_reps: list[str] = []
+        for rec in records:
+            if not isinstance(rec, (_VerbFact, _VerbUniversal)):
+                continue
+            form = rec.verb
+            if form in verb_group_of:
+                continue
+            for gi, rep in enumerate(verb_reps):
+                if _verb_tokens_link(form, rep):
+                    verb_group_of[form] = gi
+                    break
+            else:
+                verb_group_of[form] = len(verb_reps)
+                verb_reps.append(form)
+
+        mint: dict[tuple, str] = {}
+        atom_display: list[str] = []
+
+        def _mint(key: tuple, display: str, detail: str) -> str:
+            if key not in mint:
+                if len(atom_display) >= MAX_ATOMS:
+                    raise _Reject("too_many_atoms", detail)
+                mint[key] = f"a{len(atom_display)}"
+                atom_display.append(display)
+            return mint[key]
+
+        def mem_atom(ind_idx: int, group: int, detail: str) -> str:
+            return _mint(
+                ("mem", ind_idx, group),
+                f"{' '.join(individuals[ind_idx])} : {' '.join(cls_reps[group])}",
+                detail,
+            )
+
+        def verb_atom(ind_idx: int, group: int, obj: str | None, detail: str) -> str:
+            shown = verb_reps[group] if obj is None else f"{verb_reps[group]} {obj}"
+            return _mint(
+                ("verb", ind_idx, group, obj),
+                f"{' '.join(individuals[ind_idx])} : {shown}",
+                detail,
+            )
+
+        premise_formulas: list[str] = []
+        for rec, body_text in zip(premises, premise_texts):
+            if isinstance(rec, _Singular):
+                atom = mem_atom(
+                    individuals.index(rec.ind), cls_group_of[rec.cls], body_text
+                )
+                premise_formulas.append(f"~({atom})" if rec.negated else atom)
+            elif isinstance(rec, _VerbFact):
+                atom = verb_atom(
+                    individuals.index(rec.ind),
+                    verb_group_of[rec.verb],
+                    rec.obj,
+                    body_text,
+                )
+                premise_formulas.append(f"~({atom})" if rec.negated else atom)
+            elif isinstance(rec, _Universal):
+                for ind_idx in range(len(individuals)):
+                    antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text)
+                    consequent = mem_atom(ind_idx, cls_group_of[rec.predicate], body_text)
+                    premise_formulas.append(
+                        f"({antecedent}) -> (~({consequent}))"
+                        if rec.negative
+                        else f"({antecedent}) -> ({consequent})"
+                    )
+            else:  # _VerbUniversal
+                for ind_idx in range(len(individuals)):
+                    antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text)
+                    consequent = verb_atom(
+                        ind_idx, verb_group_of[rec.verb], rec.obj, body_text
+                    )
+                    premise_formulas.append(
+                        f"({antecedent}) -> (~({consequent}))"
+                        if rec.negative
+                        else f"({antecedent}) -> ({consequent})"
+                    )
+
+        if isinstance(conclusion, _Singular):
+            query_atom = mem_atom(
+                individuals.index(conclusion.ind),
+                cls_group_of[conclusion.cls],
+                query_text,
+            )
+        else:
+            query_atom = verb_atom(
+                individuals.index(conclusion.ind),
+                verb_group_of[conclusion.verb],
+                conclusion.obj,
+                query_text,
+            )
+        query_formula = f"~({query_atom})" if conclusion.negated else query_atom
+    except (_Reject, _MemberReject) as rej:
+        # ``_parse_singular``/``_parse_universal`` are v3-MEM's own functions,
+        # reused verbatim — their failures raise v3-MEM's OWN ``_Reject``
+        # class (same shape, different identity), so both are caught here and
+        # normalized to THIS band's refusal type (the v4-CM lesson).
+        return VerbRefusal(rej.refusal.reason, rej.refusal.detail)
+
+    universals = [r for r in premises if isinstance(r, (_Universal, _VerbUniversal))]
+    if any(
+        (isinstance(u, _Universal) and u.negative)
+        or (isinstance(u, _VerbUniversal) and u.negative)
+        for u in universals
+    ):
+        band = EN_VERB_NEGATIVE
+    elif len(universals) >= 2:
+        band = EN_VERB_CHAIN
+    elif len(universals) == 1:
+        band = EN_VERB_UNIVERSAL
+    else:
+        band = EN_VERB_FACT
+
+    return VerbArgument(
+        premise_formulas=tuple(premise_formulas),
+        query_formula=query_formula,
+        premise_texts=tuple(premise_texts),
+        query_text=query_text,
+        band=band,
+        atoms=tuple(atom_display),
+    )
+
+
+__all__ = [
+    "MAX_ATOMS",
+    "MAX_PREMISE_SENTENCES",
+    "VerbArgument",
+    "VerbRefusal",
+    "read_verb_argument",
+]
--- a/scripts/verify_lane_shas.py
+++ b/scripts/verify_lane_shas.py
@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = {
    "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3",
    "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4",
    "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f",
-    "deduction_serve_v1": "b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be",
+    "deduction_serve_v1": "f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a",
 }


--- a/tests/test_deduction_serve_e2e.py
+++ b/tests/test_deduction_serve_e2e.py
@ -166,3 +166,16 @@ def test_out_of_regime_argument_refuses_honestly() -> None:
    resp = rt.chat("The engine doesn't start. Therefore the engine is broken.")
    assert resp.grounding_source == "deduction"
    assert "can't parse" in resp.surface  # honest reader-refusal disclosure
+
+
+def test_verb_predicate_is_decided_end_to_end() -> None:
+    """The ADR-0260 flagship: a verb universal discharged by a membership
+    fact, decided through the real REPL spine — closed 3sg agreement linking
+    the universal's base form to the conclusion's inflected form."""
+    rt = _runtime(True)
+    resp = rt.chat(
+        "All philosophers teach. Socrates is a philosopher. "
+        "Therefore Socrates teaches."
+    )
+    assert resp.grounding_source == "deduction"
+    assert "Your premises entail: socrates teaches" in resp.surface
--- a/tests/test_deduction_serve_lane.py
+++ b/tests/test_deduction_serve_lane.py
@ -15,6 +15,7 @@ _V1 = _ROOT / "v1" / "cases.jsonl"
 _V2_EN = _ROOT / "v2_en" / "cases.jsonl"
 _V2_MEMBER = _ROOT / "v2_member" / "cases.jsonl"
 _V2_CONDMEM = _ROOT / "v2_condmem" / "cases.jsonl"
+_V2_VERB = _ROOT / "v2_verb" / "cases.jsonl"


 def test_v1_lane_wrong_is_zero() -> None:
@ -89,6 +90,22 @@ def test_v2_condmem_lane_wrong_is_zero() -> None:
    assert cbg.get("declined", 0) >= 7


+def test_v2_verb_lane_wrong_is_zero() -> None:
+    """Band v5-VP (ADR-0260): hand-authored verb-predicate arguments —
+    universals discharged by membership facts across every closed agreement
+    rule (+s, +es, y↔ies, irregular go/goes), transitive objects at face
+    value, and eight distinct honest-decline shapes — decided wrong=0."""
+    report = build_report(_load(_V2_VERB))
+    assert report["n"] == 28
+    assert report["counts"]["wrong"] == 0
+    assert report["all_cases_correct"] is True
+    cbg = report["correct_by_gold"]
+    assert cbg.get("entailed", 0) >= 11
+    assert cbg.get("refuted", 0) >= 4
+    assert cbg.get("unknown", 0) >= 5
+    assert cbg.get("declined", 0) >= 8
+
+
 def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None:
    """A committed disagreement with gold is ``wrong``; a decline never is,
    even when gold expected a definite verdict (that's a miss, tracked via
--- a/tests/test_deduction_surface.py
+++ b/tests/test_deduction_surface.py
@ -371,3 +371,64 @@ def test_runtime_decides_full_propositional_gold_corpus_wrong_zero() -> None:
            continue
        wrong.append(f"{case['text']!r} -> gold={gold} surface={surface!r}")
    assert not wrong, "\n".join(wrong)
+
+
+def test_verb_predicate_is_decided_band_v5_vp() -> None:
+    """The ADR-0258 §6.3 verb-predicate scope-out, now decided (ADR-0260):
+    a verb universal discharged by a membership fact, authoritatively (the
+    ``en_verb_universal`` band holds an earned SERVE license)."""
+    surface = deduction_grounded_surface(
+        "All philosophers teach. Socrates is a philosopher. "
+        "Therefore Socrates teaches."
+    )
+    assert surface is not None
+    assert "Your premises entail: socrates teaches" in surface
+    assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE)
+
+
+def test_verb_universal_discharged_by_membership_chain() -> None:
+    """The mechanism this band adds: the membership atom minted by copula
+    sentences unifies with a verb universal's instantiated antecedent across
+    an is-a chain — neither v3-MEM (refuses verb sentences) nor v2-EN
+    (refuses quantifier leads and is-a clauses) alone decides this."""
+    surface = deduction_grounded_surface(
+        "Felix is a tortoise. All tortoises are reptiles. All reptiles crawl. "
+        "Therefore Felix crawls."
+    )
+    assert surface is not None
+    assert "Your premises entail: felix crawls" in surface
+
+
+def test_verb_unknown_is_scoped_to_the_verb_reading() -> None:
+    surface = deduction_grounded_surface(
+        "Viktor cooks. Viktor is a chef. Therefore Viktor cooks stew."
+    )
+    assert surface is not None
+    assert "verb phrase at face value" in surface
+    assert "don't settle" in surface
+
+
+def test_verb_unearned_band_would_be_hedged() -> None:
+    """The en_verb_* bands ride the SAME earned-license gate: strip the
+    license and the same sound answer is served DISCLOSED, never
+    authoritatively."""
+    surface = deduction_grounded_surface(
+        "All philosophers teach. Socrates is a philosopher. "
+        "Therefore Socrates teaches.",
+        license_lookup=lambda band: None,
+    )
+    assert surface is not None
+    assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE)
+    assert "Your premises entail: socrates teaches" in surface
+
+
+def test_verb_reader_refusal_keeps_prior_honest_surface() -> None:
+    """When the verb band ALSO cannot read the argument (here: a
+    ditransitive), the pre-existing honest surface is preserved verbatim —
+    the band only widens."""
+    surface = deduction_grounded_surface(
+        "Hannah gives Samuel bread. Hannah is a mother. "
+        "Therefore Hannah gives Samuel bread."
+    )
+    assert surface is not None
+    assert "Your premises entail" not in surface
--- a/tests/test_verb_argument_reader.py
+++ b/tests/test_verb_argument_reader.py
@ -0,0 +1,250 @@
+"""Band v5-VP (ADR-0260) — verb-predicate argument reader contract.
+
+The reader extends v3-MEM's per-individual propositional lowering with a
+second atom family — one atom per *(individual, verb-lemma-group,
+object-term)* — in one shared atom space, so a verb universal's
+instantiation can be discharged by a membership fact minted from a copula
+sentence. It is pure and deterministic. Soundness rides on the ROBDD engine;
+these tests pin that the reader hands it the RIGHT problem — in particular
+that third-person-singular agreement links a universal's base verb form to a
+singular fact's 3sg form via the closed verb relation (NOT the noun table).
+"""
+
+from __future__ import annotations
+
+import pytest
+
+from generate.proof_chain.member import MemberRefusal, read_member_argument
+from generate.proof_chain.shape import (
+    EN_VERB_CHAIN,
+    EN_VERB_FACT,
+    EN_VERB_NEGATIVE,
+    EN_VERB_UNIVERSAL,
+)
+from generate.proof_chain.verb import (
+    MAX_ATOMS,
+    MAX_PREMISE_SENTENCES,
+    VerbArgument,
+    VerbRefusal,
+    read_verb_argument,
+)
+
+
+def _read(text: str) -> VerbArgument:
+    arg = read_verb_argument(text)
+    assert isinstance(arg, VerbArgument), arg
+    return arg
+
+
+def _refusal(text: str) -> VerbRefusal:
+    ref = read_verb_argument(text)
+    assert isinstance(ref, VerbRefusal), ref
+    return ref
+
+
+# --- the gap this band fills is real -----------------------------------------
+
+
+def test_the_gap_this_band_fills_is_real() -> None:
+    """The exact ADR-0258 §6.3 verb-predicate scope-out: v3-MEM refuses verb
+    sentences (no copula ⇒ ``sentence_shape_out_of_band``); this band decides
+    them. Both facts hold at once — v3-MEM is unchanged, this is a new tier."""
+    text = "All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches."
+    assert isinstance(read_member_argument(text), MemberRefusal)
+    assert isinstance(read_verb_argument(text), VerbArgument)
+
+
+# --- the flagship reading -----------------------------------------------------
+
+
+def test_flagship_universal_verb_instantiation() -> None:
+    arg = _read(
+        "All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches."
+    )
+    assert arg.band == EN_VERB_UNIVERSAL
+    # Universal instantiates at the one named individual: mem -> verb; the
+    # membership fact anchors it; the query is the instantiated verb atom.
+    assert arg.premise_formulas == ("(a0) -> (a1)", "a0")
+    assert arg.query_formula == "a1"
+    assert arg.atoms == ("socrates : philosophers", "socrates : teach")
+
+
+def test_agreement_links_base_and_third_person_forms() -> None:
+    # +s rule: live/lives must land in ONE verb group (and must NOT be routed
+    # through the noun table, where "lives" is the plural of "life").
+    arg = _read("All men live. Socrates is a man. Therefore Socrates lives.")
+    assert arg.query_formula == "a1"  # same atom as the instantiated consequent
+    assert "socrates : live" in arg.atoms
+
+
+@pytest.mark.parametrize(
+    "universal_form, conclusion_form",
+    [
+        ("teach", "teaches"),   # +es after sibilant
+        ("study", "studies"),   # y -> ies
+        ("go", "goes"),         # irregular table
+        ("bark", "barks"),      # +s
+    ],
+)
+def test_agreement_rules_each_link(universal_form: str, conclusion_form: str) -> None:
+    arg = _read(
+        f"All wolves {universal_form}. Rex is a wolf. Therefore Rex {conclusion_form}."
+    )
+    assert arg.band == EN_VERB_UNIVERSAL
+    assert arg.premise_formulas == ("(a0) -> (a1)", "a0")
+    assert arg.query_formula == "a1"
+
+
+def test_transitive_object_is_part_of_the_atom_key() -> None:
+    arg = _read(
+        "All poets write verses. Homer is a poet. Therefore Homer writes verses."
+    )
+    assert arg.query_formula == "a1"
+    assert "homer : write verses" in arg.atoms
+    # A different object is a DIFFERENT atom — arity/object at face value.
+    arg2 = _read(
+        "All poets write verses. Homer is a poet. Therefore Homer writes epics."
+    )
+    assert arg2.query_formula == "a2"
+
+
+def test_negative_universal_instantiates_negated() -> None:
+    arg = _read("Miriam is a nun. No nuns marry. Therefore Miriam does not marry.")
+    assert arg.band == EN_VERB_NEGATIVE
+    assert arg.premise_formulas == ("a0", "(a0) -> (~(a1))")
+    assert arg.query_formula == "~(a1)"
+
+
+def test_membership_chain_discharges_verb_universal() -> None:
+    arg = _read(
+        "Felix is a tortoise. All tortoises are reptiles. All reptiles crawl. "
+        "Therefore Felix crawls."
+    )
+    assert arg.band == EN_VERB_CHAIN
+    assert arg.premise_formulas == ("a0", "(a0) -> (a1)", "(a1) -> (a2)")
+    assert arg.query_formula == "a2"
+
+
+def test_sentential_not_wraps_a_verb_fact() -> None:
+    arg = _read(
+        "Boris does not smoke. Therefore it is not the case that Boris smokes."
+    )
+    assert arg.band == EN_VERB_FACT
+    assert arg.premise_formulas == ("~(a0)",)
+    assert arg.query_formula == "~(a0)"
+
+
+def test_universal_does_not_leak_across_individuals() -> None:
+    arg = _read(
+        "All monks chant. Basil is a monk. Therefore Gregory chants."
+    )
+    # The universal instantiates at BOTH named individuals; the query is
+    # Gregory's verb atom, whose membership antecedent nothing anchors.
+    assert arg.premise_formulas == ("(a0) -> (a1)", "(a2) -> (a3)", "a0")
+    assert arg.query_formula == "a3"
+    assert arg.atoms[2] == "gregory : monks"
+
+
+def test_verb_and_class_words_never_cross_families() -> None:
+    # "teacher" (class) and "teaches" (verb) must stay distinct atoms even
+    # though the noun rules could relate the strings.
+    arg = _read("Socrates teaches. Therefore Socrates is a teacher.")
+    assert arg.premise_formulas == ("a0",)
+    assert arg.query_formula == "a1"
+
+
+# --- band classification ------------------------------------------------------
+
+
+@pytest.mark.parametrize(
+    "text, band",
+    [
+        ("All poets write. Homer is a poet. Therefore Homer writes.",
+         EN_VERB_UNIVERSAL),
+        ("Homer is a poet. All poets are artists. All artists dream. Therefore Homer dreams.",
+         EN_VERB_CHAIN),
+        ("Homer is a poet. No poets whistle. Therefore Homer does not whistle.",
+         EN_VERB_NEGATIVE),
+        ("Homer writes. Homer is a poet. Therefore Homer writes.",
+         EN_VERB_FACT),
+    ],
+)
+def test_band_classification(text: str, band: str) -> None:
+    assert _read(text).band == band
+
+
+# --- typed refusals -----------------------------------------------------------
+
+
+@pytest.mark.parametrize(
+    "text, reason",
+    [
+        ("Caesar did not surrender. Therefore Caesar surrenders.",
+         "tense_out_of_band"),
+        ("The old sailor whittles. Therefore Socrates naps.",
+         "sentence_shape_out_of_band"),
+        ("Nero fiddles in Rome. Therefore Nero fiddles.",
+         "sentence_shape_out_of_band"),
+        ("Hannah gives Samuel bread. Therefore Hannah gives Samuel bread.",
+         "sentence_shape_out_of_band"),
+        # "do not" after a multi-token subject: the negation is real but the
+        # grammar cannot normalize it (the exact ``<name> does not`` shape is
+        # the only one read), so the honest reason is the unread negation.
+        ("The twins do not quarrel. Therefore the twins quarrel.",
+         "internal_negation_unread"),
+        ("If Noah builds then Noah rests. Noah builds. Therefore Noah rests.",
+         "mixed_structure_out_of_band"),
+        ("Someone sneezes. Therefore Ora sneezes.",
+         "quantifier_out_of_band"),
+        ("All men do not teach. Socrates is a man. Therefore Socrates teaches.",
+         "internal_negation_unread"),
+        ("Jonah preaches. Therefore all prophets preach.",
+         "universal_conclusion_out_of_band"),
+        ("Socrates teaches. Do philosophers teach?",
+         "question_sentence"),
+        # Delegated copula parses keep v3-MEM's own typed refusals.
+        ("Dogs are loyal. Rex barks. Therefore Rex barks.",
+         "bare_plural_out_of_band"),
+        ("Socrates is the philosopher. Socrates teaches. Therefore Socrates teaches.",
+         "definite_description_out_of_band"),
+        ("Socrates is a man who teaches. Therefore Socrates teaches.",
+         "relative_clause_out_of_band"),
+        # A pure-copula argument is never decided by this band (defensive
+        # closure — such texts belong to v3-MEM/v4-CM).
+        ("Socrates is a man. Therefore Socrates is a man.",
+         "sentence_shape_out_of_band"),
+    ],
+)
+def test_typed_refusals(text: str, reason: str) -> None:
+    assert _refusal(text).reason == reason
+
+
+# --- honesty caps -------------------------------------------------------------
+
+
+def test_premise_cap_refuses_not_truncates() -> None:
+    body = " ".join(f"Zed{i} naps." for i in range(MAX_PREMISE_SENTENCES + 1))
+    ref = _refusal(body + " Therefore Zed0 naps.")
+    assert ref.reason == "too_many_premises"
+
+
+def test_atom_cap_refuses_not_truncates() -> None:
+    # Each premise mints one verb atom; 16 premises fit the premise cap, but
+    # a universal instantiated at every individual overflows MAX_ATOMS.
+    names = [f"Kip{i}" for i in range(12)]
+    body = " ".join(f"{n} naps." for n in names)
+    body += " " + " ".join(f"{n} is a squirrel." for n in names[:4])
+    text = body + " All squirrels forage. Therefore Kip0 forages."
+    ref = _refusal(text)
+    assert ref.reason in ("too_many_atoms", "too_many_premises")
+
+
+# --- determinism --------------------------------------------------------------
+
+
+def test_reading_is_deterministic() -> None:
+    text = (
+        "All poets write. Homer is a poet. Therefore Homer writes."
+    )
+    assert read_verb_argument(text) == read_verb_argument(text)
+    assert MAX_ATOMS == 24 and MAX_PREMISE_SENTENCES == 16