P1：意味と引き継ぎの契約草案

作成日：2026-10-18。契約草案：p1-design-draft-1。未実装・独立確認前です。研究設計と D09、20受入条件 と併読します。P0 の p0-positive-1 と入出力契約は変更しません。

1. 比較する意味を先に指定する

層	対象	P1 が求めること
真理・含意	指定プロファイルのモデル・理論・データ・式	式の対応とモデル被覆を示す。有限例での一致とは別にする
実行上の支持	P0 の採用済み肯定閉包、明示否定、未決・衝突・未評価	対応する断片の回答状態と binding を引き継ぐ
採用・履歴	主張・確認・訂正・文脈・時点・方針	原履歴の復元と、選択結果の対応を検査する
予測	指定された有限確率モデルの事象	型付きの予測値を返す。発生・臨床判断へ型変換しない

P0 の undetermined を、任意の古典論理での非含意と同一にしません。否定の対偶を使う翻訳は、P0 の支持の引き継ぎと別の契約です。真理条件だけが成立しても、主張の採用・由来を保存したとはしません。

2. 引き継ぎ契約の識別と証拠

引き継ぎ票には次の項目を必須とする設計です。票に自己申告するだけでは認定しません。

項目	固定する内容
参照	票、原・先のコア、意味プロファイル、理論・依存実体、採用方針、翻訳規則の版とハッシュ
対象	旧語彙、データ条件、Q、対象者・時点・用途、返す変数と値の型
対応	式の移し方 E、モデルの読み戻し r、名前・回答値の対応、履歴・根拠の対応
保証	意味の保存、支持の保存、原履歴の復元、または損失付き射影のどれか
義務	モデル被覆、採用の可換性、結合・否定の対応、追加制約なし、合成条件等の検査結果
証拠の強さ	既知テンプレートの導出、有限モデル検査、個別入出力照合、自己申告を区別
停止	未対応式・必要能力・入力不正・計算上限・未解消の衝突と、その該当範囲

状態は certified/not_certified を候補とし、counterexample は未認定の根拠として別欄に残します。有限ケースに一致しただけの票は certified にしません。認定対象は処理系が検査方法を持つ既知テンプレートに限り、未知の検査方法・任意コード・未検証の証明ファイルは自動実行しません。ハッシュは実体の固定であり、意味の正しさの証拠ではありません。

3. C1 をデータ・回答まで明示する

旧側の理論とデータを T0,D0、新側を T1,D1、旧問い合わせ集合を Q とします。各プロファイルの意味を固定し、少なくとも次を要求します。

E : Q → 新側で解釈できる式
r : Mod(T1 ∪ D1) → Mod(T0 ∪ D0)

充足の対応:
  M1 ⊨ E(q)[η1] ⇔ r(M1) ⊨ q[η0]

旧モデルの被覆:
  任意の M0 ∈ Mod(T0 ∪ D0) に対し、
  r(M1) = M0 となる M1 ∈ Mod(T1 ∪ D1) がある。

η は自由変数への値の割当です。P1 の事象化では旧ソート・名前をそのまま残し、旧変数の割当は同じものを使います。別の名前空間へ移す場合は回答値の対応を明記します。任意の新しい匿名事象を旧側の既知の個体名として返しません。

二条件が成立すれば、旧側で含意された q は全ての新モデルでも E(q) として成り立ちます。旧側の非含意の反例モデルも被覆により新側へ持ち上がるので、新側だけで E(q) が確定することを防げます。R5 の C1 をデータと割当を含めて書いた、本プロジェクトの条件付き導出です。

同じ語彙へ A⊑B を加える更新では、モデル内の式の読み方が同じでも、旧 A={u},B=∅ を持ち上げられません。充足対応だけを検査して保存を認定してはいけません。整合性の未判定・衝突を、この含意の式から臨床上の真偽へ読み替えることも禁止します。

支持・採用・由来の別の義務

原主張を移す処理を F、読み戻しを R とします。少なくとも、元の主張・レビュー・訂正関係・時刻・由来を復元できる範囲で R(F(H))=H を要求します。臨床内容の移し方と、台帳参照・ローカル ID の一対一な対応は別に記録します。

R(Select1(F(H), P1, view)) = Select0(H, P0, view)

