実施日：2026-10-19。契約版：p0-draft-2。状態：作成者（AI-001）の単独・内部実施の結果。独立確認前。設計 25 に沿って、拡張の独立（L3）、記号を共有する併用（L4）、鎖（L6）を、概念の分割を題材に検査した記録です。述語・主体・文脈はすべて架空で、実在の疾患・分類の分割ではありません。P0/P1 の挙動と契約は変えていません。
1. 到達点
| 項目 | 結果 |
|---|---|
| 拡張の独立（L3） | independent_pairs：基底を除く 11 件の 55 組を機械的に判定し、42 組を独立と判定。独立な拡張の任意の部分集合を同時に載せても、登録と振り分けの順序を入れ替えても、全例の結果が不変 |
| 記号を共有する併用（L4） | 新しい拡張 p2-split-combination：複数の分割（4 個・語彙 10 まで）の併用の保存性を、併用全体の公理の下で全数で判定し、反例を返す。個別の認定は根拠にしない。K04 型（個別に保存的でも併用は不認定）を実演 |
| 鎖（L6） | 入れ子の分割：前段の除外は後段へ、後段の情報は前段へ流れる。前段が区別しない個体は、後段の分割だけでは葉まで確定しない。情報を失う段（射影）を含む鎖は範囲外（X10 は一部達成） |
| 契約の変更 | 新しいクラス JOINT「併用」（R2・R6 の義務＋JOINT-1〜6）を extensions.py に追加。拡張の独立の列挙 independent_pairs を追加。宣言は 12 件目 p2-split-combination（義務 21） |
| 実装 | splits.py、仕様 splits_spec.json（生バイトの hash を固定）。登録は host.py に 1 行。P2-b の split.py から宣言の検査を check_split に切り出した（挙動は変えていない） |
| 例 | examples/p2-splits/ 38 例。期待は設計の意味から手で導出（予算の境界の n だけ測定） |
| テスト | test_split_combination.py 26、test_combinations.py 6、独立オラクル splits_oracle.py。P2 系列は全体で 118 |
| 防護例のない義務 | 0 件（宣言 21 義務に防護例 59 件） |
| 証拠の強さ | checked_native_template 14、finite_check 5（R6-3・R6-6・JOINT-2・JOINT-4・JOINT-6）、hand_derivation 2（R6-2・JOINT-3：一般のモデルへの拡張は手作業の導出）。拡張全体は最も弱い finite_check |
| 変異検査 | 併用 39 件：39/39 検出（等価な変異はなし）。契約の検査（extensions.py）53 件：53/53 検出 |
| 既存の系列 | 開発テスト 231、レビュー系列 52、追加監査 8、P1 の 20 条件・80 JSON・417 必須パス、P0 221 必須パスは変化なし。固定済みの全例・改変入力・予算掃引の 22,052 件の出力は、基準（拡張の追加前）と完全に一致 |
2. 受入条件の結果
| 条件 | 結果 | 検査 |
|---|---|---|
| X08 独立な拡張の併用 | 達成 | 互いに独立な 3 拡張（予測・事象・分割）の全 8 通りの部分集合（残りは不活性）で、不活性にした拡張とその依存先の要求を除く全例（203 要求）の結果が不変（988 件の照合）。登録表の順序を逆にしても全例が不変。独立でない組（併用は単独の分割を読む）は、片方（分割）を不活性にすると他方（併用）の結果が変わり、逆は変わらない：判定が実際の依存を捉える。依存・読み取り・順序・import のそれぞれの条件を、人工の木で一つずつ確認 |
| X09 記号を共有する併用 | 達成 | K04 型：部分を共有する二つの分割は、単独ではどちらも保存的（認定）だが、併用は不認定で、拡張できない旧記号の割り当て（P = 偽、R = 真）を返す。部分を一つ共有しても、各親に固有の部分があれば保存的で、判定は認定する。判定を、全語彙の全数（公理を式として直接評価）で求めるオラクルと照合：1・2 個の分割の全 78 通り（72 認定・6 不認定）と乱数 400 件（347 認定・53 不認定）で一致。反例は、拡張できず、辞書順に最初であることを直接確認。判定とデータの結果の一致：旧記号だけの全状態（144）で、併用が矛盾する状態があるのは不認定のときに限る。個別の認定票は受け付けない（未知の項目として拒否） |
| X10 鎖 | 一部達成 | 入れ子の鎖で、(a) 前段の除外が後段に流れ、後段は単独では no_parent でも併用では open、(b) 前段が区別しない個体は後段で no_parent のままで葉の候補が絞られない、(c) 後段の情報が前段へ流れ、併用の結果が段ごとの結果の順次の合成と異なる、を確認。情報を失う変換（射影）を段に含む鎖は検査していない。「失われた区別は後段で回復しない」は、分割の鎖では「記録に区別がないこと」の非回復に限る |
| X03 非干渉（拡張の追加） | 達成 | 12 件目を不活性にしても、その外の結果は変わらず、中の結果は変わる。固定済みの全例の出力が変わらないことは、22,052 件の比較で確認 |
| L7/X13 基底変更の波及 | 設計どおり | 登録は host.py の 1 行で、共有の入口の pin の規則により 12 拡張すべての再検証が列挙される |
3. 検査の結果
| 検査 | 結果 |
|---|---|
| 判定とオラクル（JOINT-3） | 上の X09。部分が 2〜4 個、分割 1〜4 個の乱数 400 件を含む |
| 森なら保存的（J4） | 構造が single・disjoint・forest の乱数 149 件はすべて認定。森の十分条件の外（部分の共有・閉路）で認定される併用が 222 件あり、十分条件は必要条件でない |
| 乱数の差分 | 併用 500 件（密な台帳と疎な台帳を交互に）：オラクルと一致（計算 445 行、blocked 55 行。分割ごとの状態 7 種すべて）。個別と併用の差 405 件、相互作用による矛盾 58 件 |
| 密な差分 | 2,500 件で、七つの状態がそれぞれ 25 件以上現れ、オラクルと一致 |
| 構造を直接作った併用 | 互いに素な併用 126 行・入れ子の併用 127 行：判定は認定、構造の分類が正しく、オラクルと一致。互いに素な併用では differs が常に偽 |
| 成分への分解（J1） | 他の分割と記号を共有しない分割 153 件で、併用の結果が単独の結果に等しい。単独の結果は、P2-b の query_split が同じ分割に返す結果そのもの（100 件以上で照合） |
| 基底との照合（X05） | 行の base は、併用を知らない消費側（P0 の query）の結果と、計算した全行で一致。joint の状態の語彙は基底の状態と互いに素。converted_to_base は常に偽 |
| 情報要求の充足可能性 | 要求した候補の部分が肯定されたら、その分割の併用での状態が asserted になる（実現しない主張を求めない） |
| 予算の掃引・決定性・入力の保持 | 40 件の台帳で完了した行は無制限と同一、打切りの行は値を持たない。判定は、完了するか、認定票を出さないかのどちらか |
4. 変異検査
併用の実装・登録のゲートを壊した変異 39 件を、(a) 手で導いた例、(b) オラクルのテスト、(c) 拡張契約・独立の検査で、それぞれ検出できるか調べた。変異は作成者が選んだもの（保存性の判定・構造の分類 13、状態の表・結果の組み立て 11、停止・拒否のゲート 9、課金 4、入力の変更 1、登録 1）。
| 結果 | 件数 |
|---|---|
| 検出（オラクルのテスト） | 39 / 39 |
| うち手で導いた例も失敗 | 38 |
| うち拡張契約の検査も失敗 | 31 |
| うち独立の検査（X08）も失敗 | 31 |
| 例では検出されず、テストだけが検出 | 1（入力を書き換えないこと） |
契約の検査（extensions.py）には、JOINT の追加と独立の列挙で変異 8 件（クラスの接頭辞、必須の義務、独立の各条件：依存・読み取り・順序・import・核の扱い）を加え、全体で 53 件すべてを検出した。順序への依存の変異は、実際の宣言に順序に依存する拡張がないので、人工の木のテストを足して検出した。
変異検査で見つかった検査の穴（修正済み）：
- 候補だけが違う場合を、どの検査も生成していなかった。
differsを状態だけで決める変異（候補の違いを無視）が最初は見逃された。部分 2〜3 個の生成では、状態が同じで候補が違う併用が現れなかった。部分 4 個までの生成と、手で導いた例（状態narrowedのまま候補が [B, C, D] から [C, D] に狭まる）を足して検出できるようにした。 - 例の期待の欠落が二つあった。
converted_to_baseと、singleの情報要求は、宣言の防護例や別のテストが守っていたが、例の期待に含まれていなかった。例の期待を補った。 - 乱数の分布が偏っていた（P2-b と同じ誤り）。 乱数の併用は共有・閉路に偏り、互いに素・入れ子が 400 件中 9 件だった。矛盾する状態も多かった。密な台帳と疎な台帳の交互の生成と、互いに素・入れ子を直接作る生成を足した。
- 変異の「意図した例」の記入の誤りが二つあった（排他を外す変異は K04 の判定を変えない、など）。判定には影響しなかった。
5. 契約についての発見
- COMP（鎖）と R6（公理つき読み取り）では足りず、JOINT が要った。 COMP は順次の合成（各段を実体から再計算し、範囲を交差し、損失を回復しない）を問うが、①独立な併用が個別の結果に分解できること、②記号を共有する併用の保存性を併用全体で正確に判定し、個別の認定を根拠にしないこと、③判定とデータの結果の一致、④個別と併用の差を隠さないこと、を問わない。R6 の「旧データでの無矛盾」（R6-2）は、併用では無条件に成り立たない（K04 型）ので、「判定との一致」に読み替えた。
- L4 の「併用全体で再判定」は、この範囲では正確な判定にできた。 設計は十分条件と有限の反例探索を想定していたが、公理が個体ごとの単項文で、旧記号に公理がないので、旧記号の全割り当てを列挙すれば正確になる（J2）。森の十分条件は近道・照合にとどまり、必要条件でないことが実際に確認された（222 件）。ただし、この正確さは、単項・規則のない述語・個体ごとの公理の範囲に限る。
- 独立の判定は、核のモジュールを固有と数えない。 そのため、実装がすべて核にある拡張（
p0-definitions）は、すべての拡張と独立と判定される。実際に核の関数を他の拡張が使っていても、核の変更は基底の改訂として別に扱う（L1・L7）ので、これは設計どおりだが、独立の判定を「その拡張の固有の実装の独立」として読む必要がある。 - 宣言した読み取りが、独立の判定と無効化の両方で観測できた。 併用が単独の分割の関数（
classify）を読むことを宣言していて、独立でない組と判定され、分割を不活性にすると併用の結果が変わった。宣言を落とせば、P2-a と同じく、非干渉の検査が破れを報告する。 - 検査の穴を、変異検査が見つけた。 例とオラクルが通っても、生成の偏りで確かめていない場合分けが残る（二度目）。結果の分布を要求する検査と、構造を直接作る生成は、この種の偏りへの対策として有効だった。
6. 限界と未解決
- 独立確認は未実施。宣言、義務の導出、例の期待、公理、欠落の理由は作成者の主張で、解釈は覆り得る。
- 範囲：分割の併用（4 個・語彙 10・規則のない単項述語）で、一つの文脈・一つの個体。異なる種類の拡張が記号を共有する併用（分割と定義の追加など）、述語に規則がある併用、多項述語、文脈や個体をまたぐ併用は含まない。
- X10 のうち、情報を失う段（射影 R4）を含む鎖は未検査。
- 判定の正確さは J2 の手作業の導出に依る（全数の検査が支えるが、一般のモデルへの拡張は導出）。
- 変異は作成者が選んだ 92 件で、検出できない退行が他にないことは示していない。
- 次は P2-d（評価の固定、独立確認の準備、版の手順の実演。PO13〜PO18）。