保存条件の証明義務と実装への対応

作成日：2026-10-19。状態：作成者による形式化草案・独立確認前。R5の手作業の導出、P1契約、P1-dの固定結果 を、前提・結論・実装・未確認点に分けます。以下の導出は機械検証済み証明ではありません。レビュー計画 の確認単位です。

1. 対象と記号

意味単位を S=(L,Σ,T,D,H,P,v,Q) とします。Lは版付き意味プロファイル、Σは語彙と型、Tは依存閉包を含む理論、Dは論理的データ、Hは主張・確認・訂正の履歴、Pは採用方針、vは参照時点、Qは保証対象の問いです。DとHは同一ではなく、P0の実行ではHを選択して肯定事実と明示否定を取り出します。

真理の層では非空ソートを持つ古典的なモデルと充足を使い、実行層では supported/opposed/undetermined/conflict/unassessed と公開binding・根拠を使います。undetermined は古典的な非含意の別名ではありません。 参考意味の not_entailed は、検査した反例モデルがある場合に限ります。

一般的な意味引き継ぎは、式の翻訳E、モデル読み戻しr、必要なら変数割当の対応iを持ちます。

r : Mod(T1 ∪ D1) → Mod(T0 ∪ D0)
M1 ⊨ E(q)[η1] ⇔ r(M1) ⊨ q[i(η1)]
各旧モデルM0と対象割当η0を、新モデルM1とη1へ持ち上げられる。

閉じた文なら割当は不要です。自由変数を持つ問いの回答保存を言う場合、モデルだけでなく対象割当も覆う必要があります。今回の事象化では旧ソートと旧変数の値をそのまま残すためiは恒等です。将来、個体の名前や台集合を変える場合は、この条件を省けません。

2. 証明義務の台帳

ID	前提と要求する結論	主な実装	作成者側の現状・残る確認
PO01	旧定義・語彙・依存実体の固定、新記号の所有者の一意性、型の整合	validation.py の registry/closure/signature	既存テストあり。hashは固定の手段で、意味の証明ではない。参照の同一性と意味の同一性を独立レビューで区別
PO02	新記号だけの非循環S1/S2追加なら、全旧Dについてモデルを拡張でき、旧側への制限も妥当	definitions.py の check_extension	下記の手作業の構成＋200定義プログラムの有限監査。一般の必要十分判定ではない
PO03	完了したP0の肯定結合とground明示否定を、固定した採用済み事実に基づいて返す	query.py / definitions.py	古典論理の対偶・爆発・一般の存在推論を要求しない。既存の参照計算と停止テストを精査対象にする
PO04	原履歴の可逆性と選択に用いる全属性の保存から、採用・保留・訂正済みが可換	ledger.py / events.py の restore	下記で集合として導出。方針の同名参照だけでなく、実装と意味の一致が前提
PO05	四役割の同じ証人、旧ソートの保持、不要な制約なしなら充足対応とモデル被覆	P1契約の事象化構成、events.py	手作業の一般構成と有限実装を分ける。runtimeは一般一階式の認定器ではない
PO06	原子ごとに新鮮な内部変数を使い、結合後に旧変数へ射影し、原根拠を対応付ける	events.py の expand/bindings	同じkeyや同じ四つ組の複数根拠を統合して失わない。事象件数・同一性は旧Qの対象外
PO07	実際の中間実体・依存・方針・翻訳後Qが一致すれば、対象範囲内で有限合成できる	handover.py の validate_chain/run_chain	既知の四役割＋単射改名だけを認定。各段の票の文字列一致では足りない
PO08	射影が残した区別だけに依存するQなら保存可能。失われた区別は後段だけでは回復できない	projection.py	下記の因子化条件。別添えは追加入力で、射影単独の可逆性に含めない
PO09	未対応・未知能力・衝突・資源上限を、偽・0・空差分へ変換しない	各query/forecast/events/handover	既存の境界テストあり。意味保存から同じ予算での完了は従わない
PO10	予測型を保持し、報告の人確認と臨床上の発生・モデル精度を分離	forecast.py / forecast_spec.json	有限モデルの厳密な有理数。臨床主張を生成する経路がないこともレビューする
PO11	保存バイト、解釈可能性、旧処理系可用性、新側保証を別に検査	handover.py の audit_replay	registryと提供inventoryの範囲。旧バイナリの実行証明、世界中の所在確認ではない
PO12	認定器のコード・仕様・依存・実行環境と、票の主張範囲を追跡できる	共通manifest、評価器、native handler	固定した実装を信頼する前提が残る。Python/標準ライブラリ/OSやhashの実装を含む完全な機械証明はない

全POは独立確認待ちです。「手作業の導出あり」「有限監査あり」「独立確認済み」を別の状態として扱います。今回追加する有限監査はPO02と参考意味の限定した含意・モデル判定を対象とし、他の全POの実行監査を新たに完了したとはしません。

追加監査で確認した境界 PR01↗ は ∀x(A(x)→∃y(r(y,x)∧B(y))) と A(a) です。手作業ではxにaを代入し、存在するyの連言からB(y)を取り出せるため ∃y B(y) を含意します。B(a)は要求していません。現行の既知構文はr(x,y)の向きだけを扱うので、逆向きはunassessedです。これを非含意としない境界と、将来の推論範囲を広げる判断を分けます。

3. PO02：定義追加をモデルの拡張として示す

旧語彙Σの任意のモデルMを取ります。旧理論・旧Dの解釈を変えず、新記号を依存順に追加します。S1の N(x)↔ψ(x) では N={a | M⊨ψ(a)}、S2の N(x)→ψ(x) では N=∅ を選べます。前に追加した記号を右辺に含む場合も、非循環な順序なら同じ構成ができます。

