後続：追補記録（RV-01 の対応と RV-05 の裁定）。本書の本文は初版のまま保持し、判定の更新は追補に記す。
記録様式 に従う実施記録です。状態：AI による確認記録・独立性は認定しない・裁定者未割当・合格判定なし・評価用正解の凍結なし。計画書 §3 により、別実行や別スレッドであることを理由に独立レビューとは数えません。この記録で independent_review / evaluation_frozen は false のままです。作成者側の 証明義務 と 事前監査 は参考資料として読み、判断の根拠は固定コミットからの再実行と、私が別に書いた検査に置きました。
開始情報
| 項目 | 記入内容 |
|---|---|
| 記録ID・開始/終了日 | AI-001。開始・終了とも 2026-10-19（単一セッション） |
| 意味/実装レビュアー、資格・経験 | 1 者（AI：Claude Sonnet 5.5）が意味と実装の両方を担当。人の資格・経験は該当なし。形式証明支援系による機械検証は使っていない。意味の導出は手作業で再構成し、有限領域の全列挙と乱数照合で補った |
| 作成者との関与と独立性の判断 | 独立とは認定しない。 (1) 本リポジトリの作成にAIが関与したか、私がその作業を行った同一の主体かを、コミット履歴（共著表記なし）と本セッションの文脈からは確認できない。「関与なし」とも言えない。(2) 計画 §3 の規定どおり、別実行という理由だけでは独立と認めない。(3) 利用者の依頼文により本レビューを開始したが、計画 §3 が求める「担当と範囲の承認、共有した作成者情報、確認方法」の正式な記録は利用者の確認が必要。(4) 作成者の整理資料は読んだ。ただし実装を読む前の期待・反例は別ファイルに先に残した（下記） |
| 裁定者・必要になった理由 | 未割当。RV-01 の重大度（S1 かS2か）と RV-05 の意味の問いで必要 |
| 基準コミット・追加資料コミット | 基準 e73d4bab30cbb40b9354724c361610d5c22033c1（P1-d）。レビュー資料 559244d9e64580652b316bc15e36236c966ed934。git diff e73d4ba 559244d は既存文書5件の変更（README.md、docs/architecture.md、docs/research.md、docs/roadmap.md、examples/README.md）と追加7件（16番台の文書4件、PR01 例、監査 script、監査 test）のみで、runtime・既存テスト・既存例・契約は不変 |
| 基準manifest・実体束・追加監査束のhash | 共通manifest生バイト 1f01ed6593f555b42e370661c225fac1012bdf89b115bc29fd91513474d35efb、168ファイル束 561ef3924483c4f36c0ec3edec571979dd2418a880ac84320c70bfe7f36ef864、追加監査6ファイル束 88f606a8227cc90c0790412ecb7cb82da75fb7f28b5996302cd316f56577530e。評価器とは別の自前コードで、168ファイルの生バイトhash・サイズ・束digestを再計算して一致を確認。168ファイルは e73d4ba と 559244d で同一 |
| 対象範囲・除外範囲と理由 | 対象：PO01〜PO12、P0/P1 の全 117 例（P0 37 / P1 80）、src/med_dsl/*.py の認定・停止・入力検査の各分岐、評価器 evaluate-p1-d.py、追加監査。除外：医学的妥当性、外部処理系、性能・可用性、R4 の架空40件、実体系・実データ（D03 に従い持ち込まない）、Python 3.11 での実行（環境になく未確認）、人による独立確認 |
実装を見る前の期待・反例は、計画書・証明義務・P1契約・R5を読んだ時点（src/ 未読）で g1-expectations-before-reading-code.md(Git管理外・非公開)（SHA-256 c8fb8c7d1374f41af5c164a5798df105d65f75dc059476f9e9452943b30e9864、Git管理外）に保存しました。「読後追加」と書いた項目はその後に気付いたものです。
POごとの判断
判定欄の「適合」は、AI 単独・非独立・下記の範囲での確認を意味します。未解消の S1 が関わる PO は計画 §7 に従い「未判定」とし、合格に数えません。
| PO | 前提・結論の再構成、確認したコード/仕様 | 実装を見る前の期待・反例 | 実行/証明の根拠 | 判定・確認者・日付 |
|---|---|---|---|---|
| PO01 | 依存は digest(package)（内容の canonical hash）で結び、閉包・所有者一意・役割整合を検査。validation.py の _registry/_closure/_signature/validate_extension を全文確認。hash は内容固定であって意味同一性の証明ではない、という文書の区別は妥当 |
旧側だけで依存が解けるか、新記号の共有・上書き・循環・隠れた追加包含で崩れないか | 変異 V01/V02/V04/V06/V08 を既存テストが検出。ランダム拡張 5,200 件（依存パッケージ・追加包含・自己参照を含む）で認定 576 件がすべて有限モデルで保存的、偽認定 0（§検査1） | 適合（有限範囲）・AI-001・2026-10-19 |
| PO02 | S1：N:=ψ の解釈、S2：N:=∅、依存順の帰納、旧語彙への制限、を再構成して妥当。前提は「非空ソート・新記号のみ・非循環・右辺が旧語彙と前の新記号のみ・新所属データなし」。実装は definitions.py check_extension。defined/subtype の定義は自モジュール宣言の述語だけに限られ（validation.py:145）、旧記号の定義上書きは構文で不可能 |
追加包含、定義欠落、循環、記号共有、旧記号への隠れた制約 | 作成者の200プログラム監査は認定されるべき族だけを走査し、拒否すべき入力の誤認定は走査しない。補うため、認定 576 件の全てで追加後の全解釈（領域1〜3）の旧語彙像が旧モデル集合に等しいことを確認。認められた不完全性（保守的拒否 1,431 件）は欠陥に数えない。変異 D01〜D03/D05/D06 を検出（D04＝拡張認定の予算0は機能テストが検出せず、RV-07） | 適合（単項S1/S2、領域1〜3の有限確認）・AI-001・2026-10-19 |
| PO03 | 肯定結合と ground 明示否定、未決/否定/衝突/未知/打切りの区別。query.py・definitions.py の閉包・ledger.py を全文確認。衝突は文脈単位（契約 06 §P0 の記述どおり）で、無関係なクエリも conflict になる過保守は契約どおり | 未決と非含意の混同、否定を偽に変えること、部分結果の完全回答化 | PO04 の集合定義と Horn 閉包と全探索結合を独立に書き直したオラクルと、乱数 10,000 件×全ビュー×全クエリで status と binding 集合が一致。変異 Q01/Q02/Q05/Q06 を検出（Q03/Q04/Q07/D08＝結合1000の境界・予算消費後の事前打切り・未知能力文脈の予算0・証明の選択は機能テストが検出せず、RV-07） | 適合・AI-001・2026-10-19 |
| PO04 | V/C/S/A/Pending/Unknown を集合として再実装して一致。訂正元が後で訂正されても古い記録を復活させない方針は契約記載どおり。ledger.py 全文確認。入力検査で訂正は「同じ文脈・同じ atom（符号を除く）・厳密に早い時刻」に限られ、自己訂正・循環訂正は構文で不能 |
時点直後の確認、AI確認、未確認の訂正元、訂正済み・保留記録の未知能力 | 乱数 10,000 件で一致。変異 L01〜L07/V05/V07 を検出（V03＝訂正と元が同時刻の境界は機能テストが検出せず、RV-07）。付記：確認時刻が主張時刻より前でも採用される（RV-05、意味の問い） | 適合（RV-05 は裁定待ち）・AI-001・2026-10-19 |
| PO05 | 一階の事象化：四役割を同じ z に結び、予備要素で非空を保つ構成は妥当。充足対応は原子式の一致と構造帰納、被覆は Z = O の四つ組 ⊔ {予備}。実行表現 events.py（_expand/_event_facts/_restore）と reference.py を全文確認。導出文書の前提に1点の書き落とし（RV-06） |
別の証人を混ぜる誤翻訳、同 key/同四つ組の重複、新鮮 ID の衝突、匿名の存在から名前付き事実の捏造 | 乱数 10,000 件で legacy / native / オラクルが一致、認定は「全 status ∈ {supported, undetermined, opposed}」と一致。参考意味は 1,500 理論の証明 746 件が領域2の全モデルで健全（捏造 0）。変異 E02〜E13 を検出。参考意味の証明理由コードに矛盾（RV-02） | 適合（RV-02/06 付記）・AI-001・2026-10-19 |
| PO06 | 原子ごとの新鮮な内部変数、結合後に旧変数へ射影、同じ binding の根拠を統合。events.py _expand/_bindings |
同 key・同四つ組の根拠を失う、内部変数が旧変数と衝突する | 乱数で evidence まで一致（認定が evidence の同一を要求するため）。変異 E11（共有 z を外す）・E12（根拠統合を外す）を検出。内部変数名の衝突回避は used 集合で保証されることを確認 |
適合・AI-001・2026-10-19 |
| PO07 | 有限合成 E02=E12∘E01, r02=r01∘r12 の再構成は妥当（包含 E01(q)∈Q12 と中間実体の同一が前提）。handover.py validate_chain/run_chain 全文確認。段票は要求側が組み立てた値でなく実体から再計算した値と比較される |
票の文字列一致だけでの認定、再hashした改変の通過 | 297 個の葉を一つずつ改変した鎖で、認定を維持するもの 0。偽造・再hash改変 12 通りはすべて不認定か入力不正。乱数チェーン 10,000 件で認定と独立期待が一致。ただし票検査の分岐 handover.py:176 を無効化しても全テスト・全必須パスが通る（RV-01） |
未判定（実装挙動は期待どおり／評価欠落 RV-01 の解消待ち）・AI-001・2026-10-19 |
| PO08 | 因子化条件と喪失の不可逆性の再構成は妥当。projection.py 全文確認。保持列に含まれる Q だけを in-scope とし、全 Q が in-scope のときだけ認定。別添えは additional_source_used と分離 |
同じ射影値で旧回答が異なる二記録、二段目の無損失や別添えを全体の復元と混同 | 手作成の混在スコープ・不整合別添えで正しく動作（gap_probe.py）。混在スコープの認定条件（122行）、衝突の反例（119行）、別添えの照合（69〜70行）を壊しても全テストが通る（RV-01） |
未判定（RV-01 の解消待ち）・AI-001・2026-10-19 |
| PO09 | 未対応・未知能力・衝突・上限を偽/0/空差分へ変えないこと。全分岐を確認 | 予算の境界、「supported を返したが負例の走査前に予算切れ」、完了済み行の汚染 | 予算 0〜（steps+3）の全値を、固定 117 例（21,855 評価）と乱数 P0/事象/チェーン（32,897 評価）で掃引：完了行は無制限実行と一致、打切り時に certificate/answer なし。入力構造の乱数改変 79,560 件で未捕捉例外 0。付記：forecast の incomplete の扱い（RV-03）、境界値の個別検査欠如（RV-07） |
適合（RV-03/07 付記）・AI-001・2026-10-19 |
| PO10 | 予測型の保持、報告の人確認と臨床発生の分離。forecast.py 全文確認。臨床 assertion・supported を出す経路は存在しない（出力 status は computed/undetermined/opposed/conflict/unassessed） | 1/1 を臨床肯定にする、AI報告を採用する、別モデルの混合 | 乱数 1,500 リクエスト・3,761 回答でオラクル（採用・未知・衝突・有理数）と一致、62 bit 有理数を含む。付記：文脈主体と artifact 主体の照合（forecast.py:141-142）の負例がない（RV-07） | 適合・AI-001・2026-10-19 |
| PO11 | 保存バイト・解釈可能性・旧処理系可用性・新側保証の分離。handover.py _validate_archive/_run_archive。executed:false、availability_scope の明示は妥当 |
保存バイトだけで実行可能とする、runtime の ref だけ合って hash が違う | 変異 H10/H14/H15/H23/H24 を検出。H11（runtime 要求の hash 照合）・H12（依存の hash 照合）・H25（runtime 要求数）を外しても全テストが通るが、固定コードは期待どおり（gap_probe*.py）（RV-01） |
未判定（RV-01 の解消待ち）・AI-001・2026-10-19 |
| PO12 | 実体 hash の追跡と票の主張範囲。評価器 evaluate-p1-d.py を全文確認。型付き比較は JSON canonical bytes による（trueと1は別）。正例 15 件が認定/computed 等を要求し、全部棄権では通らない |
型の取り違え、分母の欠落、全棄権で通る評価、実体の未追跡 | 168 ファイルを自前コードで再計算し一致。変異 108 件のうち、機能テストと必須パスが検出したのは 75 件。27 件が生存し、6 件は P0 実体 hash の固定（handover 系の実体照合）でのみ失敗（RV-01/07 と等価変異）。認定系 claim キーを検査しない例が 12 件。認定票が認定器実装の同一性を持たない（RV-04）。Python 3.11 は未実行 | 未判定（RV-01・RV-04 の解消待ち）・AI-001・2026-10-19 |
集計：適合 8（PO01〜06、09、10）、未判定 4（PO07、08、11、12）、不適合 0、対象外 0。
実装を見る前の反例候補とその結果
| 反例候補（コード未読時点） | 結果 |
|---|---|
PO02：自由変数・ソート不一致・後続記号の参照・記号共有・A→N（頭が新記号） |
単項・同一役割に限る入力検査と、定義は自モジュールの宣言述語に限る構文で排除。循環・共有・隠れた追加包含は不認定。乱数拡張で偽認定なし |
| PO04：自己訂正・循環訂正・訂正元が未確認・時点直後の確認・訂正済みの未知能力 | 訂正は「同文脈・同 atom・厳密に早い」に限られ自己/循環は入力不正。未確認の訂正元は無効。未知能力は可視全件が対象。いずれも期待どおり。確認の時刻が主張より前でも採用（読後追加、RV-05） |
| PO05：同 key／同四つ組の重複、事象定数の一意名仮定、内部変数の衝突 | 重複は別事象として保持され旧回答は一致。新鮮 ID は原文字列全体と衝突検査。一意名仮定は導出文書に明記がなく RV-06 |
| PO07：再hashした改変、改名の非全射・衝突・役割入替 | 実体から再計算して拒否。改名は全域・単射・非捕獲を検査（置換の入れ替えは保守的に拒否）。票の検査自体の負例が不足（RV-01） |
| PO08：同じ射影値で旧回答が異なる二記録、別添えの混同 | 反例を記録し不認定。別添えは追加入力として分離。認定条件・反例記録・別添え照合の負例が不足（RV-01） |
| PO09：supported を返した後の負例走査前の予算切れ、部分結果の完全回答化 | 衝突検査は閉包完了後・回答前に行われ、打切りは解釈済み行を汚さない（掃引で確認）。境界値の個別検査は不足（RV-07） |
| PO10：63 bit／4096 bit の境界、AI 報告の採用、型の混入 | 63 bit は検査あり。4096 bit は入力上限の下で到達不能（RV-07）。AI 報告は人の確認がなければ保留 |
PO12：trueと1、1.0、欠落パスの null 一致、全棄権で通る評価 |
canonical bytes による型厳密な比較で全て区別。欠落は不一致。正例 15 件が全棄権を排除 |
指摘・不一致・修正
重大度は私の案です。裁定者は未割当で、担当欄はすべて「作成者側」を想定した割当案にとどまります。固定コードの修正やテスト追加は、旧版を保持した別版で行う必要があり、今回は行っていません。
| 指摘ID・PO・重大度 | 固定した再現入力・期待・実際 | 双方の根拠・裁定 | 修正版commit・影響範囲・再確認 | 担当・状態 |
|---|---|---|---|---|
| RV-01・PO07/08/11/12・S1（評価の見逃し） | 認定・可用性・射影の主要ゲート7箇所を一つずつ壊しても、機能テスト213件と117例の全必須パスが通る（詳細 §RV-01）。固定コードは正しく動作。 | 私：主要経路に負例がなく、将来の退行を検出できない。作成者側の反論候補：コードは正しい、乱数検査でも守られる。裁定未実施 | 未修正。追加案：7つの負例 fixture と、全例の予算掃引テスト。影響：H16/H17/H19 の期待結果と回帰分母（別版） | 作成者側・未割当・未判定 |
| RV-02・PO05・S2 | 参考意味：source {∀x(A→B), A(a)}、target {A(a)}、モデルなし。期待：target が弱いので未証明なのは model_reduct。実際：model_coverage:true、model_reduct:null なのに certificate.reason_codes=["model_coverage_not_established"]（reference.py:241） |
私：同じ結果内で矛盾する説明。認定の誤りではない（not_certified は正しい）。一方 source ⊂ target では正しい理由になる | 未修正。提案：未証明の側で理由を選ぶ。付随：handover.py:208 の incomparable_execution は mismatch も含む名前になっているが現行義務では到達不能 |
作成者側・未割当 |
| RV-03・PO09/10・S2 | examples/p1-a/unknown-capability.json：行は unassessed/unknown_capability だが、最上位は status:ok、incomplete:[]、reason_codes:[]（forecast.py:177,261）。P0 query と P1-b では unassessed 行が incomplete に列挙される |
12 契約は incomplete を打切りの文脈でのみ述べており、仕様違反とは言えない。プロファイル間の不一致 |
未修正。提案：契約に明記するか、forecast でも未評価行を列挙 | 作成者側・未割当 |
| RV-04・PO12・S2 | 認定票（chain/reference/projection）は方法・範囲・対象 hash を持つが、認定器の実装の同一性を持たない。実行時の固定は仕様JSONの hash と P0 の5ファイルの hash だけ（handover.py:35-50）。events/handover/projection/reference/forecast の各 .py は実行時に固定されない | PO12 の「固定した実装を信頼する前提」は文書にある。一方 profile_spec_sha256 は仕様JSONのhashで、実装ではない点が票から読めない |
未修正。提案：票へ実装束 hash を載せるか、「実装同一性は外部 manifest で追う」と票の説明に明記 | 作成者側・未割当 |
| RV-05・PO04・S2（意味の問い） | assertion h7 を 2026-01-02、その確認 r7 を 2026-01-01 に記録し、as_of 2026-01-03：supported、adopted=[…,h7]。as_of が確認時刻と主張時刻の間なら主張は不可視 |
PO04 の式（recorded_at ≤ t の確認があれば C）には適合。時刻の前後関係を要求する文言は契約にない。構文妥当性と運用上の妥当性の区別 |
意味の問い：入力不正とするか、現状を契約に明記するか | 裁定者未割当 |
| RV-06・PO05・S2（文書） | 証明義務 §5・R5 C1-a の被覆の構成は「四つ組ごとに一事象」。同じ四つ組を持つ二主張の事象定数 e1,e2 を同じ要素へ読むため、事象定数に一意名仮定・不等式を課さないことが被覆の前提になるが、明記がない（「key の一意性等を追加しない」だけ） |
導出は正しく、前提を1行足せば足りる。実行表現は件数を保証対象外としており整合 | 未修正 | 作成者側・未割当 |
| RV-07・PO09/10/12・S2 | 小さな網羅性の欠落：events の上限 4096/1000（events.py:238,248）、P0 の結合上限 1000 の境界（query.py:38）、回答前の予算消費後の事前打切り（query.py:47）、未知能力文脈での予算0（query.py:80-81）、拡張認定の予算0（definitions.py:11）、導出の証明選択（definitions.py:111）、訂正と元が同時刻の境界（validation.py:309）、関係 ref の一致（handover.py:131）、文脈主体の照合（forecast.py:141）、存在規則の形の絞り込み（reference.py:190）に、境界・負例がない。forecast の 4096 bit 中間値上限は、入力上限（63 bit×64世界≦約4033 bit）の下で到達不能で、検査も不能 | 固定コードは期待どおり（拡張認定の予算0＝resource_limit、未知能力文脈の予算0＝resource_limit、同時刻の訂正＝invalid_revision を確認）。境界の全網羅は文書でも主張していない |
未修正。提案：到達不能であることを仕様に注記、境界値は個別に追加 | 作成者側・未割当 |
| RV-08・PO03/05・判断のみ | PR01（逆向き存在規則）は unassessed、B(a) は not_entailed |
仕様どおりの限定と判断する。非含意や名前付き事実への誤変換はなく、証明義務 §2・事前監査 §3 の説明で足りる。推論範囲の拡張は別の判断 | 変更なし | 完了（指摘ではない） |
RV-01 の内訳
検出の数え方：231テストのうち、実体 hash を固定する評価系の18件（test_p0_evaluation・test_p1_evaluation）は、固定対象のどんな変更でも失敗するため、変異の検出には数えていません。残りの機能テスト213件と、117例の必須パス（評価器の check_paths と同じ比較）で判定しました。P0 の5ファイル（model/validation/definitions/ledger/query）は handover 系の操作で実行時に hash 照合されるため、これらの変異は handover 系のテスト・例も失敗させます。それだけが失敗の原因の変異（6件）は検出に数えていません。実体 hash の固定は変更の検知であって挙動の検査ではなく、正当な変更後に --create-snapshot で再固定された後の退行は、機能テストと必須パスだけが守ります。
| 変異 | 場所（e73d4ba） | 壊すと何が起きるか | 固定コードの確認結果 | 追加すべき負例 |
|---|---|---|---|---|
| H07 | handover.py:176 段票と実体の再計算値の照合 | 両段で整合した偽の政策・依存・範囲 hash、始端/終端票の改竄を通す | 偽造 6 通り（始端・終端・中間の政策/依存/範囲・段種別）をすべて chain_obligation_failed |
一貫して偽造した票 3〜5 件（H16） |
| H11 | handover.py:320 | ref が med-dsl:p0-native@1 で hash が違う runtime を「利用可」とする |
unavailable／unknown_runtime_handler |
runtime の hash 不一致（H19） |
| H12 | handover.py:319 | 要求 hash と保存 hash が違う依存を「供給済み」とする | unavailable、stored_bytes_verified:false |
依存の hash 不一致（H19） |
| H25 | handover.py:282-283 | runtime 要求が 0 件でも ready_to_replay になり得る |
invalid_input:expected_one_runtime_requirement |
runtime 要求 0 件（H19） |
| P02 | projection.py:122 | 一部の Q だけ保持列に収まる射影を certified にする |
not_certified、certificate.scope.query_ids=["q1"]、query_out_of_scope |
保持列に収まる Q と収まらない Q の混在（H17） |
| P03 | projection.py:119 | 同じ射影値で旧回答が異なる反例の記録が消える | verified_collision、counterexamples[0]。ただし lossy-composition.json は counterexamples/evidence_level を必須パスにしていない |
同例に必須パスを追加（H17） |
| P04 | projection.py:69-70 | 元記録と異なる別添えを受理 | invalid_input:sidecar_mismatch |
自己整合した hash の別添えが元と不一致（H17） |
補足：認定系 claim（certificate/model_coverage/second_step_certificate/semantic_handover 等）を必須パスに持たない例が 12/117 あります（p1-b conflict・unknown-capability、p1-c no-countermodel-no-proof・existential-without-named-witness・finite-check-is-not-coverage・finite-check-without-countermodel・sidecar-is-additional-input・full-column-identity・kept-query-scope・discarded-query-scope・stored-runtime-is-not-handler・missing-dependency）。一覧は strength.py で再生成できます。
作成者の追加監査（559244d）との関係：変異 R09（存在規則の前提述語の照合を外す＝不健全な含意）は既存の機能テスト213件と117例では生存しますが、事前監査の存在規則族が検出しました（32 件中 2 件が不合格）。つまりその分岐は追加監査が守っています。ただし追加監査は 20 条件・231 テストとは別の分母で、通常の回帰に入っていません。
実施した検査（§検査）
すべて架空データ。実行 script は data/research/review-001/scripts/（Git管理外）。
| # | 検査 | 規模 | 結果 |
|---|---|---|---|
| 1 | 任意拡張の保存性：認定されたら全解釈で旧モデル集合に一致するか（ext_fuzz.py） |
5,200 プログラム（認定 576、保守的拒否 1,431、非保存的 3,193）、領域 1〜3 | 偽認定 0 |
| 2 | P0 クエリ・事象 native・認定器 対 独立オラクル（fuzz_oracle.py） |
10,000 ケース（認定 8,684／不認定 1,316） | 不一致 0 |
| 3 | 予算掃引（固定例 budget_sweep.py／乱数 budget_fuzz.py） |
21,855／32,897 評価 | 不整合 0 |
| 4 | 参考意味の証明の健全性（ref_probe.py） |
1,500 理論、証明 746 件、領域2の全4,096モデル | 不健全 0。RV-02 を確認 |
| 5 | 予測 対 独立オラクル（forecast_fuzz.py） |
1,500 リクエスト・3,761 回答 | 不一致 0 |
| 6 | 鎖の偽造・葉改変（chain_probe*.py、leaf_tamper.py） |
偽造 12＋依存/第二4項述語の例＋297 葉 | 偽認定 0 |
| 7 | 入力構造の乱数改変（robust_fuzz.py） |
79,560 リクエスト | 未捕捉例外 0 |
| 8 | 変異検査（mutants.py／mutrun.py） |
108 変異 | 機能テスト・必須パスが検出 75、生存 27、P0 実体 hash 経由でのみ失敗 6（§変異の内訳） |
変異の内訳
機能テスト・必須パスが検出しなかった変異は 33 件（生存 27 件と、P0 実体 hash 経由でのみ失敗した 6 件）です。以下は私の分類で、等価か否かは私の判断であり裁定の対象です。
- 冗長な防御で等価と判断（13）：H01、H02、H05、H06、H08、H19（予算切れは後続の commit tick でも再発する）、E14、E16、E17（単独では等価・両方外すと既存テストと私の乱数検査の双方が検出）、E24、R03（自己点検の assert）、P06（canonical JSON の往復は常に成立）、F08（到達不能）。
- 評価欠落 S1（7）：H07、H11、H12、H25、P02、P03、P04（RV-01）。
- 追加監査（559244d）が検出（1）：R09。
- P0 実体 hash 経由でのみ失敗（6）、評価欠落 S2：Q03、Q04、Q07、D04、D08、V03（RV-07）。
- 評価欠落 S2（6）：H20、E18（理由コードのみ）、E19、E20、R06（より厳しい条件を緩めても健全、網羅性の欠落）、F12（RV-07）。
再現記録と結論
環境：Python 3.14.4（標準ライブラリのみ）、Linux 6.18.33.1-microsoft-standard-WSL2 x86_64。Python 3.11 は環境になく未実行。静的に ast.parse(feature_version=(3,11)) が通ることだけ確認した（実行の代替ではない）。
| 対象 | コマンド | 終了 | 結果（分母は別々） |
|---|---|---|---|
| 基準 e73d4ba：開発テスト | python3 -m unittest discover -s tests -v |
0 | 231/231 |
| 基準 e73d4ba：P1-d CLI 評価 | python3 scripts/research/evaluate-p1-d.py --cli --output data/research/p1-d/review-baseline |
0 | P1 20/20条件、80/80 JSON、417/417必須パス。P0 22/22、37/37、221/221（P22 相互関係を含む）。bundle 561ef392… 一致 |
| 追加資料 559244d：追加監査テスト | python3 -m unittest discover -s tests/audits -v |
0 | 8/8 |
| 追加資料 559244d：有限監査 | python3 scripts/research/audit-preservation.py --output data/research/preservation-audit/review |
0 | 拡張 600/600、単項 256/256、存在規則 32/32、PR01 1/1。束 88f606a8… 一致。走査 873,600 解釈・旧モデル 8,800 など文書の件数と一致 |
| PR01 CLI | PYTHONPATH=src python3 -m med_dsl --fixture examples/audits/existential-reversed.json |
0 | unassessed を維持 |
| 空白検査 | git diff --check |
0 | 指摘なし（クリーンな worktree のため自明に通る） |
ログとその hash は data/research/review-001/SHA256SUMS（Git管理外）にあります。実行は隔離した worktree で行い、HEAD の作業ツリーと runtime は変更していません。作成者側の実行（テスト・評価・監査）に失敗はなく、除外した結果はありません。私の検査 script 自身の誤りで再実行したもの（予算掃引の比較フィルタ、予測の乱数生成器の誤記、変異検査の中断、探索用 probe の添字）が計4件あり、いずれも固定コードの不具合ではありません。
結論（対象範囲付き）
- 今回の範囲と手法では、S0 に当たる事象（無根拠な certified、誤った含意、未知や打切りの確定、原情報の消失）は見つからなかった。 これは網羅の証明ではない。
- 未解消の S1 が1件（RV-01）。 固定コードの挙動は期待どおりだが、認定・可用性・射影の主要ゲートに負例がなく、退行を検出できない。計画 §7 により、PO07/08/11/12 は未判定のまま、この限定範囲のレビュー合格とはしない。
- S2 は 6 件（RV-02〜07）と、判断のみの 1 件（RV-08）。RV-05 は意味の問いとして裁定が要る。
- 独立性が認定できないため、この記録で評価用正解を凍結しない（G5 へ進まない）。保証対象は「作成者草案の実装が、記載の有限領域と乱数照合の範囲で、私が書き直した参照計算と矛盾しなかった」ことまでで、体系の永続性・一般の保存判定・無限更新・臨床妥当性には及ばない。私の参照計算は文書に書かれた PO04 の集合定義と Horn 閉包に従っており、その定義自体の誤り（たとえば訂正元を復活させない方針の妥当性）は、この照合では検出されない。
未確認点と次の作業
- 人または別系統の確認者による独立確認、裁定者の割当、独立性の判断。
- Python 3.11 での実行。他の OS。
- 417 の必須パスを人手で一件ずつ再導出していない。確認したのは、認定を要求する 15 例の読み直し、強度の不足 12 例の特定、変異・乱数による照合まで。
- 参考意味の健全性は領域2の全モデルまで。3要素以上の反例は走査していない。
- 変異・乱数検査の対象外：P0 比較（
compare.py）の変異、事象のsplit_roles診断経路と反例生成（固定例のみ）、cli.py。乱数生成器は依存パッケージ・複数文脈・第二の4項述語を限定的にしか含まない（固定の手作成例で個別に確認）。 - 形式証明支援系による機械検証。無限列の極限、未知の意味能力に対する一般の E/r/i。
- 次の作業：(1) RV-01 の負例追加と予算掃引の回帰化を、旧版を保持した別版で実施し、H16/H17/H19 を再確認。(2) RV-05 の裁定。(3) RV-02〜04・06・07 の修正または理由付き保留。(4) 上記後に独立確認者が G1〜G3 をやり直し、G5 へ進む。