P0-b：定義追加の認定と正の推論

実施日：2026-10-18。状態：S1/S2 の限定した保存認定と、単項包含・連言定義による推論を実装しました。独立レビュー、P0 全 22 ケースの受入評価、R4 の実行評価、臨床実証は未完了です。最終目標は 変化に原理的に耐える体系 の確立であり、今回の有限例を永続性全体の証明とはしません。

後続の P0-c で主張・否定・未知能力のケースと停止根拠を整備しました。本書の件数・ハッシュ・次の作業は P0-b 時点の記録です。

実装した範囲

部分	動作
check_extension	旧側と追加側をハッシュ付き依存閉包で解決し、S1/S2 の十分条件を検査。旧語彙、新記号、依存実体、適用範囲、未認定理由を返す
合成の検査	追加側の全依存先の定義・包含を検査。二重所有・二重定義は入力不正。追加一般包含・定義欠落・定義循環は未認定
正の推論	S1 は N→各連言要素と連言→N、S2 と一般包含は一方向の規則に展開。有限の事実と証明の固定点を計算する
文脈と採用	各 view・context を分離。人の確認・参照時点・明示訂正を経た肯定主張だけを規則の前提にする
根拠	元の assertion、review、定義・包含への参照を返す。定義根拠はパッケージのハッシュと入力内 pointer まで追跡できる
衝突と未知能力	導出された肯定と明示的否定の衝突でも文脈全体を停止。未知能力がある文脈では推論を開始しない
上限	認定のグラフ検査と規則の ground 適用を計数。途中の認定票や、未完成の閉包に基づく回答を返さない

旧側をまず単独検証するため、追加側の新しい語彙で旧側の未解決参照を埋めることはできません。拡張の参照は旧側と追加側の和で解決するので、初期 P01 のように旧 A/B を extension に再宣言せず参照できます。query のパッケージでは必要な宣言を同梱するか、依存先とそのハッシュを明示します。

認定は旧データを固定した旧語彙の文に対するモデル保存の十分条件です。新しい所属データ、採用方針、対応表の変更を保証しません。条件外の not_certified を非保存・危険の証明とせず、保証欄は null にします。根拠は R5 の S1/S2、実行時の意味は P0 契約 を参照してください。

草案との照合

初期 P01/P07/P10 の JSON は b760c4c の内容を維持しました。今回十ファイルを追加し、期待値を最初の一括照合前に明記しました。開発中に作成した作成者草案であり、独立確認後の正解凍結ではありません。

ケース	JSON 数	必須パスの一致	確認結果
P01	2	11/11	S1 を certified。A(a),B(a) から N(a) と両主張・確認・定義の根拠
P02	2	8/8	S2 を certified。A(a) から B(a) を支持し、N(a) は未決
P03	2	7/7	一般包含の追加は not_certified。追加後には旧 B(a) の支持が生じる
P04	1	2/2	別モジュール間の共有 N の二重所有を invalid_input とする
P05	1	4/4	循環定義は not_certified。非保存とは断定しない
P07	1	6/6	従来の二観察の結合結果を維持
P10	1	9/9	従来の疑い・訂正後の否定・原履歴を維持
P19	2	8/8	空の台帳では旧 A/B は未決。新 N(a) の観察を加えると両方が支持される
P20	1	2/2	同一 N の S1/S2 二重定義を invalid_input とする
合計	13	57/57	P0 全 22 ケースの合格数とは別の集計

P04 はテスト内で単独の N↔A と N⊑B がそれぞれ認定されても、併用時の再検査で拒否されることを確認しました。P19 の二つの query を照合しており、compare 操作を実装したわけではありません。

開発テストと参照計算

Python 3.14.4 で 62 件の unittest が通過しました。P0-a の 36 件を維持・更新し、26 件を追加しました。以前の「定義推論は未実装」と「check_extension は未実装」という能力境界のテストは、実装後の結果に更新しました。初期三例の入力・期待値は変更していません。Python 3.11 自体での実行は未確認です。

• 保存認定とは別の参照計算として、二個体の有限領域で全解釈を列挙。S1、S2、混合連鎖の三例で、追加後の全モデルを旧語彙へ射影した集合が旧モデル集合と一致しました。一般領域の証明を置き換える検査ではありません。
• 正の推論とは別の参照計算として、三述語の全解釈を真理値で評価。S1、S2 と旧包含、一般包含の三理論について、肯定種データの全 8 通り、計 24 入力で全モデル共通の肯定と回答が一致しました。
• 全ての草案例の生バイト SHA-256・サイズと必須パスを確認し、入力を変更しないことを検査しました。
• 同じ引数・同じ文脈が揃わなければ連言から導出しないこと、包含の方向を逆に使わないこと、新しい個体・所属を作らないことを確認しました。
• 依存先に隠れた一般包含・未定義の新記号、依存ハッシュの不一致、旧依存語彙の再導入、役割不一致、未解決参照を検査しました。
• 否定を規則の前提や対偶へ使わず、未確認・将来の主張で導出しないこと、導出後の衝突に両根拠を残すことを確認しました。
• 循環包含・循環定義が有限の query として停止すること、直接主張の根拠を循環で水増ししないこと、複数導出の根拠選択と再実行が決定的なことを確認しました。
• 0・認定途中・閉包途中・閉包完了直後の予算境界で、未完成の認定や途中回答を返さないことを確認しました。

循環定義を query で計算できることと、保存の十分条件を認定できることは別です。証明は事実ごとに短い導出を優先して一つ選び、全ての代替証明は列挙しません。根拠の具体的な選択規則、入力内参照、ステップの計数は契約に追記しました。

再現と記録

外部依存のインストールは不要です。リポジトリのルートで実行します。

PYTHONPATH=src python3 -m med_dsl --fixture examples/p0/definition-extension.json
PYTHONPATH=src python3 -m med_dsl --fixture examples/p0/definition-entailment.json
PYTHONPATH=src python3 -m med_dsl --fixture examples/p0/cyclic-definitions.json
python3 -m unittest discover -s tests

CLI は 0=正常処理、2=入力不正、3=未対応プロファイル/操作、4=資源上限 です。未認定は正常に計算された判定なので 0、二重所有・二重定義は 2 です。13 例を CLI から実行して終了コードと JSON を照合しました。

JSON 結果、unittest の出力、実行日時・環境・ソースハッシュの実験票は Git 管理外の data/research/p0-b/ に保存しました。束のハッシュは P0-a と同様に、src/med_dsl/*.py と tests/*.py の相対パス→生バイト SHA-256 の対応を、キー順・空白なし JSON にして SHA-256 を計算します。実装コミットはこの文書とコードを含む履歴で特定できます。

記録	SHA-256
草案 manifest の生バイト	7247121efbfc2068b882e6a81a14c4997f32e66dda5c0483c4c754577e0fdfdf
実行したソース・テストの束	29d32b7a122dc61b1cd1925b5854fb71461f57cde6796a17e45b09b0f4f4669f

残る作業

次は P0-c の P09〜P15・P17・P21・P22 を JSON 化し、先行実装した主張選択・否定の検索・未知能力の停止を、定義推論との組合せまでケースとして検証します。その後 P0-d で compare と 22 ケース全体の受入評価へ進みます。compare は現在も unsupported_profile / operation_not_implemented を返します。

一般の量化・古典論理の否定推論・確率・新しい存在証人、外部マスターとの変換、永続的レジストリ、確認記録の認証、実際の臨床ライブラリは対象外です。独立確認・R4 の比較評価・全将来の意味能力の引き継ぎも継続課題です。