各段で旧記号を変えず追加公理を満たすので、有限帰納により全体を拡張できます。逆方向は、追加後のモデルを旧語彙へ制限しても旧理論・旧Dを失わないことから従います。旧モデルの反例も拡張できるため、旧文の含意が前後で一致します。整合した旧モデルがあるなら拡張後にもあります。旧モデル自体がない場合の論理的な一致から、医学的妥当性を導いてはいけません。

新記号に新データ N(a) を追加すること、旧記号への追加包含、公理の上書き、存在制約はこの前提外です。二つの追加がそれぞれ保存的でも、同じ新記号を共有するなどで同時に旧モデル上へ構成できなければ、併用は認定できません。P0の所有者検査と追加包含の拒否を、この前提と照合します。

4. PO04：履歴と採用の可換性を集合で示す

有限の履歴H、参照時点tについて次を定義します。確認は、固定したschemaに適合するhuman/confirmed reviewだけを意味します。reviewの存在は臨床的正しさの証明ではありません。p0-draft-2 以降、確認の記録時刻は対象主張の記録時刻以後（等しくてよい）でなければ入力不正で、C に入る確認はこれを満たします（レビュー AI-001 の RV-05）。

V = {h | h.recorded_at ≤ t}
C = {h∈V | h.certainty=confirmed かつ時点tまでの確認がある}
S = {a | あるh∈Cのsupersedesにaが含まれる}
A = C \ S
Pending = V \ (C ∪ S)
Unknown(c) = {h∈V | context(h)=c かつ必要能力を理解できない}

後で訂正された主張もCに入るため、その主張が訂正した古い記録を自動復活させません。UnknownはAだけでなくV全体を対象にします。未確認・訂正済みという理由で、未知の修飾を無影響として落としてはいけません。

履歴変換Fが原ID・時刻・確度・確認・訂正辺・文脈・必要能力を一対一に保持し、読み戻しRがこれらを復元し、方針・理解済み能力も対応しているとします。V/C/Sを決める各条件が保存されるため、各集合の像は新側で対応する集合に一致し、AとPending、未知能力の判定も可換です。原主張の意味だけを移せても、これらの属性が欠ければこの結論は得られません。

肯定・否定の索引はAから別々に作り、negativeの四つ組を個別役割の否定へ分解しません。新側の全履歴を読むことと、採用された肯定だけを活動事象として検索することも区別します。

5. PO05/06：事象化の数学的モデルと実行表現

数学的モデルでは旧ソートを保持し、旧Oの四つ組ごとに活動事象を置きます。新事象ソートを非空に保つため、別に非活動の予備要素を一つ置けます。四役割は関数として一意に定義し、予備要素には非空の旧ソートから値を選びます。これはモデル構成であり、JSONに架空の臨床値を補う指示ではありません。

読み戻しは O(k,s,m,v) ⇔ ∃z(Active(z)∧key(z)=k∧specimen(z)=s∧method(z)=m∧value(z)=v)。原子式で一致し、旧ソートの量化と結合を構造に沿って移すことで、旧式の充足対応が手作業の構造帰納から従います。旧モデルから上記の新モデルを作れるため被覆も成立します。新理論は翻訳した旧理論と必要な型構造に限り、keyの一意性等を追加しないことが前提です。被覆では、同じ四つ組を持つ二つの原主張の事象定数 e1,e2 を同じ要素へ読むので、事象定数に一意名仮定（e1≠e2）も課さないことが前提に含まれます（レビュー AI-001 の RV-06）。

実行表現は原台帳/assertionごとに新鮮なIDを持ち、同じ四つ組の重複根拠も別に残します。モデル構成の「四つ組ごとに一事象」と、履歴中の「原主張ごとに一事象」は件数が異なり得ます。旧Qは存在する四つ組と旧変数だけを見るため、この違いを区別しません。その理由で事象件数・同一性の新しいQまで保証することはできません。

各旧原子の内部zは、その原子の四役割で共有し、他の原子・公開変数から新鮮にします。結合は旧変数で共有してから旧変数だけへ射影し、同じbindingの原根拠を保持します。未採用の活動化、異なるzの役割を混ぜる翻訳、ground否定以外への否定拡張は認定条件から外れます。

6. PO07/08：合成と失われた区別

0→1→2で、各段の実体と前提が一致し、E01(q)が第二段の対象に入るQだけを残すとします。充足対応を二回適用すれば E02=E12∘E01、読み戻しは r02=r01∘r12。旧モデルの持ち上げも二回行えます。履歴と採用の対応は別途合成します。有限段数の帰納で同じ構成ができますが、無限列の極限については極限の意味自体をまだ定めていません。

決定的な射影fと問いqについて、ある回答関数gで q=g∘f と書けるためには、同じf出力を持つ入力同士でqの回答が一致しなければなりません。逆に全ての同一出力の組で一致するなら、fの像の上でその共通回答をgとして定義できます。これは集合上の存在条件で、gを計算できることまで示しません。

したがって f(d1)=f(d2) かつ q(d1)≠q(d2) は、出力単独からの回答復元が不可能な反例です。後段の無損失符号化を合成しても同じです。原記録sを別添えした入力 (f(d),s) は別の関数の定義域であり、元のfの可逆性の証拠にできません。

7. 今回の到達点と未解決事項

保存原理を12の確認単位へ分け、前提から結論までの作成者による導出と実装の対応を明示しました。追加の有限監査は 事前監査結果 に記録します。有限領域で反例がないことは上記の全モデルの証明を代替しません。

未知の意味能力に対する一般的なE/r/iの構成、任意理論の保存判定、無限更新の意味、臨床ライブラリやAIの入力と意味の対応は未完了です。現行のJSON上限・プロファイル断片を最終体系の表現力の上限とはせず、変更時にどの義務を再確認するかを明確にしていきます。