この一致には採用・保留・訂正済みの状態と各原参照への対応を含めます。方針の意味・参照時点・文脈が一致しない場合は成立を要求できず、保存ではなく方針変更として記録します。その後に、完了した各 query の支持 binding、ground 否定の根拠、衝突・未評価状態を対応させます。新しい翻訳規則を導出根拠へ追加しても、元の assertion/review を失わせません。

4. 既知テンプレート：四項関係から事象へ

旧 O(k,s,m,v) の四つのソートは非空とし、新側でも保持します。新しい事象ソート Z、Active、四つの役割関数を導入します。

E(O(k,s,m,v)) = ∃z:Z (
  Active(z) ∧ key(z)=k ∧ specimen(z)=s
  ∧ method(z)=m ∧ value(z)=v
)

論理的な契約では旧ソートの量化・結合を構造に沿って移し、変数捕獲を避けます。新理論は移した旧理論とこの型構造だけとし、key の一意性・事象件数・新しい所属条件を加えません。

任意の旧モデルについて Z を「O の四つ組の集合と、非活動の予備要素」にし、活動する要素の四役割を射影にすれば読み戻せます。O が空でも Z は非空にできます。予備要素の関数値は非空の旧ソートから数学的に選べますが、観察された臨床データや JSON の補完値として出力しません。逆に新モデルの活動事象を四つ組として読むと旧モデルを得ます。原子式の一致と構造帰納が充足の対応を与えます。これは C1-a の手作業の構成で、一般の自動証明器の実装ではありません。

実行する最初の断片は、有限の四項肯定事実と P0 の正の結合 Q です。対象関係に unary の定義規則は掛からず、既存の単項部分はそのまま保持します。翻訳した結合で内部 z を使っても、返すのは旧 query の変数だけです。新しい z の件数・同一性を尋ねる Q はこの保証外です。

個別記録では、事象 ID は原台帳・assertion の組に対して新鮮に発行し、既存の記録や互いに異なる原主張と衝突しないことを検査します。同じ key の二観察も別事象として保持します。同じ四つ組の複数の支持も原根拠を残し、読み戻した旧回答は集合として重複を除きます。

negative O は四役割全体を否定した主張として移します。negative method や任意の一つの ¬Active(z) へ分解しません。採用後の肯定だけを Active の問い合わせへ使い、否定は四つ組・同じ文脈の否定索引として照合します。訂正・疑い・未確認は先に採用方針で分けます。活動事象の役割が欠ける入力は不正で、架空の方法を補いません。

5. 意味モジュール：有限の予測

予定プロファイル名は p1-finite-forecast-draft-1。仕様・実装の採用版を決める前の識別子です。一つの予測 artifact は、参照、profile と仕様 hash、対象者、文脈、UTC の半開区間 [start,end)、モデル参照、標本空間参照、有限の世界と重み、事象の世界集合を持ちます。start<end を要求し、日数や時差を補完しません。

各世界の重みは {numerator,denominator} の整数比とし、分母>0、0≤分子≤分母、総和が厳密に1であることを要求します。世界・事象の参照は各集合内で一意とし、事象内の世界参照と all_of の参照も重複を認めません。all_of は一つ以上の既知の事象を要求し、空の事象集合そのものは確率0として許します。重複世界、未宣言の世界参照、重みの欠落、誤った総和は入力不正です。正規化や丸めで直しません。返却値は約分した整数比、0 は0/1、1は1/1です。

Pr(E) = E に含まれる世界の重みの和
Pr(E1 ∧ E2) = E1 ∩ E2 に含まれる世界の重みの和

事象が列挙世界のどこに属するかは、この指定モデル内で完全に与えられた集合の定義です。世界に含まれる値や重みを、現実の医療情報の完全性・観察済み状態と同一視しません。別の forecast/model/標本空間の事象同士を合わせたり、独立性を推定して周辺確率を掛けたりしません。

artifact の存在と、その予測が報告されたことの採用を分けます。P0 で表せる forecast_reported(subject,artifact_ref) の主張・別の human review を使い、同じ view で採用された正の報告を参照します。報告の台帳は臨床台帳と別の参照を持ち、臨床 snapshot は書き換えません。文脈の参照・用途も明示し、同じ対象者という理由で臨床文脈と統合しません。報告の subject/artifact/context と、参照した artifact の対象・参照・文脈の一致を検査し、不一致は入力不正にします。確定していない AI 報告は保留し、artifact と由来を残します。人の確認も「そのモデルの予測が報告された」という情報の確認であり、発生・校正・臨床的妥当性の確認ではありません。

