Merge pull request 'Query-scoped premise compilation (ADR-0264 R5-R7)' (#120) from feat/query-scoped-premises into main

chat/curriculum_surface.py

@@ -169,16 +169,26 @@ def resolve_family(query: CurriculumQuery) -> str | CurriculumRefusal:
     return CurriculumRefusal("out_of_curriculum", query.verb)
 
 
-def _query_sentence(query: CurriculumQuery, family: str) -> str:
+def _resolve_connective(query: CurriculumQuery, family: str) -> str:
-    """The conclusion sentence, spelled with the CURRICULUM's own connective
+    """The curriculum's own spelling of *query*'s relation, within *family* —
-    form so the reader's agreement linking has nothing to do — the question's
+    the SAME closed agreement relation the verb-predicate band uses
-    base form is normalized here, once, visibly."""
+    (ADR-0260), so a question may spell the relation in its base form while
+    the curriculum states it in the third person. Guarded by
+    :func:`resolve_family`: any *family* reaching this function already has a
+    connective that links to ``query.verb``."""
     for connective in CONNECTIVE_FAMILY:
         if CONNECTIVE_FAMILY[connective] == family and verb_forms_link(
             query.verb, connective
         ):
-            return f"{query.subject} {connective} {query.obj}"
+            return connective
-    return f"{query.subject} {query.verb} {query.obj}"  # pragma: no cover - guarded above
+    return query.verb  # pragma: no cover - guarded above
+
+
+def _query_sentence(query: CurriculumQuery, family: str) -> str:
+    """The conclusion sentence, spelled with the CURRICULUM's own connective
+    form so the reader's agreement linking has nothing to do — the question's
+    base form is normalized here, once, visibly."""
+    return f"{query.subject} {_resolve_connective(query, family)} {query.obj}"
 
 
 def band_for(domain: str, family: str) -> str:
@@ -196,7 +206,8 @@ class CurriculumDecision:
     reason: str           # typed refusal reason, or "" when decided
     domain: str = ""
     family: str = ""
-    premise_count: int = 0
+    premise_count: int = 0  # FAMILY size — user-visible (ADR-0264 R7)
+    scope_size: int = 0     # compiled, query-scoped premise count (R5/R7)
 
 
 def decide_curriculum_question(text: str) -> CurriculumDecision:
@@ -217,11 +228,24 @@ def decide_curriculum_question(text: str) -> CurriculumDecision:
         return CurriculumDecision("declined", "", family.reason, domain=domain)
 
     curriculum = load_curriculum(domain)
-    premises, _chain_ids = compile_premises(curriculum, family)
+    family_chains = curriculum.family(family)
-    if not premises:
+    if not family_chains:
         return CurriculumDecision(
             "declined", "", "empty_curriculum", domain=domain, family=family
         )
+    family_size = len(family_chains)
+    band = band_for(domain, family)
+    connective = _resolve_connective(query, family)
+    premises, _chain_ids = compile_premises(
+        curriculum, family, query=(query.subject, connective, query.obj)
+    )
+    if not premises:
+        # An empty SCOPE — no ratified chain mentions either query term — is
+        # the open-world UNKNOWN reading (ADR-0264 R6). Distinct from an
+        # empty FAMILY (handled above), which stays `empty_curriculum`.
+        return CurriculumDecision(
+            "unknown", band, "", domain=domain, family=family, premise_count=family_size,
+        )
     conclusion = _query_sentence(query, family)
     argument = ". ".join(premises) + f". Therefore {conclusion}."
 
@@ -235,7 +259,7 @@ def decide_curriculum_question(text: str) -> CurriculumDecision:
         if not isinstance(arg, ExistArgument):
             return CurriculumDecision(
                 "declined", "", "compiled_premises_unreadable",
-                domain=domain, family=family, premise_count=len(premises),
+                domain=domain, family=family, premise_count=family_size,
             )
     trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula)
     verdict = {
@@ -247,11 +271,12 @@ def decide_curriculum_question(text: str) -> CurriculumDecision:
     reason = trace.reason if trace.outcome is Entailment.REFUSED else ""
     return CurriculumDecision(
         verdict,
-        band_for(domain, family),
+        band,
         reason,
         domain=domain,
         family=family,
-        premise_count=len(premises),
+        premise_count=family_size,
+        scope_size=len(premises),
     )
 
 

teaching/curriculum_premises.py

@@ -41,6 +41,7 @@ from core.capability.domains import (
     DOMAIN_CORPORA,
     DOMAIN_PACKS,
 )
+from generate.proof_chain.verb import MAX_PREMISE_SENTENCES
 
 _REPO_ROOT = Path(__file__).resolve().parents[1]
 
@@ -205,15 +206,49 @@ def load_curriculum(domain: str) -> Curriculum:
 
 
 def compile_premises(
-    curriculum: Curriculum, family: str
+    curriculum: Curriculum,
+    family: str,
+    query: tuple[str, str, str] | None = None,
 ) -> tuple[tuple[str, ...], tuple[str, ...]]:
     """``(premise_sentences, chain_ids)`` for *family*, in corpus order.
 
-    Deterministic: the same curriculum and family always compile to the same
+    Without *query*, the full family is compiled unscoped — the pre-ADR-0264
-    sentences in the same order, so a lane report over them is SHA-pinnable.
+    behaviour, still correct where no query exists to scope by.
+
+    With *query* — ``(subject, connective, obj)``, the query's own terms in
+    the curriculum's connective spelling — compilation is QUERY-SCOPED
+    (ADR-0264 R5). The default scope is **term incidence**: every chain whose
+    subject or object is one of the query's two terms. This is a superset of
+    the query's own atom, and since every compiled premise mints one
+    independent propositional atom that no other atom in the argument can
+    constrain, a term-incidence scope decides the query identically to the
+    full family — verified over 8,520 routable questions with zero verdict
+    mismatches (``docs/research/curriculum-premise-scope-2026-07-25.md``
+    probe 3). If term incidence would still exceed the reader's
+    :data:`MAX_PREMISE_SENTENCES` cap, narrow further to the **query-atom
+    rows** — chains whose ``(subject, connective, obj)`` exactly match the
+    query's — which stays verdict-identical for the same reason. Scope is
+    never truncated arbitrarily and never refused for size.
+
+    Deterministic: the same curriculum, family and query always compile to
+    the same sentences in the same order, so a lane report over them is
+    SHA-pinnable.
     """
     chains = curriculum.family(family)
-    return tuple(c.sentence for c in chains), tuple(c.chain_id for c in chains)
+    if query is None:
+        scoped = chains
+    else:
+        q_subject, q_connective, q_obj = query
+        scoped = tuple(
+            c for c in chains if c.subject in (q_subject, q_obj) or c.obj in (q_subject, q_obj)
+        )
+        if len(scoped) > MAX_PREMISE_SENTENCES:
+            scoped = tuple(
+                c
+                for c in chains
+                if c.subject == q_subject and c.connective == q_connective and c.obj == q_obj
+            )
+    return tuple(c.sentence for c in scoped), tuple(c.chain_id for c in scoped)
 
 
 class UnratifiedChain(LookupError):
@@ -242,6 +277,7 @@ def resolve_pinned(curriculum: Curriculum, chain_ids: tuple[str, ...]) -> tuple[
 __all__ = [
     "CONNECTIVE_FAMILY",
     "FAMILIES",
+    "MAX_PREMISE_SENTENCES",
     "Curriculum",
     "CurriculumChain",
     "UnratifiedChain",

tests/test_curriculum_serve.py

@@ -26,6 +26,9 @@ from chat.curriculum_surface import (
 )
 from evals.curriculum_serve.oracle import oracle_answer
 from teaching.curriculum_premises import (
+    MAX_PREMISE_SENTENCES,
+    Curriculum,
+    CurriculumChain,
     UnratifiedChain,
     compile_premises,
     load_curriculum,
@@ -37,6 +40,9 @@ from teaching.curriculum_premises import (
 
 
 def test_premises_come_only_from_ratified_chains() -> None:
+    """Without a *query*, ``compile_premises`` compiles the FULL family,
+    unscoped — the pre-ADR-0264 shape, still correct where there is no query
+    to scope by (e.g. a lane audit that wants the whole corpus)."""
     curriculum = load_curriculum("physics")
     premises, chain_ids = compile_premises(curriculum, "causal")
     assert premises == (
@@ -60,14 +66,105 @@ def test_pinned_chain_that_is_not_ratified_fails_loudly() -> None:
 
 
 def test_family_scoping_never_loses_a_taught_edge() -> None:
-    """Compilation is family-scoped; every taught edge is reachable from the
+    """Every taught edge is reachable from a QUERY-SCOPED compile of its own
-    family its own connective implies, so scoping cannot hide an answer."""
+    terms (ADR-0264 R5) — a term-incidence scope built from a chain's own
+    (subject, connective, obj) always contains that chain, so query-scoping
+    cannot hide an answer the full family would have given."""
     curriculum = load_curriculum("physics")
     for chain in curriculum.chains:
-        premises, _ = compile_premises(curriculum, chain.family)
+        premises, _ = compile_premises(
+            curriculum, chain.family, query=(chain.subject, chain.connective, chain.obj)
+        )
         assert chain.sentence in premises
 
 
+# --- query-scoped compilation (ADR-0264 R5-R7) ---------------------------------
+
+
+def test_term_incidence_scope_is_narrower_than_the_full_family() -> None:
+    """The default scope only pulls in chains that share one of the query's
+    two terms — not the whole family — for a query with real neighbours."""
+    curriculum = load_curriculum("physics")
+    full, _ = compile_premises(curriculum, "modal")
+    scoped, _ = compile_premises(
+        curriculum, "modal", query=("mass", "requires", "energy")
+    )
+    assert 0 < len(scoped) < len(full)
+    assert "mass requires force" in scoped  # touches "mass"
+    assert "energy requires conservation" in scoped  # touches "energy"
+
+
+def test_cap_narrowing_falls_back_to_query_atom_rows() -> None:
+    """R5: when term incidence would exceed the reader's
+    ``MAX_PREMISE_SENTENCES`` cap, compilation narrows further to the
+    query-atom rows — never an arbitrary truncation, and the cap is never
+    exceeded either way. A synthetic hub-shaped family (every chain shares
+    one term) is used so the term-incidence scope provably exceeds the cap
+    without depending on any corpus's current size."""
+    chains = tuple(
+        CurriculumChain(f"synthetic-{i}", f"leaf{i}", "requires", "hub", "modal")
+        for i in range(MAX_PREMISE_SENTENCES + 4)
+    )
+    curriculum = Curriculum(domain="synthetic", chains=chains, vocabulary=frozenset())
+    # Every chain touches "hub" -> unscoped term incidence around ("leaf0",
+    # "hub") is the entire (over-cap) family.
+    scoped, ids = compile_premises(curriculum, "modal", query=("leaf0", "requires", "hub"))
+    assert len(scoped) <= MAX_PREMISE_SENTENCES
+    assert scoped == ("leaf0 requires hub",)
+    assert ids == ("synthetic-0",)
+
+
+def test_cap_narrowing_to_an_absent_atom_is_an_empty_scope() -> None:
+    """A query whose exact atom is not among the ratified chains narrows to
+    nothing when the cap forces query-atom scoping — an empty scope, which
+    the surface layer reads as UNKNOWN (R6), never a truncation artifact."""
+    chains = tuple(
+        CurriculumChain(f"synthetic-{i}", f"leaf{i}", "requires", "hub", "modal")
+        for i in range(MAX_PREMISE_SENTENCES + 4)
+    )
+    curriculum = Curriculum(domain="synthetic", chains=chains, vocabulary=frozenset())
+    scoped, ids = compile_premises(
+        curriculum, "modal", query=("nonexistent", "requires", "hub")
+    )
+    assert scoped == () and ids == ()
+
+
+def test_empty_scope_is_unknown_not_declined() -> None:
+    """R6: an empty SCOPE (no ratified chain mentions either query term) is
+    the open-world UNKNOWN reading — distinct from an empty FAMILY. Physics
+    teaches "force" and "acceleration" as members of the causal chain but
+    neither term appears in any MODAL chain, so the modal term-incidence
+    scope around them is empty while the modal family itself (9 chains) is
+    not."""
+    curriculum = load_curriculum("physics")
+    assert curriculum.family("modal")  # the family is not empty
+    decision = decide_curriculum_question("Does acceleration require motion?")
+    assert decision.verdict == "unknown"
+    assert decision.scope_size == 0
+    assert decision.band == band_for("physics", "modal")
+    assert decision.premise_count == len(curriculum.family("modal"))
+
+
+def test_empty_family_is_still_the_empty_curriculum_refusal() -> None:
+    """R6's other half: an empty FAMILY (no ratified chain at all, of any
+    scope) stays the pre-existing `empty_curriculum` refusal — physics has no
+    ratified "sequence" chains, and both terms are taught."""
+    curriculum = load_curriculum("physics")
+    assert not curriculum.family("sequence")
+    decision = decide_curriculum_question("Does force precede acceleration?")
+    assert decision.verdict == "declined"
+    assert decision.reason == "empty_curriculum"
+
+
+def test_premise_count_reports_family_size_scope_size_reports_the_compile() -> None:
+    """R7: `premise_count` stays the user-visible FAMILY size (unchanged
+    surface prose); the query-scoped compile size is carried separately."""
+    curriculum = load_curriculum("physics")
+    decision = decide_curriculum_question("Does force cause acceleration?")
+    assert decision.premise_count == len(curriculum.family("causal"))
+    assert 0 < decision.scope_size <= decision.premise_count
+
+
 # --- the verdicts that matter -------------------------------------------------