diff --git a/docs/adr/ADR-0262-curriculum-grounded-serving.md b/docs/adr/ADR-0262-curriculum-grounded-serving.md index 5659794d..a74482db 100644 --- a/docs/adr/ADR-0262-curriculum-grounded-serving.md +++ b/docs/adr/ADR-0262-curriculum-grounded-serving.md @@ -98,6 +98,16 @@ is §5.1. ### 5.1 The binding constraint on Phase 2 is ratified curriculum VOLUME +> **Amended 2026-07-25 by ADR-0264 §4.1.** The conclusion below — that the +> remaining work is "a curriculum-authoring and ratification task, not an +> engineering one" — is wrong, and the reason is in this ADR's own §6. Authoring +> the ≈219 relations prescribed here takes the family past +> `MAX_PREMISE_SENTENCES` at row 17, at which point the band answers *nothing*. +> The §6 scope-out is therefore not a future contingency; it is a prerequisite. +> The *criterion* stated below (a band whose entailed class is ~1% of its volume +> demonstrates nothing) is upheld and promoted to a measured precondition. The +> original text is preserved unchanged. + A band earns SERVE at θ_SERVE=0.99 only with n ≥ 657 committed cases and a genuine outcome mix. The question space of a subject is `|vocabulary|² − |vocabulary|`, so volume is reachable (physics: 240, @@ -125,6 +135,13 @@ curriculum to teach a negative ("no X causes Y") or an exclusion. Until a corpus does, `refuted` is a verdict this path can render but never reach. The serving code handles it; the lane documents it. +> **Sharpened 2026-07-25 by ADR-0264 Fact 1.** Stronger than "never reach": +> authoring a negative row *without* teaching the compiler polarity does not +> yield UNKNOWN — it yields a confident wrong `entailed`, because +> `CurriculumChain.sentence` is unconditionally affirmative. The independent +> oracle ignores `polarity` for the same reason, so gold agrees and `wrong=0` +> stays green. ADR-0264 R1–R4 and R8 close this before any negative is authored. + ### 5.3 The commit gate must be routability, not shape Shipped first as a shape gate (`Does …?`) with the deduction composer's @@ -177,6 +194,16 @@ chosen from those, or biology's chain corpus authored first. family (sound: fewer premises can lose an entailment, never create one), and to disclose the narrowing. + > **Superseded 2026-07-25 by ADR-0264 R5.** This is no longer a scope-out: §5.1's + > own remedy triggers it at row 17. Two corrections to the reasoning above. + > (i) "No current family exceeds 9" is measured against a corpus that §5.1 asks + > to grow 24×. (ii) *Sound* is the wrong property — a sound narrowing can still + > lose true entailments, which is coverage loss in exactly the class the license + > counts. The property needed is *verdict-identical*, which holds for any scope + > that is a superset of the query-atom rows, because each compiled premise mints + > one independent propositional atom. Verified over 8,520 questions with zero + > mismatches — `docs/research/curriculum-premise-scope-2026-07-25.md` probe 3. + ## 7. Verification - `tests/test_curriculum_serve.py` — 20 tests: premise provenance and the diff --git a/docs/adr/ADR-0264-negative-curriculum-and-premise-scope.md b/docs/adr/ADR-0264-negative-curriculum-and-premise-scope.md new file mode 100644 index 00000000..3c165e55 --- /dev/null +++ b/docs/adr/ADR-0264-negative-curriculum-and-premise-scope.md @@ -0,0 +1,350 @@ +# ADR-0264 — Negative curriculum, premise scope, and what a curriculum band can earn + +- **Status:** Proposed — awaiting Joshua Shay's ratification. This ADR changes no + flag and no default; it fixes a schema shape and a compilation rule, and it + records a blocking finding about ADR-0262 §5.1. +- **Date:** 2026-07-25 +- **Arc:** curriculum-license-loop Phase A + (`docs/plans/curriculum-license-loop-2026-07-25.md` §4) +- **Governs:** the `polarity` field of `teaching/domain_chains/*.jsonl`, + `teaching/curriculum_premises.py` (`CurriculumChain.sentence`, + `compile_premises`, `load_curriculum` admission), + `chat/curriculum_surface.py::decide_curriculum_question`, + `evals/curriculum_serve/oracle.py`, and + `teaching/ratification.py::validate_admissible`. +- **Amends:** ADR-0262 §5.1 (its conclusion, not its decision) and §6's + premise-set-scaling scope-out. Builds on ADR-0261 §5.1 (refuse, don't drop) + and ADR-0260 (the verb-predicate band that decides these arguments). + +## 1. Context + +The plan of record asked Phase A one question: how does an explicitly-taught +negative coexist with the open-world reading, where an absent edge must stay +UNKNOWN and never become "no"? Answering it required reading the compilation +path end to end, and that read produced three facts that were not known when the +plan was written. Two of them change what the arc must do next. + +Everything below was verified by running the real path in-tree, not by reading +docstrings. Reproduction is in §6. + +**Fact 1 — the row field `polarity` is silently ignored, and a negative row +serves a confident wrong "Yes."** `load_curriculum` reads +`review_status`, `domain`, `subject`, `object`, the two `*_pack_id` fields and +`connective`. Nothing else. `CurriculumChain.sentence` is unconditionally +`f"{subject} {connective} {obj}"`. So a row added today with +`"polarity": "negative"` compiles to the *affirmative* sentence, and the question +it was authored to refute comes back `entailed`: + +``` ++1 negative row (acceleration requires charge, polarity=negative) + Does acceleration require charge? -> verdict='entailed' +``` + +The user-visible surface for that verdict is *"Yes — my physics curriculum +teaches that acceleration requires charge, directly, among the 10 modal +relations it states."* The curriculum said the opposite. + +This is not caught by any gate. `evals/curriculum_serve/oracle.py` is +independent in code but reads the same rows, and it ignores `polarity` for the +same reason. Gold and the serving path agree on the wrong answer, so the lane +stays green and `wrong=0` holds. This is the exact failure class Phase A exists +to prevent, and it is now demonstrated rather than hypothesised. + +**Fact 2 — `operator_family` is not the band axis; the connective is.** The plan +of record and the division-of-work both state that bands key on +`(domain, operator_family)` and warn against a `modal_negative` family. The +warning points at a real hazard but names the wrong field. `load_curriculum` +never reads the row's `operator_family`; `CONNECTIVE_FAMILY[connective]` is the +sole family authority, deliberately and as documented in +`teaching/curriculum_premises.py`. Two rows in the corpus already declare a +family their connective contradicts (`physics-causal-008` and one +`systems_software` row, both `requires`/`causal`) and are correctly read as +modal. `physics · modal` therefore holds **9** chains, not 8 — which is where +the plan's `n=9` came from. + +The hazard restated correctly: the connective fixes both the band **and the +propositional atom**. A negative expressed as a *new connective* (`precludes`, +`does_not_require`) mints a different atom from the positive question it was +meant to refute, so the ROBDD returns UNKNOWN instead of REFUTED — silently, at +every such row. + +**Fact 3 — the premise cap makes ADR-0262 §5.1's own prescribed remedy destroy +the capability it was meant to build.** `compile_premises` emits *every* chain in +the family as a premise sentence, and `read_verb_argument` refuses beyond +`MAX_PREMISE_SENTENCES = 16`. Measured end to end: + +``` +physics modal chains = 9 (cap = 16) + +7 rows -> 16 premises: taught positive = 'entailed' negative pair = 'entailed' + +8 rows -> 17 premises: taught positive = 'declined' negative pair = 'declined' + reason='compiled_premises_unreadable' +``` + +At row 17 the band stops answering *anything* — including +`conservation requires symmetry`, which works today. ADR-0262 §5.1 prescribes +authoring **≈219 relations per subject × family** to reach a balanced band. +ADR-0262 §6 scopes premise-set scaling out, on the reasoning that "no current +family exceeds 9" and the fix can wait until one does. Those two sections are in +contradiction: §5.1's remedy triggers §6's deferred fix at row 17 and then +collapses the band for the remaining 202 rows. The scope-out silently blocks the +plan it shares an ADR with. + +## 2. Decision + +**R1 — Polarity is a row-level `polarity` field.** Values `"affirmative"` and +`"negative"`; **absent means affirmative**, so all 88 existing rows are +unchanged and no migration is required. + +It is *not* an `intent` value. `intent` already carries an orthogonal +teaching-intent axis with five values in use +(`cause`/`verification`/`procedure`/`comparison`/`correction`); overloading it +would conflate two independent axes in one column and make each unreadable from +the other. It is *not* a new `operator_family` value and *not* a new +`connective` — see R3. + +**R2 — A negative row compiles to the sentential-not form.** + +``` +affirmative: f"{subject} {connective} {obj}" +negative: f"it is not the case that {subject} {connective} {obj}" +``` + +The `("it","is","not","the","case","that")` prefix is an existing shape in +`generate/proof_chain/english.py` and `member.py`, already read by the verb +band. It is chosen over `"{subject} does not {connective} {obj}"` for one +reason: the `does not` shape wants the base form of the verb (`require`, not +`requires`), which would require a de-inflection table — a new inverse of +`_VERB_IRREGULAR_3SG` — to be invented and maintained. The band happens to read +`"does not requires"` too, but that is ungrammatical English written into a +reasoning trace, and depending on it would be depending on an accident. + +Verified: all three shapes reach `REFUTED` with correct atom identity +(premises `('a0','a1','~(a2)')` against query `'a2'`). + +**R3 — A negative row MUST reuse the affirmative connective.** Atom identity is +`(subject, normalized-verb, object)`. `REFUTED` is `(⋀P) → ¬Q` being a tautology, +which requires the negated premise and the query to be *the same atom*. A new +connective mints a new atom and yields UNKNOWN. `validate_admissible` must reject +a negative row whose connective is absent from `CONNECTIVE_FAMILY`. + +**R4 — Contradiction is rejected at ratification, not discovered at serve +time.** A negative row for a `(domain, subject, connective, object)` that already +holds an affirmative row — or the reverse — is inadmissible. +`teaching/ratification.py::validate_admissible` rejects it. Without this guard +the compiled premise set is inconsistent, `evaluate_entailment_with_trace` +returns `REFUSED`/`INCONSISTENT_PREMISES`, and the surface says *"The curriculum +I have for that is inconsistent"* — an honest answer to a problem that should +never have been ratified. Fail at authoring, where a human is present. + +**R5 — Premise compilation is query-scoped, and the scope must be a superset of +the query-atom rows.** The soundness condition is exact: + +> For a corpus of atomic rows, every compiled premise mints one independent +> propositional atom. A scope that contains every row whose atom is the query's +> atom decides the query identically to the full family, because no other atom +> appears in the query formula and independent atoms cannot constrain it. + +Two consequences worth stating separately, because ADR-0262 §6 conflates them: + +- **Sound** (narrowing cannot invent an entailment) is the weaker property §6 + argues for. It is true but insufficient — a narrowing can be sound while + silently *losing* true entailments, which is coverage loss in exactly the + class of case the license counts, and is the shape ADR-0261 §5.1 was written + about. +- **Verdict-identical** is the property R5 requires, and it holds only for a + scope that is a superset of the query-atom rows. + +The default scope is **term incidence**: rows whose subject or object is one of +the query's two terms. This is bounded by vocabulary degree rather than corpus +size, keeps real neighbouring premises in the argument, and is a superset of the +query-atom rows. If term incidence would still exceed the band's cap, narrow to +the query-atom rows — which is verdict-identical, never an arbitrary truncation. +The reader is never asked to refuse for size. + +**R6 — An empty scope is UNKNOWN; only an empty family is a refusal.** Today +`compile_premises` returning nothing means "this family has no ratified chains" +and correctly refuses `empty_curriculum`. Under R5 it will much more often mean +"no ratified chain mentions this query", which is UNKNOWN — the open-world +reading. These two must be distinguished at the call site, or 8,463 of the 8,520 +questions measured in §6 flip from `unknown` to `declined`. + +**R7 — `premise_count` continues to report family size.** It is user-visible +(*"It states 9 modal relations, and none of them decides this one"*). Under R5 +the compiled scope is usually 0 or 1, and reporting that number would understate +the curriculum to the user. Report family size in the surface; carry the +compiled-scope size as a separate field for the lane and the audit ledger, and +disclose the narrowing there. This also keeps ADR-0262 §7's existing assertions +stable. + +**R8 — The oracle learns polarity independently.** `evals/curriculum_serve/oracle.py` +reads `polarity` with its own default rule and its own restated vocabulary, sharing +no helper with `teaching/curriculum_premises.py`. Its code-level independence is +the entire evidentiary value of the lane; a shared polarity helper would make the +two agree by construction, which is what Fact 1 shows is indistinguishable from +being right. Additionally: **negative edges are excluded from the BFS adjacency**. +A negative edge is not a traversable path, and including it would inflate the +reachability depths the lane asserts against. + +**R9 — Earning requires an outcome-mix floor, and a band that cannot reach the +threshold must say so before anyone authors for it.** ADR-0262 §5.1 already +states the acceptability criterion — "a band whose entailed class is 1% of its +volume is passed by a pipeline that never entails anything" — but leaves it as +prose. It becomes a measured precondition: the practice producer reports, per +band, the maximum honest committed volume and the maximum entailed share +achievable from the ratified corpus, and a band whose ceiling is below the +licensing threshold is reported **structurally unable to earn SERVE** rather than +left for authoring effort to discover. Phase B specifies the bound; this ADR +fixes the requirement that the bound exist. + +## 3. Why this is sound + +R5 is the only rule that changes an existing answer, so it is the only one that +needs evidence rather than argument. Both candidate scopes were compared against +full-family compilation over every routable question in all four served domains +(philosophy_theology sampled to its first 40 lemmas to stay tractable): + +``` +questions compared : 8520 +term-incidence mismatches : 0 +query-atom mismatches : 0 (over non-empty scopes) +query-atom EMPTY scopes : 8463 <- R6 governs these +max premises, full-family : 9 +max premises, term-incidence : 8 +``` + +Zero verdict changes. The physics lane's `entailed 14 / unknown 12 / declined 6` +gold is preserved exactly: taught edges keep a non-empty query-atom scope and +stay `entailed`; untaught pairs get an empty scope and stay `unknown` under R6; +pre-band refusals are untouched. + +R1–R4 and R8 add a verdict (`REFUTED`) that the decision path already maps and +already has a surface template for. They do not change any existing answer, +because absent `polarity` means affirmative. + +## 4. Findings + +### 4.1 No curriculum band can earn a SERVE license under the current architecture + +This follows from two facts already in the repository, and it does not depend on +any rule in §2. + +- A taught edge makes exactly one question come back `entailed`, so the entailed + cases available to a band equal the number of ratified chains in its family. +- The premise cap holds a family to **≤16 chains** — beyond that the band + answers nothing at all (Fact 3). + +So a band has at most 16 entailed cases available, against a licensing threshold +of **n ≥ 657 committed**. Reaching 657 therefore requires a ledger that is at +least `1 − 16/657` = **97.6% non-entailed**. ADR-0262 §5.1 already rules that +unacceptable. Its ⅓-entailed target caps committed volume at `3 × 16 = 48`, and +*any* mix floor above 2.44% blocks a license outright. + +The conclusion inverts §5.1's: the binding constraint is **not** curriculum +volume, and not "a curriculum-authoring and ratification task — Shay's call, not +an engineering one." Authoring is blocked by an engineering prerequisite. R5 is +that prerequisite: query-scoped compilation removes the 16-chain ceiling, at +which point §5.1's ≈219-relation prescription becomes achievable and its +arithmetic becomes correct again. + +### 4.2 Eight of eleven bands cannot reach the threshold even with unlimited authoring + +Volume is bounded by *taught vocabulary*, not by corpus size, because a question +must have both terms in exactly one served subject's vocabulary to route at all +(`ambiguous_reading` otherwise). Measured routable question spaces: + +| domain | \|V\| | exclusive lemmas | routable ordered pairs | +|---|---|---|---| +| physics | 16 | 16 | 240 | +| mathematics_logic | 16 | 15 | 210 | +| systems_software | 16 | 15 | 210 | +| philosophy_theology | 151 | 149 | 22,052 | + +`max_honest_n = routable_pairs × |connectives(family)|`, one committed case per +distinct question: + +| band | chains | max honest n | vs 657 | +|---|---|---|---| +| curriculum_physics_causal | 7 | 720 | reachable | +| **curriculum_physics_modal** | **9** | **480** | **impossible** | +| curriculum_mathematics_logic_modal | 4 | 420 | impossible | +| curriculum_mathematics_logic_contrast | 8 | 210 | impossible | +| curriculum_mathematics_logic_evidential | 8 | 210 | impossible | +| curriculum_mathematics_logic_sequence | 4 | 210 | impossible | +| curriculum_systems_software_causal | 7 | 630 | impossible | +| curriculum_systems_software_modal | 6 | 420 | impossible | +| curriculum_systems_software_sequence | 3 | 210 | impossible | +| curriculum_philosophy_theology_contrast | 8 | 22,052 | reachable | +| curriculum_philosophy_theology_modal | 8 | 44,104 | reachable | + +**The plan of record's first content target is one of the impossible ones.** +`physics · modal` was chosen for having the most chains (9, "closest of eleven +bands"). Chain count is not the constraint; vocabulary is. Its ceiling is 480 — +below the threshold with every possible question counted, and that ceiling cannot +be raised by authoring chains, only by growing `en_physics_v1`. + +`physics · causal` is nominally reachable at 720 but would need 657 of its 720 +questions — 91% of the entire space — leaving no held-out room at all. + +**The defensible first target is `philosophy_theology · modal`:** 44,104 honest +ceiling (67× the threshold), 8 chains already ratified, and the same 8-chain +starting point as the physics band. This reverses a decision in the plan of +record, on a measurement. + +### 4.3 The two unbuilt segments are still unbuilt, and are still not the blocker + +Phases C and D stand as written — `evals/curriculum_serve/practice/` and the +`reseal` verb do not exist, and `chat/data/curriculum_serve_ledger.json` has no +writer. That finding survives. What changes is its priority: building the +producer before R5 lands would produce a correct instrument reporting that every +band is at its ceiling. + +## 5. What this ADR does not decide + +- **The bound in R9.** The specific de-duplication tuple and mix floor are + Phase B's deliverable. R9 fixes only that a bound must exist and be reported. +- **Raising `MAX_PREMISE_SENTENCES`.** Rejected as an approach, not deferred: it + is a shared honesty cap that the 25 deduction bands also decide under, raising + it would move hash-pinned lanes, and a 219-premise argument is not honest at + any cap. R5 makes the cap irrelevant to curriculum instead. +- **Composition across curriculum edges.** Still scoped out per ADR-0262 §3.3. + R8's exclusion of negative edges from BFS is a reachability-reporting rule, not + a licence to chain. +- **Negated questions.** The grammar stays `Does ?`, + three tokens. Polarity lives in the curriculum, never in the question. "Does X + not require Y?" is four tokens and refuses typed, as it does today. +- **Growing `en_physics_v1`.** §4.2 says physics bands need vocabulary, not + chains. Whether to grow the pack is a separate ratified decision. +- **Any flag.** `curriculum_serving_enabled` stays False. + +## 6. Verification + +All four probes are in +`docs/research/curriculum-premise-scope-2026-07-25.md`, each runnable against a +clean tree; the corpus-mutating one restores the file and asserts byte-identity. + +1. **Negation reaches REFUTED** — three shapes, atom identity checked. +2. **Cap collapse** — real negative rows appended to + `physics_chains_v1.jsonl`; band answers at 16 premises, declines at 17, + including the previously-working taught positive. Also demonstrates Fact 1: + at +1 row the negative pair answers `entailed`. +3. **Scope equivalence** — 8,520 routable questions, 0 mismatches for both + candidate scopes, 8,463 empty query-atom scopes. +4. **Band ceilings** — the §4.2 table, derived from `CONNECTIVE_FAMILY` and the + loaded vocabularies rather than restated. + +No production code changed in this ADR; §2's rules are implemented by Phase C +against Phase B's tests. + +## 7. Consequences for the plan of record + +1. **New phase, before content: implement R5–R7.** Nothing else in the arc can + earn anything until the 16-chain ceiling is gone. Loud failure mode (the lane + pins every physics verdict), so it is a Sonnet unit once the assertion set + here is fixed — which it now is. +2. **Phase F retargets to `philosophy_theology · modal`** per §4.2, and its + volume target is recomputed against that band's ceiling. +3. **Phase B additionally specifies R9's ceiling report**, so no future arc + spends authoring effort on a structurally impossible band. +4. **ADR-0262 §5.1's conclusion is amended** by §4.1 — the constraint is + engineering-then-content, not content alone. §5.1's *criterion* is upheld and + promoted to a measured precondition. diff --git a/docs/adr/INDEX-by-domain.md b/docs/adr/INDEX-by-domain.md index 1d2ccdbb..847b8210 100644 --- a/docs/adr/INDEX-by-domain.md +++ b/docs/adr/INDEX-by-domain.md @@ -43,7 +43,8 @@ check). Surfaces: `generate/proof_chain/render.py`, `chat/deduction_surface.py`. | ADR | Decision | Governs | |---|---|---| -| [0262](./ADR-0262-curriculum-grounded-serving.md) | Exams answered from the ratified curriculum, read OPEN-world; §5 records that curriculum **volume** is the binding constraint (~25× gap) | `chat/curriculum_surface.py`, `chat/curriculum_serve_license.py`, `evals/curriculum_serve/runner.py` | +| [0262](./ADR-0262-curriculum-grounded-serving.md) | Exams answered from the ratified curriculum, read OPEN-world; §5 records that curriculum **volume** is the binding constraint (~25× gap) — **conclusion amended by 0264 §4.1** | `chat/curriculum_surface.py`, `chat/curriculum_serve_license.py`, `evals/curriculum_serve/runner.py` | +| [0264](./ADR-0264-negative-curriculum-and-premise-scope.md) | Negatives via a row-level `polarity` field reusing the affirmative connective; premise compilation is query-scoped (superset of the query-atom rows ⇒ verdict-identical). §4.1: the 16-premise cap holds a band to ≤16 entailed cases, so **no curriculum band can earn SERVE** until scoping lands — the blocker is engineering, not content | `teaching/curriculum_premises.py`, `teaching/ratification.py`, `evals/curriculum_serve/oracle.py`, `teaching/domain_chains/*.jsonl` | ## Reliability licensing and the ledger bridge diff --git a/docs/research/curriculum-premise-scope-2026-07-25.md b/docs/research/curriculum-premise-scope-2026-07-25.md new file mode 100644 index 00000000..d941a823 --- /dev/null +++ b/docs/research/curriculum-premise-scope-2026-07-25.md @@ -0,0 +1,311 @@ +# Curriculum premise scope, negative rows, and band ceilings — measurements + +**Date:** 2026-07-25 · **Arc:** curriculum-license-loop Phase A · +**Decision record:** `docs/adr/ADR-0264-negative-curriculum-and-premise-scope.md` +**Base:** main @ `6ada6f7a` + +Four probes, run against a clean tree on canonical Python 3.12.13. Each is +self-contained and reproducible; probe 2 mutates a corpus file and restores it, +asserting byte-identity at the end. Written down because the numbers reverse two +decisions in the plan of record, and a claim that reverses a plan needs to be +re-runnable by whoever doubts it. + +Run from a worktree root with `uv run python `. + +--- + +## Probe 1 — negation reaches REFUTED, with correct atom identity + +**Question.** The verb band reads three negation shapes. Does a negated premise +mint *the same atom* as the affirmative question it should refute? If the verb +agreement normalizes `does not require` to a different atom than `requires`, the +ROBDD returns UNKNOWN and every authored negative is silently inert. + +```python +from generate.proof_chain.verb import read_verb_argument, VerbArgument +from generate.proof_chain.entail import evaluate_entailment_with_trace + +POS = ["conservation requires symmetry", "mass requires force"] +QUERY = "conservation requires asymmetry" + +CANDIDATES = { + "A does-not (base verb)": "conservation does not require asymmetry", + "B does-not (3sg verb)": "conservation does not requires asymmetry", + "C sentential-not": "it is not the case that conservation requires asymmetry", +} + +for label, neg in CANDIDATES.items(): + argument = ". ".join(POS + [neg]) + f". Therefore {QUERY}." + arg = read_verb_argument(argument) + if not isinstance(arg, VerbArgument): + print(f"{label:26s} UNREADABLE -> {arg}") + continue + tr = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula) + print(f"{label:26s} outcome={tr.outcome.value:9s} reason={tr.reason!r}") + print(f"{'':26s} premises={arg.premise_formulas} query={arg.query_formula!r}") +``` + +**Result.** All three reach `refuted` / `tautological_refutation`, with +`premises=('a0', 'a1', '~(a2)')` against `query='a2'` — same atom, negated. +Agreement normalization is not an obstacle; shape B works despite being +ungrammatical. + +**Bearing.** ADR-0264 R2 picks shape C, on the grounds that shape A needs a +de-inflection table that does not exist and shape B depends on an accident. + +--- + +## Probe 2 — the premise cap collapses the band at 17 chains, and `polarity` is ignored + +**Question.** Two at once. (a) What happens to a band when the family exceeds +`MAX_PREMISE_SENTENCES = 16`? (b) What does a row carrying +`"polarity": "negative"` actually serve today? + +Appends synthetic-but-admissible negative rows to the real physics corpus — +`en_physics_v1` lemmas, `review_status: reviewed`, `connective: requires`, so +they survive `load_curriculum` admission — then asks the real decision path. + +```python +import json, sys +from pathlib import Path + +CORPUS = Path("teaching/domain_chains/physics_chains_v1.jsonl") +ORIG = CORPUS.read_text(encoding="utf-8") + +sys.path.insert(0, ".") +from evals.curriculum_serve.oracle import vocabulary +vocab = sorted(vocabulary("physics")) +print(f"physics vocabulary = {len(vocab)} lemmas: {vocab}") + +def row(n, subj, obj, polarity): + return json.dumps({ + "chain_id": f"physics-modal-neg-{n:03d}", "domain": "physics", + "operator_family": "modal", "subject": subj, "intent": "verification", + "connective": "requires", "object": obj, + "subject_pack_id": "en_physics_v1", "object_pack_id": "en_physics_v1", + "review_status": "reviewed", "polarity": polarity, + "provenance": "probe:phase-a:2026-07-25", + }) + +taught = {(r["subject"], r["object"]) for r in map(json.loads, ORIG.strip().splitlines())} +cands = [(s, o) for s in vocab for o in vocab if s != o and (s, o) not in taught] + +for n_neg in (1, 7, 8, 20): + rows = [row(i, s, o, "negative") for i, (s, o) in enumerate(cands[:n_neg], 1)] + CORPUS.write_text(ORIG.rstrip("\n") + "\n" + "\n".join(rows) + "\n", encoding="utf-8") + for mod in [m for m in list(sys.modules) if m.startswith(("teaching.", "chat.", "evals."))]: + del sys.modules[mod] + from teaching.curriculum_premises import load_curriculum, compile_premises + from chat.curriculum_surface import decide_curriculum_question + load_curriculum.cache_clear() + prem, _ = compile_premises(load_curriculum("physics"), "modal") + s, o = cands[0] + d_neg = decide_curriculum_question(f"Does {s} require {o}?") + d_pos = decide_curriculum_question("Does conservation require symmetry?") + print(f"\n+{n_neg:2d} negative rows -> modal premises={len(prem)}") + print(f" negative pair ({s} requires {o}): verdict={d_neg.verdict!r} reason={d_neg.reason!r}") + print(f" taught positive: verdict={d_pos.verdict!r} reason={d_pos.reason!r}") + +CORPUS.write_text(ORIG, encoding="utf-8") +print("\ncorpus restored:", CORPUS.read_text(encoding="utf-8") == ORIG) +``` + +**Result.** + +``` +physics vocabulary = 16 lemmas ++ 1 negative rows -> modal premises=10 negative pair='entailed' taught positive='entailed' ++ 7 negative rows -> modal premises=16 negative pair='entailed' taught positive='entailed' ++ 8 negative rows -> modal premises=17 negative pair='declined' taught positive='declined' + reason='compiled_premises_unreadable' ++20 negative rows -> modal premises=29 both 'declined' +corpus restored: True +``` + +**Bearing, (b) first because it is worse.** At +1 row the question the negative +was authored to refute answers **`entailed`** — surfaced to a user as *"Yes — my +physics curriculum teaches that acceleration requires charge, directly."* The +`polarity` field is read by nothing. `evals/curriculum_serve/oracle.py` ignores +it too, so lane gold agrees with the wrong answer and `wrong=0` stays green. This +is ADR-0264 Fact 1 and it is the reason Phase A had to precede Phase F. + +**Bearing, (a).** At 17 chains the band stops answering everything, including the +taught positive that works today. ADR-0262 §5.1 prescribes ≈219 chains per +band; ADR-0262 §6 scopes the cap out as a future contingency. The remedy trips +the deferred fix at row 17. ADR-0264 §4.1. + +Also confirms `physics · modal` holds **9** chains, not 8: `physics-causal-008` +declares `operator_family: causal` but its connective is `requires`, and +`CONNECTIVE_FAMILY` is the sole family authority. That is where the plan's `n=9` +came from. + +--- + +## Probe 3 — narrowed premise scope is verdict-identical + +**Question.** ADR-0262 §6 proposes compiling "the query's k-hop neighborhood" +and argues it is sound because "fewer premises can lose an entailment, never +create one." Sound is not the property needed — a narrowing can be sound while +silently losing true entailments, which is coverage loss in exactly the class the +license counts. Is there a scope that is verdict-*identical*? + +Compares two candidate scopes against full-family compilation over every +routable question in all four served domains (philosophy_theology sampled to its +first 40 lemmas to stay tractable). + +```python +from teaching.curriculum_premises import CONNECTIVE_FAMILY, load_curriculum +from chat.curriculum_surface import SERVED_DOMAINS +from generate.proof_chain.verb import read_verb_argument, VerbArgument +from generate.proof_chain.exist import read_exist_argument, ExistArgument +from generate.proof_chain.entail import evaluate_entailment_with_trace, Entailment + +VERDICT = {Entailment.ENTAILED: "entailed", Entailment.REFUTED: "refuted", + Entailment.UNKNOWN: "unknown", Entailment.REFUSED: "declined"} + +def decide(premise_sentences, conclusion): + if not premise_sentences: + return "EMPTY_SCOPE" + argument = ". ".join(premise_sentences) + f". Therefore {conclusion}." + arg = read_verb_argument(argument) + if not isinstance(arg, VerbArgument): + arg = read_exist_argument(argument) + if not isinstance(arg, ExistArgument): + return "unreadable" + return VERDICT[evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome] + +fam_conn = {} +for c, f in CONNECTIVE_FAMILY.items(): + fam_conn.setdefault(f, []).append(c) + +total = mismatch_ti = mismatch_qa = empty_qa = 0 +for domain in SERVED_DOMAINS: + cur = load_curriculum(domain) + vocab = sorted(cur.vocabulary) + if len(vocab) > 40: + vocab = vocab[:40] + for family, conns in fam_conn.items(): + chains = cur.family(family) + if not chains: + continue + for connective in conns: + for s in vocab: + for o in vocab: + if s == o: + continue + concl = f"{s} {connective} {o}" + full = [c.sentence for c in chains] + ti = [c.sentence for c in chains if c.subject in (s, o) or c.obj in (s, o)] + qa = [c.sentence for c in chains + if c.subject == s and c.connective == connective and c.obj == o] + v_full, v_ti, v_qa = decide(full, concl), decide(ti, concl), decide(qa, concl) + total += 1 + if v_ti != v_full and v_ti != "EMPTY_SCOPE": + mismatch_ti += 1 + if v_qa == "EMPTY_SCOPE": + empty_qa += 1 + elif v_qa != v_full: + mismatch_qa += 1 + +print(f"questions compared : {total}") +print(f"term-incidence mismatches : {mismatch_ti}") +print(f"query-atom mismatches : {mismatch_qa}") +print(f"query-atom EMPTY scopes : {empty_qa}") +``` + +**Result.** + +``` +questions compared : 8520 +term-incidence mismatches : 0 +query-atom mismatches : 0 (over non-empty scopes) +query-atom EMPTY scopes : 8463 +max premises, full-family : 9 +max premises, term-incidence: 8 +``` + +**Bearing.** Verdict-identity holds for any scope that is a superset of the +query-atom rows, because every compiled premise mints one *independent* +propositional atom and no other atom appears in the query formula. That exact +condition is ADR-0264 R5 — stronger than §6's soundness argument and the reason +narrowing here is not the ADR-0261 §5.1 premise-dropping failure. + +8,463 of 8,520 (99.3%) have an empty query-atom scope. Those must return UNKNOWN, +not the current `empty_curriculum` refusal — ADR-0264 R6. The same 99.3% is the +quantified UNKNOWN-padding exposure that Phase B's mix floor has to bound. + +--- + +## Probe 4 — band ceilings against the licensing threshold + +**Question.** A question routes only if exactly one served subject's vocabulary +contains both terms. So honest volume is bounded by *vocabulary*, not corpus +size. Which bands can reach n ≥ 657? + +```python +from collections import Counter, defaultdict +from teaching.curriculum_premises import CONNECTIVE_FAMILY, load_curriculum, compile_premises +from chat.curriculum_surface import SERVED_DOMAINS + +fam_conn = defaultdict(list) +for c, f in CONNECTIVE_FAMILY.items(): + fam_conn[f].append(c) + +vocab = {d: load_curriculum(d).vocabulary for d in SERVED_DOMAINS} +owner = Counter(t for d in SERVED_DOMAINS for t in vocab[d]) + +routable = {} +for d in SERVED_DOMAINS: + excl = {t for t in vocab[d] if owner[t] == 1} + routable[d] = sum(1 for s in excl for o in excl if s != o) + print(f"{d:22s} |V|={len(vocab[d]):4d} exclusive={len(excl):4d} routable={routable[d]:6d}") + +for d in SERVED_DOMAINS: + cur = load_curriculum(d) + for f in sorted(fam_conn): + n_chains = len(compile_premises(cur, f)[0]) + if not n_chains: + continue + cap = routable[d] * len(fam_conn[f]) + print(f"curriculum_{d}_{f:12s} chains={n_chains:3d} max_honest_n={cap:6d} " + f"{'reachable' if cap >= 657 else 'IMPOSSIBLE'}") +``` + +**Result.** 8 of 11 bands are structurally unable to reach 657 — including +`curriculum_physics_modal` (480), the plan of record's chosen first content +target. Full table in ADR-0264 §4.2. + +``` +physics |V|= 16 exclusive= 16 routable= 240 +mathematics_logic |V|= 16 exclusive= 15 routable= 210 +systems_software |V|= 16 exclusive= 15 routable= 210 +philosophy_theology |V|= 151 exclusive= 149 routable= 22052 +``` + +**Bearing.** `physics · modal` was chosen for having the most ratified chains. +Chain count is not the constraint. Its 480 ceiling counts *every possible +question* and still falls short, and no amount of authoring raises it — only +growing `en_physics_v1` would. `philosophy_theology · modal` has the same 8-chain +start and a 44,104 ceiling. ADR-0264 §4.2 retargets Phase F accordingly. + +Cross-check against ADR-0262 §5.1, which computed the question space as +`|V|² − |V|` and got physics 240 (identical) and philosophy_theology 22,650 +(vs 22,052 here). The difference is that this probe excludes lemmas taught by +more than one served subject, which `resolve_domain` refuses as +`ambiguous_reading`. 22,052 is the tighter and correct figure; §5.1's arithmetic +was right and its bound slightly loose. + +--- + +## What these four probes jointly establish + +A taught edge yields exactly one `entailed` question, so entailed cases available += chains in the family. The cap holds that to ≤16. Against n ≥ 657 committed, a +license therefore needs a ledger ≥ 97.6% non-entailed — which ADR-0262 §5.1 +already rules unacceptable, and its ⅓-entailed target caps committed volume at +48. + +**So no curriculum band can earn a SERVE license as the architecture stands**, +and the blocker is engineering (premise scope), not content. That inverts the +conclusion two arcs closed on. Probe 3 is the unblock: it shows the narrowing +that removes the ceiling costs nothing in verdict fidelity.