作成日：2026-10-19。状態：設計用草案・独立確認前。P2 の研究設計 19 の §7（パイロット候補 A）を、拡張契約に沿って設計する文書です。実装は 24（結果）に記録します。導出は手作業で、形式証明支援系による検証はありません。実証済みと言えるのは、24 に記す有限の範囲の検査だけです。
実在する疾患や分類の分割、医学的な妥当性は扱いません。述語名・主体・文脈はすべて架空です（fiction:）。
1. 問い
旧い概念 P が、新しい定義で P1 と P2 に分割される。旧い記録
P(a)には、どちらかを区別する情報がない。基底の Horn 断片は選言を持たない。このとき、契約は、新しい意味能力（候補集合と情報要求）の設計と検査を導けるか。
R4 の K06 の期待は、①旧回答を再現する、②現在の候補は P1・P2 で各確定はしない、③必要な区別情報を返す、④旧参照を消して任意の一方へ書き換えたら失敗、の四つです。P2-b はこれを満たす最小の拡張を作り、契約の側が不足しないかを点検します。確かめることは次の三つです。
| 確かめること | 受入条件（19 の §8） |
|---|---|
| 拡張を理解しない消費側は、拡張の能力を要求する文脈で停止し、保留・訂正済みの修飾も落とさない | X04 |
拡張の回答型（候補集合）が、基底の状態（supported 等）へ暗黙に変換される経路がない |
X05 |
| 旧の P の問いは変わらず、新の P1／P2 の問いは候補集合と情報要求を返し、偽にも確定にもしない | X14 |
2. 意味
2.1 分割の宣言
要求は split = {parent, parts} を持つ。parent は旧い述語 P、parts は新しい述語 Q1…Qk（2 ≤ k ≤ 8、互いに異なり、parent を含まない）。すべて要求の package で宣言された単項の述語で、package の閉包の定義・包含のどれにも現れない（規則のない原子的な述語）こと。満たさない要求は invalid_input で拒否する。
2.2 公理と、個体ごとの枠
公理は仕様（split_spec.json）に固定され、要求は変更できない。各個体 x について：
| 公理 | 内容 |
|---|---|
| A1 包含 | Qj(x) → P(x)（各 j） |
| A2 被覆 | P(x) → Q1(x) ∨ … ∨ Qk(x) |
| A3 排他 | ¬(Qi(x) ∧ Qj(x))（i < j） |
補題 S1（枠）：一つの個体について、(P, Q1,…,Qk) の真偽の割り当てで A1〜A3 を満たすものは、ちょうど k+1 個：すべて偽の w0、および Qj と P だけが真の wj（j = 1…k）。導出：A3 より Q は高々一つ真。A1 より真の Q があれば P は真。A2 より P が真なら Q のどれかが真。よって「P と Q がすべて偽」か「P と一つの Qj だけ真」しかない。∎
公理は個体ごとの全称単項文の連言なので、個体ごとに独立に調べれば足りる（補題 S2）。
2.3 入力：採用された文字列だけ
基底の採用選択（select_view）が文脈 c・参照時点 v で採用した主張のうち、個体 s についての、語彙 {P, Q1…Qk} の原子の肯定・否定を D = (Pos, Neg) とする。疑い・確認のない AI 候補・訂正済みの主張は D に入らない（基底の採用方針そのまま）。同じ原子の肯定と否定がともに採用されていれば、基底の衝突であり、拡張は解決しない（§2.5）。
2.4 候補集合
Mod(D) = { w ∈ {w0, w1,…,wk} | w が D の肯定をすべて満たし、否定をすべて満たさない }。
| 条件 | split.status |
candidates |
意味 |
|---|---|---|---|
| Mod = ∅ | inconsistent |
なし | 採用された記述が公理に反する（例：P かつどの Qj も否定、二つの Q の肯定） |
| Mod = {w0} | parent_opposed |
なし | P が否定された（A1 から、どの部分も成り立たない）、またはすべての部分が否定された（A2 から、P が成り立たない）。基底の P は後者では未決のまま |
| w0 ∈ Mod かつ他にもある | no_parent |
なし | P が成り立つかどうか未決。候補を作らない |
| w0 ∉ Mod、候補が k 個 | open |
全部 | P は成り立つが、どの部分かを区別する情報がない |
| w0 ∉ Mod、2 個以上 k 個未満 | narrowed |
残り | 一部の部分が否定されて除かれた |
| w0 ∉ Mod、1 個、その Q の肯定は採用されていない | single |
その 1 個 | 他の候補がすべて除かれたので、公理から一つに定まる。採用された主張ではない |
| w0 ∉ Mod、1 個、その Q の肯定が採用されている | asserted |
その 1 個 | 部分が直接採用されている（P が採用されていなくても、A1 から P が成り立つ） |
candidates は w ∈ Mod の j の集合（credulous）。除かれた部分には理由（adopted_negative・other_part_asserted・parent_opposed）と主張の ID を付ける。single を supported にしない（§3 の S5）。
2.5 基底との関係と停止
| 場合 | 行の status |
理由 |
|---|---|---|
| 文脈に未知の能力を要求する可視の主張がある（保留・訂正済みも含む） | blocked |
unknown_capability（missing_capabilities、blocking_assertion_refs つき） |
| 同じ原子の肯定と否定がともに採用されている | blocked |
unresolved_conflict |
| 資源の上限 | blocked |
step_limit |
| 上記以外 | computed |
－ |
各行は base も持つ：parent と各 part の原子 1 個について、基底が答える状態（supported／opposed／undetermined）を、採用された主張から同じ規則で並べる（規則のない述語なので、基底の閉包は採用された原子そのもの）。これは基底の query の結果と一致しなければならない（検査する）。split.status の語彙は基底の状態の語彙と互いに素にする。
2.6 情報要求
open・narrowed・single の行は、information_requests に confirm_part を返す：候補の部分の一覧と、「候補のどれか一つの人の確認済みの肯定、または他の候補すべての人の確認済みの否定があれば定まる」という充足条件、および保留中の主張（AI 候補・疑い）の ID。inconsistent は resolve_split_violation。いずれも臨床上の否定を意味しない（「検査が存在しない」等を含意しない）。
2.7 能力
拡張の能力名は p2-concept-split-draft-1。主張がこれを required_capabilities に持つとき、基底だけの消費側は、その文脈を解釈せず unassessed（I4）。拡張は、理解する能力を {P0 の基底, 分割} だけにして select_view を呼ぶ。要求の自己申告（read_only など）は受け付けない。
2.8 範囲
| 含む | 含まない（範囲外） |
|---|---|
| 一つの文脈の中の、一つの個体の、採用された原子 | 文脈をまたぐ推論、時間による持続（「過去に P なら現在も P」）、別の個体との結合 |
| 規則のない原子的な単項述語の分割 | 定義・包含を持つ述語の分割、多項述語、部分の再分割（入れ子） |
| 候補の集合と、確認を求める情報要求 | 候補の確率、ある部分への自動的な確定、旧参照の書き換え |
| 旧データ（部分の主張を含まない）の旧い問い | 実在の分類の対応表 |
2.9 要求と結果の形
要求 schema_version p2-split-request-draft-1 operation query_split
consumer {profile, profile_spec_sha256, operations} budget {max_steps}
source {package, dependency_packages?, contexts, ledger} views
split {parent, parts} queries [{id, context_ref, subject, required}]
結果 schema_version p2-split-result-draft-1 profile p2-concept-split-draft-1
status, reason_codes, results[...], views, snapshot_sha256, split{parent, parts, axioms}, incomplete, steps_used
行 view, query, subject, context_ref, status(computed|blocked), reason_codes, answer_kind candidate_set, converted_to_base false,
base{parent, parts{部分: 状態}},
split{status, candidates[], excluded[{part, reasons[]}], parent_derived, derivation[公理の名前]},
evidence{ledger_ref, snapshot_sha256, adopted[{predicate, polarity, assertion_refs, review_refs}],
pending[{assertion_ref, predicate, polarity, origin_kind}]},
information_requests[]
blocked の行は split・base を持たない（null）。理由に応じて missing_capabilities・blocking_assertion_refs・conflicts を持つ
2.10 課金（steps）
要求の開始に 1。参照時点ごとに、主張 1 件・確認 1 件につき 1。問い合わせごとに、開始に 1、分割の語彙の原子（k+1 個）の各参照に 1、行の確定の前に 1。上限に達したら、完了した行を残し、未完了の行は blocked（step_limit）で値を持たない。
3. 導出（手作業）
S1 枠（§2.2）。S2 個体ごとの独立：A1〜A3 は個体ごとの単項全称文。D も個体ごとに分かれるので、Mod(D) は個体ごとの積。
S3 候補集合の健全性・完全性：candidates は Mod(D) の部分 j の集合に等しい。導出：定義より。実装は Mod を列挙せず、規則（除外：¬Qj ∈ Neg、Qm ∈ Pos (m ≠ j)、¬P ∈ Neg。親の成立：P ∈ Pos または Qj ∈ Pos）で計算するので、規則と列挙の一致を有限の範囲で全数検査する（k = 2〜5 で、各原子の {なし, 肯定, 否定} の全組。両方は基底の衝突として別に止める）。
S4 旧データでの無矛盾（保存性）：D が部分の原子を含まない（旧データ）なら、Mod(D) ≠ ∅。導出：D は P の肯定、P の否定、またはなし。それぞれ Mod = {w1…wk}、{w0}、全体で、空でない。さらに、旧い任意のモデル M（P を解釈する）に対し、Q1 := P^M、他の Qj := ∅ とすれば A1〜A3 を満たす拡張 M′ が作れる（P^M が空でも成り立つ）。よって旧語彙の任意の文について、旧理論 T と T ∪ {A1〜A3} は同じ旧語彙の帰結を持つ（保存的拡張）。この拡張は基底の答えを変えない：拡張は基底の状態を書き換えず、基底の query は分割を知らない。
S5 回答型の変換はできない（L5 の適用）：single（P(s) と ¬Q1(s) が採用、k = 2）は Q2(s) を A2 から導く。しかし基底の supported は I1（採用された主張からの Horn 閉包）で、Q2(s) は閉包に入らない。single を supported にする規則は I1 の意味を変えるので、拡張の一部としては認められず、別の拡張（橋渡し、R5）が、新しい採用方針と人の確認を要求して行う。したがって split.status から基底の状態への写像を定義しない。
S6 能力（L2 の適用）：主張が分割の能力を要求するとき、理解しない消費側にとって、その文脈の可視の主張は解釈できない。基底の規則により文脈全体が unassessed。拡張を理解する消費側では、同じ主張が分割の意味で解釈される。能力を要求しない文脈の結果は、拡張の有無で変わらない。
S7 情報要求の充足可能性：open・narrowed・single の各候補 j について、wj ∈ Mod(D)。したがって D に Qj(s) の肯定が採用されれば Mod = {wj}（asserted）となる。要求は、実現しない主張を求めない。除かれた部分は候補に含めない。
導出が示さないこと：任意の述語への一般化、複数個体・複数文脈の結合、時間による持続、実在の分割の正しさ、並行する更新。
4. 契約の適用：R2 では足りない
分割は読み取り専用で、独自の回答型を持つので、まず R2 の義務を点検する。
| R2 の義務 | 分割での扱い |
|---|---|
| R2-1 書き込み操作がない | 満たす（query_split は純粋） |
| R2-2 基底の語彙の述語へ導出しない | 読み替えが要る：分割は基底の語彙の述語（P、Qj）について推論する。結論は原子ではなく候補集合の状態として返し、基底の閉包に入れない、と読み替える |
| R2-3 基底の状態は核の採用選択を通してだけ読む | 満たす（select_view） |
| R2-4 回答型は基底と別で、変換規則を持たない | 満たす（S5） |
| R2-5 自己申告を根拠にしない | 満たす（能力は固定集合） |
R2 が問わないことが五つある。いずれも、分割が公理を加え、その下で結論を出すことから生じる。
| 不足 | 新しい義務 |
|---|---|
| 追加する公理が何で、要求が変えられないか | R6-1 公理の閉じた宣言 |
| 公理を加えても、旧データを矛盾させないか（保存性） | R6-2 旧データでの無矛盾 |
| 公理の下での結論が、公理の意味（モデル）に対して健全で完全か | R6-3 結論の健全性・完全性 |
| 公理の下で導いた結論を、採用された主張として示さないか | R6-4 結論は公理に相対 |
| 範囲外（文脈をまたぐ、時間の持続、規則のある述語）を明示し、黙って広げないか | R6-5 範囲の明示 |
| 情報要求が実現可能で、臨床の否定を含意しないか | R6-6 情報要求 |
これらは 19 の §3.3 のどのクラス（R1〜R5・COMP）にも収まらない：R1 は公理を加えるが回答型を持たず、R2 は回答型を持つが公理を加えない。新しいクラス R6「公理つき読み取りモジュール」を定義する。必須の義務は、共通の K-ID・K-STOP・K-INV・K-RES、R2-1〜R2-5（R2-2 は上の読み替え）、R6-1〜R6-6。クラスの定義は extensions.py の CLASSES・REQUIRED に加える。
これは契約の不足の発見であり、19 の §10 の「収まらない場合は新しいクラスを定義する手順を、P2-b の結果から検討する」の実演でもある。R6 が将来の公理つきの能力すべてに十分であることは主張しない。
5. 宣言（案）
| 項目 | 内容 |
|---|---|
id・class |
p2-concept-split・R6 |
depends_on |
p0-positive。reads_extensions は空 |
owns |
操作 query_split、schema p2-split-request-draft-1・p2-split-result-draft-1、profile p2-concept-split-draft-1、回答型 candidate_set、能力 p2-concept-split-draft-1。述語は所有しない（要求の package の述語を読むだけ） |
spec・pins |
src/med_dsl/split_spec.json（生バイトの hash を実装に固定）。embedded_in：実装と例（consumer が仕様 hash を持つ） |
implementation |
src/med_dsl/split.py（最上位の登録は host.py に 1 行：共有の入口の pin なので、追加は全拡張の再検証を要する） |
| 証拠の強さ | K-・R2-・R6-1・R6-4・R6-5：checked_native_template／R6-3・R6-6：finite_check（全数列挙）／R6-2：hand_derivation（一般のモデルへの拡張）。拡張全体は最も弱い finite_check |
6. 検査の計画
| 条件 | 検査 |
|---|---|
| X04 | 分割の能力を要求する主張を含む文脈：基底の query は unassessed（missing_capabilities・blocking_assertion_refs、保留・訂正済みを含む）／拡張は分割の意味で解釈する。第三の未知の能力は拡張でも blocked |
| X05 | 乱数 1,000 件以上で、行の base が基底の query の結果と一致する。split.status の語彙が基底の状態と互いに素。converted_to_base は常に偽。single でも base の部分は undetermined のまま |
| X14 | K06 の例：旧い問い（基底）は分割の有無で同じ結果。新の問いは候補集合と情報要求。旧参照を消さない（入力の保持）。AI 候補・訂正・参照時点ごとの違い・文脈の分離 |
| R6-3 | 規則と全数列挙（k = 2〜5 で各原子 3 通りの全組）の一致、乱数と密な生成の差分 |
| R6-2 | 旧データのみの全状態で inconsistent にならない。小さな旧モデルでの拡張の全数検査 |
| 全体 | 防護例（拒否・境界・変換しない）を最初から義務ごとに付ける（欠落を作らない）。予算の全値掃引。変異検査（作成者が選んだゲートの変異）。非干渉（登録して全 131 例が不変）。入力の保持と決定性 |
7. 範囲外と未解決
- 実在の概念の分割、医学的な妥当性。
- 文脈をまたぐ推論と時間の持続（「過去に P だったので現在も P」）。これは別の意味能力（有効期間つきの主張、候補 B）。
- 規則のある述語（定義・包含を持つ）の分割、多項述語、入れ子の分割、複数の分割の併用（記号を共有する併用は 19 の L4 により併用全体で再判定が要る）。
singleや候補の自動的な確定（橋渡し）。必要なら R5 の別拡張として、新しい採用方針と人の確認を要求する。- 契約のクラス R6 の義務表が、他の公理つきの能力に十分であること。