概要
Algorithmic Legitimacy Shift（ALS）理論における有限実験カーネルがLean 4で形式化され、GitHub Actions上で自動検証可能な形で公開されました。
本カーネルが示すのは、AIガバナンス一般において「人間よりアルゴリズムが常に正しい」という規範的な主張ではありません。証明されているのは、確認対象数 ![][image1] に対して人間のレビュー予算 ![][image2] が不足する ![][image3] の有限モデルにおいて、人間レビューには構造的なリスク下限が生じる一方、所定の指数誤差上界を満たすアルゴリズム検証チャネルは、その下限を厳密に下回りうる、という minimax-risk の比較です。
この結果は、「人間が最終確認すれば安全性・正当性が担保される」という素朴なヒューマン・イン・ザ・ループ観に対し、少なくとも有限実験モデル上では明確な反例構造を与えます。重要なのは、人間かAIかという二項対立ではなく、どちらのチャネルが、どの仮定の下で、より低い最悪ケースリスクを持つかを「再実行可能な証明」として比較できる点にあります。
▼ALS理論 Lean
https://github.com/GhostDriftTheory/als-finite-experiment-kernel
1. 抽象リスクから「有限確率モデル」への接地
従来のALSカーネルは、人間とアルゴリズムの比較を抽象的なリスク数値として扱っていました。今回検証を通過したコード群（ALSFiniteExperimentKernel.lean）の工学的価値は、これを「有限集合上の確率実験（Finite Experiment Family）」として明示的にモデル化した点にあります。
-
カバレッジ制約下の人間レビューの限界 (HumanReviewExperiment)
確認すべき項目数（![][image1]）に対して人間の処理能力（![][image2]）が下回る状態（![][image3]）では、人間がどのようなサンプリングを行っても構造的な見落としが生じ、エラー率の下限（humanFloor）を突破できないことが示されました。 -
アルゴリズムによるリスク統制 (AlgorithmSampleExperiment)
対してアルゴリズム側は、十分なサンプル数（![][image4]）とマージン（![][image5]）を確保し、各項目のエラー確率に指数関数的な上界（fieldWrong_exp_bound）が与えられた場合、人間の限界点（humanFloor）を厳密に下回りうることが証明されました（algorithmic_legitimacy_shift_from_finite_experiment_families）。
これにより、理論が現実のログデータや監査トレースをマッピング可能な計算モデルとして接地されました。
2. 感情的ガバナンスから「計算可能なリスク評価」へ
社会システムへのAI導入において、「人間による最終確認」はこれまで倫理的・心理的な安心感の拠り所とされてきました。しかし、カバレッジ制約（![][image3]）が生じる複雑なシステムにおいて、無条件に人間に依拠することは、最悪ケースのリスク（Minimax Risk）の観点で最適でない場合があります。
本証明は、「アルゴリズムが道徳的・法的に優れている」と主張するものではありません。しかし、特定のリスク最小化という合理的要請において、「条件を満たすアルゴリズム検証チャネルへ正当性評価が移る（Shiftする）場合がある」ことを数理的に示した点で、計算可能なリスク管理への移行を後押しするものです。
3. ADIC（計算台帳による高度データ保全）へのインフラ的示唆
この証明構造は、次世代のAIアシュアランスや高責任ロジスティクスにおいて、ADIC（Advanced Data Integrity by Ledger of Computation）のような再検証可能な証拠基盤が重要になる理由を、有限実験モデルの側から説明しています。
人間のレビュートレース（ログ）を残すだけでは、カバレッジ制約に起因するリスクの底は抜け出せません。より安全であることを事後的に検証するためには、恣意性を排除し、アルゴリズムチャネルを通した客観的な検証結果を台帳として固定するアーキテクチャが有用な選択肢となります。
4. 「再実行可能な証拠」による合意形成
本成果がGitHub Actions上で「Success」として公開・維持されている事実は、ガバナンスに関する合意形成の手法に新しい基準を提示します。
自然言語で記述されたガイドラインは解釈の余地を生みやすいですが、Lean 4のコンパイラを通過した本定理群に対して反論を行う場合、自然言語上の印象論ではなく、「モデルの仮定（制約条件）」「定理の論理展開」「コードの実装」のいずれを争うのかを明確にすることが要求されます。
この証明が「再実行可能な証拠（Re-executable Evidence）」としてパブリックに配置されたことは、AIガバナンスの議論を、誰もが再計算可能で検証可能な論理の土俵へと移行させるための重要な基盤となります。