作成日：2026-10-19。状態：設計用草案・独立確認前。P2 の研究設計 19 の P2-c（併用の検査：独立な二拡張、記号を共有する二拡張、鎖。受入条件 X08〜X10）を、P2-b の概念の分割 を題材にして設計する文書です。実装は 26（結果）に記録します。導出は手作業で、形式証明支援系による検証はありません。述語・主体・文脈はすべて架空です。
1. 問い
個別には共存できる拡張（または同じ拡張の複数の使用）を併用したとき、併用も共存すると言えるのは、どのときか。個別の認定から導けないとき、何を全体で再判定するか。
19 の補題 の対応：
| 補題 | 内容 | 受入条件 |
|---|---|---|
| L3 | 所有が互いに素で、互いを読まない読み取り専用モジュールの併用は、個別の結果に分解できる | X08 |
| L4 | 個別に保存的でも、記号を共有する併用は保存的とは限らない（K04）。併用全体で再判定する | X09 |
| L6 | 鎖の範囲は交差に狭まり、途中で失われた区別は後段で回復しない | X10 |
L3 は拡張（宣言）の水準、L4・L6 は拡張の使用（インスタンス）の水準の性質である。分割の拡張は、一つの要求で複数の分割を宣言できるようにすると、その分割どうしが記号を共有し得る。K04 型の失敗（個別には保存的な二つの分割が、併用すると旧語彙に新しい含意を作る）を、分割で実際に作り、判定できるかを調べる。
2. 拡張の独立（L3、X08）
拡張 X、Y（基底は除く）が独立であるとは、次のすべてが機械的に検査できること。
- どちらも他方に（推移的に）依存しない（
depends_on）。 - 所有する名前が互いに素（登録時に検査済み）。
- 他方を読む宣言（
reads_extensions）がない。 - どちらの実装も、他方の固有のモジュール（基底が宣言したモジュール＝核を除いたもの）を import の閉包に含まない。
- どちらも順序に依存しない（
order_dependentが偽）。
independent_pairs(registry) がこれを列挙する。X08 は、独立な拡張の任意の部分集合を同時に載せ、登録と振り分けの順序を入れ替えても、基底と各拡張の観測（要求ごとの結果）が、単独で載せたときと一致することを、全例で検査する。独立でない組は、片方を不活性にすると他方の結果が変わることも確かめ、独立の条件が実際の依存を捉えていること（宣言が実体に合うこと）を確認する。
3. 複数の分割の併用の意味（L4・L6、X09・X10）
3.1 宣言と語彙
要求は分割の一覧 splits = [{parent, parts}, …]（1〜4 個）を持つ。各分割は P2-b と同じ条件（単項・宣言済み・規則のない述語、部分は 2 個以上で互いに異なり、親を含まない）を満たす。同じ分割を二度宣言できない。語彙 V は全分割の記号の和（|V| ≤ 10）。旧記号は、どの分割の部分でもない記号、新記号は、いずれかの分割の部分である記号。
3.2 公理と、成分ごとの枠
各分割に P2-b の公理 A1（包含）・A2（被覆）・A3（排他）が付く。記号を共有する分割の連結成分（共有する記号でつながる分割の同値類）ごとに、成分の語彙 V_c の真偽の割り当てで、成分の全分割の公理を満たすものの集合 Z_c を考える（|V_c| ≤ 10 なので全数列挙できる）。公理は個体ごとの単項全称文なので、個体ごと・成分ごとに独立（補題 J1）。
3.3 保存性の判定（全数で正確）
成分 c が旧語彙に対して保存的とは、旧い任意のモデル（旧記号の任意の解釈）が、新記号を解釈し直すだけで公理を満たす拡張を持つこと。旧記号 O_c の割り当て u（O_c → {0,1}）が拡張できるとは、Z_c の要素の O_c への制限に u が現れること。
成分 c は保存的 ⟺ すべての u ∈ {0,1}^{O_c} が拡張できる（補題 J2）。
併用の判定は、成分ごとの判定の積。保存的でなければ、拡張できない最初の u（記号名の整列順で最初）を反例として返す。
3.4 併用の結果
要求の各問い（参照時点・文脈・個体）について、採用された原子（P2-b と同じく、採用選択を通る）を D とし、成分ごとに Mod_c(D) = { v ∈ Z_c | v が D に合う } を求める。分割 s（成分 c）の併用での状態は、Mod_c(D) を s の記号へ射影した集合 M_s（s 単独の枠 W_s の部分集合）から、P2-b の表（inconsistent／parent_opposed／no_parent／open／narrowed／single／asserted）で決める。単独での状態は、D の s の記号だけに制限し、s の公理だけで決めた P2-b の結果。差があれば differs。
行は、splits（分割ごとの individual／joint／differs と、頼る公理の分割 axioms_of_splits）、leaf_candidates（葉の記号：どの分割の親でもない部分のうち、併用で成り立ち得るもの）、成分が公理に反する（inconsistent）が、どの分割も単独では反しない場合の interaction_violation を持つ。基底の状態は P2-b と同じく base に分けて返す。
3.5 構造の分類
| 構造 | 条件 |
|---|---|
single |
分割が一つ |
disjoint |
分割の語彙が互いに素 |
forest |
互いに素でなく、どの記号も高々一つの分割の部分で、「部分→親」の辺が閉路を持たない |
shared_parts |
ある記号が二つ以上の分割の部分（閉路はない） |
cyclic |
「部分→親」の辺が閉路を持つ |
chain は、ある分割の親が別の分割の部分である（入れ子）併用。構造は宣言した分割から再計算し、要求や構成員の主張から取らない。
3.6 操作・資源
操作は二つ：check_split_combination（併用の保存性の判定。台帳なし）と query_split_combination（併用の候補集合と情報要求）。課金：判定は、開始に 1、調べる旧記号の割り当て（成分ごとに辞書順に、最初の反例で止める。併用全体と、各分割を単独で判定する分）に 1、確定の前に 1。問い合わせは、P2-b の課金に加えて、問い合わせごとに成分の Z_c の要素の検査に 1。Z_c の構成そのものは要求の検証の一部で、|V| ≤ 10 の範囲で有限なので課金しない。
4. 導出（手作業）
J1（成分への分解） 公理も D も個体ごと・成分ごとに分かれるので、Z = ∏ Z_c、Mod = ∏ Mod_c。したがって、分割 s の併用での状態は、s の連結成分の分割の公理と、成分の語彙の D だけで決まる。導出の帰結（独立な併用の分解）：s の成分が {s} だけなら、s の併用での状態は単独での状態に等しい。
J2（保存性の判定の正確さ） 旧記号 O_c の上に旧理論の公理がない（規則のない述語だけを使う）とする。(⇒) ある u が拡張できないなら、一個体だけの旧モデル（O_c を u と解釈する）が拡張を持たない。この旧モデルは旧理論の（唯一の）モデルの一つなので、公理を加えた理論は、u を排除する旧語彙の文を含意する。それは旧理論からは導けないので、保存的でない。(⇐) 任意の旧モデル M について、各要素の O_c の割り当ては拡張できるので、要素ごとに拡張を選べる。公理は個体ごとの単項文なので、これで M の拡張が公理を満たす。したがって旧語彙の帰結は変わらない。∎ 限界：この判定は、旧記号の上に公理がなく、公理が単項で個体ごとである範囲に限る。
J3（K04 型） 分割 S1 = P→{Q1, Q2}、S2 = P′→{Q1, Q2}（部分を共有）。単独ではどちらも保存的（Q1 := P、Q2 := ∅ など）。併用では、Q1, Q2 ⊆ P ∩ P′ と P ⊆ Q1 ∪ Q2、P′ ⊆ Q1 ∪ Q2 から P = P′ が強制される。旧モデル P = {x}、P′ = ∅ は拡張できない（反例 u = (P=1, P′=0)）。旧語彙の新しい含意 P ⊆ P′ が個別の認定から導けない形で現れる。個別の認定は、併用の根拠にならない。
J4（森は保存的） 構造が disjoint または forest なら、トップダウンに、各分割で第一の部分 := 親、他の部分 := ∅ と解釈すれば、公理を満たす拡張が作れる（各記号は高々一つの分割の部分なので、一度だけ定義される。閉路がないので、親が先に定まる）。したがって J2 の判定は保存的になる。判定が J4 の十分条件の外でも保存的になり得る（例：S1 = P→{Q1, Q2}、S2 = P′→{Q1, Q3} は部分 Q1 を共有するが、Q1 := P ∩ P′、Q2 := P ∖ P′、Q3 := P′ ∖ P で拡張できる）。十分条件は判定の近道・照合に使い、判定は全数で行う。
J5（データの水準との一致） 旧記号だけを含む、採用された状態 D（O_c の各記号が肯定か否定で定まっている）に対し、Mod_c(D) ≠ ∅ ⟺ その割り当て u が拡張できる。したがって、成分が保存的 ⟺ 旧データだけの状態が inconsistent にならない。判定（静的）と問い合わせの結果（データ）が一致する。単独の分割（P2-b の R6-2）は、この特別な場合。
J6（鎖） 入れ子 S1 = P→{Q1, Q2}、S2 = Q1→{R1, R2}（鎖）。情報は双方向に流れる（R1 の肯定は Q1、P を導く。P の肯定と Q2 の否定は Q1 を導く）。後段 S2 の併用での状態が open／asserted になるのは、Q1 が（採用された肯定、または前段の除外により）全モデルで真のときに限る。前段が Q1 と Q2 を区別していない個体（P だけが採用）では、S2 は no_parent のまま、葉の候補は {Q2, R1, R2}。前段で区別されていない個体を、後段の分割だけで葉まで確定することはできない。鎖の結果が前段・後段の単独の結果の順次の合成と異なり得る例：P と ¬Q2 が採用されると、S1 は Q1 を定め（single）、その結果 S2 は open {R1, R2} になるが、S2 を単独で見ると no_parent。
導出が示さないこと：多項述語・規則のある述語・個体間の関係をまたぐ併用、四つを超える分割や 10 を超える語彙、文脈をまたぐ併用、情報を失う変換（射影 R4）を段に含む鎖（X10 のうち、失われた区別が後段で回復しない部分は、分割の鎖では「記録に区別がないこと」の非回復としてのみ検査し、射影を含む鎖は範囲外）。
5. 契約の適用：COMP と R6 では足りない
併用の拡張は、読み取り専用で、公理を加え（R2、R6）、さらに複数の使用を合成する（COMP）。既存のクラスの義務を点検する。
| 既存の義務 | 併用での扱い |
|---|---|
| COMP-1 各段を実体から再計算して照合 | 構造・語彙・判定を、宣言した分割から再計算する（要求や個別の認定票の主張を使わない）。そのまま適用できる |
| COMP-2 範囲は各段の交差 | 鎖では、前段が定める個体に限り後段が定まる、と読み替える |
| COMP-3 途中の損失は後段で回復しない | 射影を含まない鎖では、「記録にない区別」の非回復になる。読み替えが要る |
| R6-2 旧データでの無矛盾（単独の分割） | 併用では無条件に成り立たない（J3）。判定との一致（J5）に読み替える |
COMP も R6 も問わないことが四つある：①独立な併用が個別の結果に分解できること（J1）、②記号を共有する併用の保存性を、個別の認定と独立に、併用全体で正確に判定すること（J2・J3）、③判定とデータの結果の一致（J5）、④個別の結果と併用の結果の差を隠さないこと。新しいクラス JOINT（併用：記号を共有し得る拡張の合成）を定義する。必須の義務は、共通の K-ID・K-STOP・K-INV・K-RES、R2-1〜R2-5、R6-1〜R6-6（R6-2 は J5 への読み替え）、および次の六つ。
| 義務 | 内容 |
|---|---|
| JOINT-1 構造の再計算 | 併用の構造・成分・旧記号と新記号を、宣言した分割から再計算する。個別の認定票・自己申告の構造を根拠にしない |
| JOINT-2 独立な併用の分解 | 成分が単独の分割は、併用での状態が単独での状態に等しい（differs が偽）。拡張の独立（L3）は機械的に検査できる |
| JOINT-3 共有記号の併用は全体で再判定 | 保存性は併用全体の公理の下で全数で判定する。個別に保存的でも不認定になる例（K04 型）で反例を返す。判定は旧データでの結果と一致する |
| JOINT-4 鎖の範囲と非回復 | 後段の状態は前段が定める個体に限り定まる。前段で区別されないものを、後段の分割だけで葉まで確定しない |
| JOINT-5 範囲の明示 | 語彙 10、分割 4、規則のない単項述語、一つの文脈・個体。範囲外は拒否する |
| JOINT-6 差を隠さない | 個別と併用の結果の両方と differs、旧記号だけの状態で併用が矛盾する場合の interaction_violation を返す |
これは契約の不足の発見であり、19 の §10 の「クラスの義務表が完全であること」の未解決への、P2-c の追加の実演でもある。JOINT が他の併用に十分であることは主張しない。
6. 宣言（案）
| 項目 | 内容 |
|---|---|
id・class |
p2-split-combination・JOINT |
depends_on・reads_extensions |
p0-positive、p2-concept-split。p2-concept-split の単独の分類（classify）を読むので、読む拡張に宣言する |
owns |
操作 check_split_combination・query_split_combination、schema p2-splits-request-draft-1・p2-splits-result-draft-1、profile と能力 p2-split-combination-draft-1、回答型 joint_candidate_set |
spec・pins |
src/med_dsl/splits_spec.json（生バイトの hash を実装に固定） |
| 証拠の強さ | K-・R2-・R6-1・R6-4・R6-5・JOINT-1・JOINT-5：checked_native_template。R6-3・R6-6・JOINT-2・JOINT-4・JOINT-6：finite_check（全数列挙・オラクル・差分）。R6-2・JOINT-3：hand_derivation（一般の旧モデルへの拡張は J2 の手作業の導出。全数の検査が支える）。拡張全体は最も弱い finite_check |
7. 検査の計画
| 条件 | 検査 |
|---|---|
| X08 | 独立な拡張の組を機械的に列挙し、任意の部分集合を同時に載せて、全例の結果が単独と一致。順序の入れ替え。独立でない組（併用の拡張と分割）は、片方を不活性にすると他方が変わる（宣言の依存が実体に合う） |
| X09 | K04 型の例（部分を共有する二つの分割）：単独の判定は保存的、併用は不認定で反例を返す。部分を共有しても保存的な例も認定する。全数列挙による判定と、オラクルの独立な判定の一致。判定と、旧データのみの状態の結果の一致（J5）。個別の認定票を受け付けない |
| X10 | 入れ子：前段の除外が後段に流れる例、前段が区別しない個体は後段で葉まで定まらない例、併用の結果が単独の順次の合成と異なる例 |
| 全体 | 分割の連結成分ごとの分解（J1）、乱数と全数の差分、予算の掃引、拒否の防護例（義務ごとに設計時に付ける）、変異検査 |
8. 範囲外と未解決
- 射影（R4）などの情報を失う段を含む鎖。X10 のうち「失われた区別は後段で回復しない」は、分割の鎖では「記録に区別がないこと」の非回復に限る（一部達成として記録する）。
- 異なる種類の拡張どうしが記号を共有する併用（分割と定義の追加など）。K04 型は、分割どうしの共有で実演する。
- 複数の文脈・複数の個体をまたぐ併用、述語に規則がある併用、語彙が 10 を超える併用。
- 併用の結果から基底の状態への変換（橋渡し）。必要なら R5 の別拡張。
- 契約のクラス JOINT の義務表が他の併用に十分であること。