結果の候補は status=computed と answer.kind=forecast_probability、有理数値、対象・区間・モデル・artifact・事象参照、報告の assertion/review 根拠です。数値1でも clinical X を supported にする暗黙規則は持ちません。未採用の報告しかなければ undetermined と情報要求、必要能力が未知なら unassessed、解釈するプロファイル自体が未知なら unsupported_profile とし、数値回答は null にします。

臨床部分への影響

認識済みの本プロファイルは予測値を返す読み取り演算だけを持ち、臨床主張・定義・採用方針への書き込み演算を持ちません。この境界と依存閉包を検査でき、元の臨床 snapshot が同じなら、元の P0 問い合わせの入力と回答は変わりません。これは明示した読み取り専用モジュールの条件付き無影響性です。追加処理が共通予算を消費する場合、旧問い合わせが同じ予算内で完了することまでは保証しません。両側の計算が完了した回答を比較し、予算不足は意味の差ではなく未評価として残します。

自己申告した read_only や未知の profile 名だけを根拠に、未知の意味修飾を無視しません。既知の native handler と仕様 hash・操作能力を照合できない場合は停止します。未対応側では P0 の既存の unknown_capability/unsupported_profile の停止を維持します。予測を臨床判断へ用いる明示的な規則を後で導入する場合、それ自体が別の意味・採用方針の変更です。

6. 合成と部分的な引き継ぎ

0→1 と1→2を合成するには、第一の出力と第二の入力の profile/仕様/依存実体/方針/名前対応が一致し、E01(q) が第二の保証対象に入ることを要求します。対象は次の交差に限ります。

Q02 = { q ∈ Q01 | E01(q) ∈ Q12 }
E02 = E12 ∘ E01
r02 = r01 ∘ r12

充足対応とモデル被覆はこの条件で合成できます。採用・由来の対応も別に合成し、各段階と全行程の証拠を残します。途中の射影が失った区別は、後段の無損失符号化だけでは復元できません。原記録の別添えを使うなら追加入力として参照し、射影単体から復元したとしません。

全てを移せない場合は、移せた Q、移せない式と理由、意図した喪失・追加、未評価を別に返します。未対応、モデル反例、衝突、採用の不一致、計算打切りを正常な空差分にしません。旧コアで再実行する legacy_replay は、意味を新コアへ移す semantic_handover と別の経路です。

7. 入出力・上限・認定の着手条件

予定する操作は query_forecast、check_handover、compare_handover。request の実行 schema と全ケースの入出力は P1-a 以降で具体化します。今回の設計例は p1-design-case-draft-1 で、P0 の request schema ではありません。コア・意味・保存形式・出力型・能力の各版を照合し、未知の演算を同じ名前の演算へ代用しません。

工学的上限の初期案	値・単位
request	全体1 MiB、JSON 深さ64
artifact 数・問い合わせ数	request ごと各64
世界・事象・一問の連言事象	artifact ごと世界64、事象64、連言8
有理数の入力	非負整数、各分子・分母63 bit以内。浮動小数不可
有理数計算	最大4096 bitの中間値。超過は resource_limit、丸めない
主張・確認・文脈	snapshot ごと各1,000。P0 の既存制限も維持
原 Q と翻訳	原 Q は最大64 atom/公開変数4。各四項 atom が最大5原子式へ展開するので、翻訳は320原子式/内部変数込み68を上限とする
中間結合・返却	中間 binding4,096、返却 binding1,000。一問の途中結果を完全回答にしない
計算予算	request 全体100,000 stepsまで。比較・合成で共有し、予算0は開始前の打切り

steps の具体的な課金点と全ての境界値は実装前に実行契約へ固定します。有限予測の有理数の加算・比較、事象の所属検査、結合候補検査等を数える案です。論理的な保存の条件と、実行が予算内で完了したことは別です。

既知テンプレートの十分条件・不成立の反例・部分範囲を実行票で区別し、有限モデル検査だけで全モデルを覆う認定を出さないことを最小条件とします。P0 の37例は引き続き回帰評価し、P1 の20件は独立した分母として記録します。