実施日：2026-10-19。状態：作成者による精査済み・独立レビュー未実施（p0-draft-1 の記録。p0-draft-2 での再実行は 17-internal-run-ai-001.md）。12の証明義務、独立レビュー計画書、記録様式 を作成しました。レビュアーと必要時の裁定者は未割当です。
1. 今回進めたこと
保存の主張を、モデルの拡張、参考意味の含意、履歴と採用の可換性、同じ事象の役割結合、合成、射影、資源停止、予測の型、旧再実行可用性へ分解しました。各義務の前提・結論・実装と、手作業の導出・有限検証・独立確認の違いを明示しています。
特に、自由変数の回答保存にはモデルだけでなく対象割当も覆うこと、数学的モデルの「四つ組ごとの事象」と履歴実装の「原主張ごとの事象」は件数が違い得ること、射影の出力だけから答えられるQはその出力で区別できる範囲に限ることを整理しました。新たな意味能力や一般の証明器は追加していません。
レビュー計画は、基準コミットとhash、確認者の専門性と独立性、G0〜G5の開始/終了条件、12 POと認定/停止の全分岐の確認、再現コマンド、重大度、不一致の裁定、修正後の再確認、独立確認済み正解の別版凍結までを定めました。担当者名や承認を仮に記入せず、未割当・未実施を維持しています。
2. 追加監査の方法と結果
nativeの規則生成・閉包・参考ASTのtruthを期待値計算に使わず、今回生成する族の述語を有限集合のbit maskとして直接解釈しました。nativeの実際の認定・モデル判定・含意結果をこの参照計算と照合します。参照計算も作成者が書いたコードであり、独立レビューや全モデルについての形式証明ではありません。
| 対象 | 生成した範囲 | 照合結果 |
|---|---|---|
| S1/S2 の定義追加 | 旧A/Bの包含4通り、Nの定義5通り、Mの定義10通りの計200プログラム。各1/2/3要素領域 | 600/600組でnative認定と旧モデルの読み戻し像を照合。873,600解釈を走査し、旧モデル延べ8,800件の被覆と旧側にない読み戻しがないことを確認 |
| 単項Hornの参考意味 | A→B/B→A/A(a)/B(a)の有無で16理論。前後の全256組。2要素・a=u・A/Bの全16解釈 | 256/256要求、モデルと要求の組4,096件、6問×前後の3,072回答を照合 |
| 存在規則の参考意味 | 前提/結論A/B、r(x,y)/r(y,x)、ground事実4通りの32要求。2要素でA/B/rの全256解釈 | 32/32要求、モデルと要求の組8,192件、384回答を照合。nativeには証人候補を最大3モデルだけ渡し、oracle側は全256解釈を確認 |
| PR01の境界例 | 逆向きの存在規則、名前付き個体と匿名の存在の違い | 1/1例・6必須パスを照合 |
| 監査器のテスト | 隠れた旧制約、誤った含意/反例/認定、全棄権、結果行の欠落、未知と偽の混同 | 8/8テストが通過 |
定義追加は、追加後の全解釈を調べ、旧語彙への制限の集合が旧モデル集合に等しいか比較します。構成した一つのモデルだけの確認ではありません。ただし有限領域と上記200プログラムの範囲です。新所属データ、存在公理、任意の依存DAGをこの件数で検証したとはしません。
参考意味では、nativeがentailedとした回答に列挙内の反例がないこと、not_entailedの証人が実際に該当理論のモデルで問いを満たさないこと、model_coverage/reductの主張が参照計算と矛盾しないことを確認しました。明示文の肯定を必須とする正例もあり、全棄権で通しません。この有限検査で任意の理論の含意や保存を認定しません。
3. 確認した未対応境界 PR01
保存した実行例 は次の規則とA(a)を持ちます。
∀x (A(x) → ∃y (r(y,x) ∧ B(y)))
A(a)
手作業の導出では∃y B(y)が従います。B(a)を導く必要はありません。現行handlerの既知構文はr(x,y)を扱うため、逆向きの存在についてはunassessed/nullを返します。B(a)は与えた有効な反例モデルでnot_entailedです。述語A/Bを入れ替えた対称例でも同じ未対応を確認し、32要求・384回答のうち2回答がunassessedでした。非含意や名前付きの事実への誤変換はありません。
これは現在明示している推論範囲に沿う保留です。レビューでは、説明が十分か、将来その十分条件を広げるかを判断します。今回runtime・native仕様・期待条件を変更して解消したという扱いにはしていません。
代表例の初回生成では、規則だけの向きを反転して候補モデルのrを反転しなかったため、候補がsourceモデルでなくなり、B(a)まで未評価となりました。監査はincompleteの不一致を検出して終了コード1になりました。候補モデルも意図した規則へ対応させ、既存の期待を弱めず、B(a)の非含意とモデル妥当性の確認を追加しました。失敗時の記録・入力・監査実体は data/research/preservation-audit/pr01-first-construction/ に保持しています。これは新しい代表例の構成時の修正で、P0/P1の不具合や独立レビューの指摘ではありません。
4. 固定基準と再現
P1-dの基準は e73d4bab30cbb40b9354724c361610d5c22033c1、共通manifestは 1f01ed6593f555b42e370661c225fac1012bdf89b115bc29fd91513474d35efb。監査前後で固定168ファイルと一覧の一致を確認しました。runtime・元の例・元のテスト・契約・共通manifestを変更していません。
新しい監査は既存の評価系列と分け、script、tests/audits/、新しい文書、PR01を追加しました。共通manifestの対象を再固定して既存結果へ混ぜることはしていません。P1-dの231テスト・全20条件と今回の8監査テスト・追加の有限検査は別の分母です。既存実体が同じであることを確認し、今回その全231テストやCLI評価を再実行したとは記録しません。
python3 -m unittest discover -s tests/audits -v
python3 scripts/research/audit-preservation.py --output data/research/preservation-audit/development
PYTHONPATH=src python3 -m med_dsl --fixture examples/audits/existential-reversed.json
git diff --check
Python 3.14.4・標準ライブラリのみ。3.11自体は未確認です。外部資料やデータは追加していません。監査はP1-dの固定manifestを指定hashで確認し、通常実行で再固定しません。監査自身の6ファイルの生バイトhashを data/research/preservation-audit/development/results.json に保存します。その一覧のcanonical digestは 88f606a8227cc90c0790412ecb7cb82da75fb7f28b5996302cd316f56577530e です。ログは data/research/preservation-audit/unit-tests.txt。いずれもGit管理外です。
今回の実行時HEADは e73d4ba、作業差分あり。コミット後に基準168ファイルと追加監査6ファイルを当該コミットの実体と照合し、検証したcommitを監査記録へ追記します。実行時HEADは書き換えません。
5. 次の開始条件
計画書と事前資料の作成・今回の有限監査は完了しました。独立レビューは担当の割当と独立性の確認から開始します。指摘の裁定と独立確認済み正解の凍結は未実施で、independent_review/evaluation_frozenはfalseです。形式仕様の追加精査や未対応意味の研究は、その状態でも作成者側の作業として区別して進められます。