draft v0 — 各判定は要再audit STEP 未採番 2026-09-18

適用04 — チューリングマシンを超える

t の欄。他の三件が前提として使ってしまった欄。

藤本 伸樹 ／ Rei-AIOS ／ prior-art audit v0

draft v0 — 各判定は要再audit。STEP 未採番。素材のみ。shared tree 不触。 作成: 2026-09-18 / 前提: decision-device-type-prior-art-audit-v0.md の4欄 関連: [[braid-stopping-calibration]] / [[proof-pipeline-device-map]] PIN 3・PIN 5・PIN 6 / [[collatz-analysis]]

0. 位置づけ — 他の3件が前提にしてしまった欄

前3件（オートマトン / ウルフラム / Lean4）はすべて c（較正） の話だった。本件は t（全域性） の話で、欄が違う。

四欄はオートマトンに対して定義した。オートマトンは t = 全域 が構成上そうなっている——どの入力にも必ず答える。チューリングマシンはこれを定理によって壊す。部分性が設計上の選択ではなく数学的必然になる、最初の装置がここにある。

そして「どれだけ待ったら『停止しない』と呼ぶか」は、[[braid-stopping-calibration]] の較正問題そのものである。停止条件較正 arc の発生源が t の破れにある。

1. 「超える」の分岐

分岐 内容 判定 参照
A. 計算可能性で超える オラクル、無限時間TM、BSS、Malament–Hogarth 時空 KILL（既決。根拠を訂正） §4.1
B. 資源で超える BPP、BQP、P/poly 対象外 §3.4
C. 信頼モデルで超える IP=PSPACE、MIP=NEXP、MIP*=RE CONFINE §3.3
D. t の較正で超える 停止判定器の盲点を実測する SURVIVE §3.1

2. チューリングマシンを四欄で型付け

2.1 まず正確な形

HALT = {⟨p,x⟩ : p は x 上で停止する} は Σ⁰₁完全——半決定可能だが決定可能でない。壊れているのは全域性だけである。この区別は載せる価値がある：装置は「はい」を必ず出せるが「いいえ」を必ず出せるとは限らない、という非対称がここで発生する。

2.2 四欄

欄 状態
V {halt, not-halt}。ただし二つの verdict の到達可能性が非対称（halt は半決定可能、not-halt は違う）
e 0 にできる（健全性は保てる）
t 定理により全域にできない
c 不要——ただし t を犠牲にした場合に限る。実装が棄権を持つ瞬間、棄権率の較正が必要になる

2.3 実装可能な判定器の三択——実は二択＋定義の移動

停止性を判定する装置は、全域性・健全性・完全性のうち二つしか持てない。

sound + complete + total: pick two.

そして「unknown を返す」は第三の真理値に見えるが、不完全性を三値で言い直しただけである。だから実質は二択：

この定式化に正典的な出典が見つからなかった。 二方向版（健全な停止性解析器は必ず不完全）は Wikipedia の Termination analysis と Meyer のブログにあるが、三方向の命名された定理としては存在しない。folklore として扱い、引用する場合はそう書くこと。

2.4 ★ 型に欠けているもの — verdict の非対称性

MIP*=RE（§3.3）が浮かび上がらせた問題。四欄は V を「返しうる値の集合」としか見ていないが、同じ V の中で値ごとに認識論的地位が違う場合がある。

MIP*=RE の検証者は、受理からは結論できるが却下からは何も結論できない。健全性は無条件（z ∉ L ならどんな絡み合い戦略も 1/3 を超えない）だが、完全性は prover が最適戦略を見つけて物理的に実装できることに依存し、その次元は instance から計算可能に決まらない。だから却下は「z ∉ L」と「z ∈ L だが prover が力不足だった」を区別しない。

同じ非対称は停止性にもある：半決定器の「停止した」は結論だが、「まだ停止していない」は結論ではない。

四欄は V の要素数しか見ておらず、この非対称を表現できない。型の拡張候補として §3.5 に置く。

3. 各分岐の判定

3.1 分岐 D（t の較正）→ SURVIVE

3.1.1 既存 — 較正の器はあるが、競技会は測っていない

termCOMP は構造的に測れない。 正しさが「他ツールと矛盾しない答え」として否定的に定義されており、全ツールが MAYBE を返した問題には status が付かない。分母が定義上存在しない。 棄権率自体は per-category の summary.json に YES / NO / MAYBE / timeout / error / wrong / conflicts として精密に記録されている（2025年の例：TRS Standard で AProVE25 は inconclusive 15%、NTI25 は 63%；SRS Standard で NaTT は 89%）——が、真理で条件付けられていない。

SV-COMP は測れるのに測っていない。 各タスクに expected_verdict があり、採点は UNKNOWN = 0点、FALSE 正解 +1、TRUE 正解 +2、FALSE 誤り −16、TRUE 誤り −32。棄権のコストがゼロなので、勾配が棄権へ向いている。

△ 本 audit の調査過程で SV-COMP 2025 の公開生データから導出した値（公式が公表している形ではない）：停止性カテゴリ 2339 タスクのうち、既知停止 1538 / 既知非停止 801。UAutomizer は既知停止で inconclusive 30.8%、既知非停止で 24.3%。AProVE は既知非停止で 89.4%。全体では誤答 100件 / 約51,458 判定（0.19%）に対し、inconclusive 約32,450件（63%）。 誤ることは極めて稀で、黙ることが極めて多い。そして黙りは採点されない。 引用前に再計算すること。

3.1.2 較正を実際にやった論文は3本ある

出典 何を測ったか
Chen, Cook, Fuhs, Nimkar, O'Hearn, TACAS 2014 既知非停止 81件に対し検出 51件（63%）、既知停止 254件に対し偽陽性 0。層別が明示された最もきれいな事例
Giesl et al., JAR 2017（AProVE） 停止が既知の整数プログラム 311件で失敗7＋timeout19＝棄権率 8.4%
Metta ら, arXiv:2409.12985 既知非停止の C ベンチマーク 875件に対する検出率：BOUNTY 91% / 2LS 81% / CPAchecker 75% / UAutomizer 66%。TestU01 の f-module に最も近い形

3.1.3 盲点曲線として最も近いもの

Metta ら の unwinding 深さ分布：SV-COMP の非停止ベンチマークの 75% は深さ 2〜3 で recurrent state が現れ、1000 反復超を要するのは 3%。これは「深さ k の有界手法が既知非停止集団のどれだけに届くか」の被覆曲線であり、残余も命名されている（深いカウンタ、ヒープ形状の反復、再帰）。

3.1.4 ★ そして bbchallenge には曲線が引かれていない

BB(5) の証明（§3.2）は decider ごとの内訳を n=5 についてのみ、しかもカスケード（各 decider は前段が取り逃がしたものだけを見る）として出している。decider 群を n=2,3,4,5,6 の完全な TNF 列挙に当てて UNKNOWN 率を size の関数としてプロットした公表物は存在しない。 データはすべて bbchallenge の公開 DB にある。

判定 SURVIVE：ただし「較正の方法論」は新規でない（前回 audit で確認した通り、injection–recovery / error seeding / occupancy model / TestU01 に先行がある）。新規性は「停止判定という、t が定理で壊れている場所に、この方法論が当てられていない」という一点にのみ立つ。

3.2 素材 — BB(5) は「探索し尽くして不在を機械検証した」完成例

BB(5) = 47,176,870（2024-07-02、bbchallenge Collaboration、arXiv:2509.12337）。

項目 値
Tree Normal Form での列挙数 181,385,789 台
Coq-BB5 の規模 27,274 行（+ busycoq から 10,553 行）、638 補題（+319）
ビルド時間 13コア native_compute で 約45分 ／ 単スレッド vm_compute で 約13時間
最終定理ファイル BB5_Statement.v = 121行

decider 別内訳（arXiv:2509.12337 Table 3）：

decider 非停止 停止
Loops（cyclers + translated cyclers） 126,994,099 48,379,711
n-gram Closed Position Set 6,005,142 0
Repeated Word List 6,577 0
Finite Automata Reduction (FAR) 23 0
Weighted FAR 17 0
1RB-reduction 24 0
個別証明（sporadic machines） 13 0
長時間停止機（直接シミュレーション） 0 183

Loops だけで停止機の 99.99%、非停止機の 95.48% を処理している。残り 13台（Skelet #1, #10, #17、shift overflow counter 5台、finned 5台）は個別の Coq 証明。

3.2.1 ★ 不在の証明のされ方——「証明書の山」ではない

これは外部チェッカが再生する per-machine 証明書のアーカイブではない。反射による単一の Coq 定理であり、列挙器と全 decider が Gallina プログラムとして書かれ Coq 内で健全性が証明され、Coq のカーネルが型検査中に 181,385,789 台すべてに対して実行する。

三層が入れ子になっている：

  1. 検証済みアルゴリズム層（Loops / NGramCPS / RepWL）——証明済み判定手続き、外部 witness なし
  2. 証明書検査層（FAR / WFAR）——高速な非信頼探索が外で witness を見つけ、Coq 内の検証済みチェッカが検査する。SAT の「探すのは難しく検査は易しい」形に一致するのはこの層だけ
  3. 13台の手書き証明

3.2.2 ★ 適用03 への直結 — native_compute は同じ穴

45分のビルドは native_compute を使い、これは信頼基盤に OCaml コンパイラを加える。13時間の vm_compute ビルドはカーネルのバイトコードVMを使う。これは適用03 §2.2 で扱った Lean の native_decide / Lean.trustCompiler と同じ構造の信頼交換である。

△ この信頼上の含意は本 audit の分析であって、論文がそう書いているわけではない。論文は両方の時間を報告しているのみ。

3.3 分岐 C（信頼モデル）→ CONFINE

MIP* = RE（Ji, Natarajan, Vidick, Wright, Yuen; arXiv:2001.04383 / CACM 64(11):131–138, 2021）。

abstract verbatim: "the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages."

系 verbatim: "there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value 1 or at most 1/2."

正確に言えること：古典・確率的・多項式時間の検証者が、絡み合いを共有する二つの通信しない無限能力 prover とやりとりして、特定のチューリングマシンが停止することを、それを走らせずに、実行時間の上界も持たずに確信できる。健全性は無条件——z ∉ L ならどんな絡み合い戦略も 1/3 を超えない。

正確に言えないこと（overclaim 予防に最重要）：

最も誤報される結果として記録する価値がある。「量子計算機が停止問題を解く」「絡み合いがチューリングの壁を破る」は誤り。

判定 CONFINE：これは信頼モデルの変更であって計算の変更ではない。ただし判定器の型にとっては重要で、verdict の非対称性という欠けた次元を可視化した（§3.5）。

3.4 分岐 B（資源）→ 対象外

計算可能性を変えないことを、正確な形で記録しておく。

3.5 ★ 型の拡張候補 — verdict の非対称性

§2.4 と §3.3 から出た。四欄に第五の欄を足すか、V の定義を変えるか。

装置 accept reject
オートマトン 結論 結論
半決定器 結論 結論でない（まだ、かもしれない）
MIP* 検証者 結論（健全性は無条件） 結論でない（prover の力不足と区別できない）
健全な停止性解析器 結論 「わからない」に降格済み
抽象解釈 「安全」は結論 alarm は結論でない（false alarm と区別できない）

この非対称は e（誤り率）では表現できない。 誤り率は両方向に一様な量だが、ここでの非対称は片方の verdict だけが定義上誤りえないという構造的なもの。

判定 CONFINE：片側誤り（one-sided error）という概念自体は property testing・PCP・抽象解釈に古くからある（適用01 §3 の prior art に記載済み）。新規性は「型の欄として明示する」ことにしかなく、それは記法の整理であって発明ではない。 適用01 の型定義に追記する形にとどめる。

★ 2026-09-18 追記（適用05 より）— この非対称には正確な圏論的棲家がある。 新しい欄ではなく、代数側と余代数側のどちらを見ているかの区別だった。

圏論的側 原理 最小化
可観測性（外から見える） コアルゲブラ finality / coinduction 行動的同値による商
到達可能性（作られうる） アルゲブラ initiality / induction 到達可能部分の切り出し

「受理は結論だが却下は結論でない」は「finality は到達可能性を見ない」という構造の影である。決定性オートマトンの五つ組 (Q, A, δ, q₀, F) が (Q, δ, F)＝余代数と (Q, δ, q₀)＝代数に割れることが、その具体形（[[algebra-coalgebra-audit]] §2.2）。CONFINE の判定は維持し、根拠をこの構造に差し替える。

4. ★ 前件への訂正・補強

4.1 適用01 分岐B の KILL は正しいが、根拠を1点訂正

適用01 は「計算可能性で超える」を KILL した。判定は維持されるが、多くの人が使う対角線論法による反駁は使えない。

Ord & Kieu（arXiv:math/0307020）が決定的：対角線論法は相対化する障害であって絶対的な不可能性証明ではない。「ハイパーマシンも自分自身の停止問題に直面するから自己反駁的だ」という推論は無効である。無限時間TM はチューリング停止性を決定しつつ自分自身の停止問題を持つ。Turing 次数の階層は無矛盾で豊かな構造である。

正しい根拠は二つ：

  1. Davis の deflationary dilemma（"The Myth of Hypercomputation", 2004）——提案は「非計算可能な入力を許せば非計算可能な出力が得られる」という自明な観察以上のものでないか、そうでなければハイパーコンピュテーションでない。Davis は論理的不可能性を主張していない。 主張は「分野としての中身がない」であって、この区別は載せる必要がある
  2. Piccinini の usability constraint（BJPS 2011）——有限の観測者が有限時間・有限資源で入力を指定し出力を読み出せることを要求すると、Modest PCT は経験的で反証可能な主張になり、現状生き残っている。Davis の第二の刃も同じ形：無限精度の実数の値は有限の情報では検証できないので、本物のハイパーコンピュータがあっても出力は認識論的に使えない

適用01 の該当箇所に、この訂正を反映すること。

4.2 適用02 への補強 — Blum の高速化定理

適用02 の調査では「Blum の高速化定理と計算的既約性を結びつけた研究は見当たらない」としていた。ほぼ正しかったが、例外が1件あり、しかもそれが重要。

Zwirn, Complex Systems 24(2):149–174, 2015 が唯一この接続を明示し、しかも切り捨てるためにしている。verbatim：

"it is well known that the so-called Blum speedup theorem [12] shows that for some decision problems, any program that solves the problem will be much slower than some other program solving the same problem." "But these problems are artificially constructed to prove the theorem."

彼はその上で Blum 高速化を仮定によって排除し、「自然な問題」に限定することで初めて計算的既約性を定義できるようにしている。

含意（適用02 の主張を強める）：Blum の定理は「必要最小の計算量」という概念そのものへの潜在的な障害である。ある関数に漸近的に最適なプログラムが存在しないなら、「この関数が要求する計算量」は well-defined でなく、計算的既約性（近道は存在しない）に指示対象がない。Zwirn はこれを見て宣言で処理した。誰もこれを批判として展開していない。

Gorard の Slowdown Theorem（Complex Systems 27(2), 2018）も Blum を引用していない。

適用02 §2.3（計算的既約性の四欄）に、この論点を追記すること。 「反証条件なし」に加えて「そもそも指示対象があるか未確定」が立つ。

4.3 ★ 副産物 — Turing 1936 は停止問題を証明していない

Hamkins & Nenu, "Did Turing prove the undecidability of the halting problem?", Journal of Logic and Computation 36(1), art. exaf075, 2026（preprint arXiv:2407.00680）。

Turing が 1936年に実際に証明したのは：

Turing がやっていないこと：停止問題を述べること、その語を使うこと、いま標準的な自己言及構成を (program, input) の一様な決定問題についての定理として与えること。

自己言及論法は Kleene（Introduction to Metamathematics, 1952）。「halting problem」の語を活字にしたのは Martin Davis（Computability and Unsolvability, 1958）。

Hamkins & Nenu の判定：Turing への帰属は限定付きなら "completely fine"（道具は全部彼が用意し、同値な結果を証明した）が、文字通りの帰属は歴史的に誤り。

これは前2件で見つけた Li–Packard の rule 137 や Bigelow の 120文字と同じ型の証拠——全員が繰り返している帰属が一次資料と合っていない事例。適用04 の較正素材として、また「一次資料 audit を前置する」原則の実例として価値がある。

5. 差分候補 — 証明書サイズは「不在の構造の量」を測る

5.1 ★ 最も強い発見

「X が起こらないことの証明書」を SAT・停止性・網羅探索を横断して一つの範疇として扱う枠組みは存在しない。 探して見つからなかった（不在証明ではない）。

存在するのは互いを包含しない四つの枠組み：

  1. Certifying algorithms（McConnell, Mehlhorn, Näher, Schweitzer, Computer Science Review 5(2):119–161, 2011）——最も一般的で、肯定・否定の答えを明示的に対称に扱う（二部性の witness は yes なら二分割、no なら奇閉路）。ただしアルゴリズム中心で SAT/停止性/探索に踏み込まない
  2. 証明複雑性——理論的な本籍地だが、別々の証明系として扱い、工学的な一範疇としては扱わない
  3. Certifying model checking（Namjoshi CAV 2001 ／ Froleyks ら CAV 2025）——最も運用的に成熟。共通形式・チェッカ・サイズ統計を持つ。モデル検査に限定
  4. 認証済みツール生態系（IsaFoR/CeTA + CPF ／ DRAT/LRAT + 検証済みチェッカ）——成熟しているが領域ごとに孤立し形式が非互換

5.2 ★ そして証明書サイズが三層に割れる

設定 対象 証明書 比
FAR（bbchallenge） 30バイトのTM DVF レコード：方向1バイト + DFA表 2n バイト、n ≤ 12 → 証明データ25バイト以下 約 1×
HWMCC'24 witness circuit AIGER モデル 帰納的不変量回路 幾何平均 1.74×、8割超が 2× 未満
k-induction witness（CAV'21） 回路 k-witness circuit 約 1.5×
DRAT/LRAT CNF（数MB） Pythagorean triples 200TB（圧縮68GB）／Schur 5 約2PB 10⁶〜10⁹×

含意：証明書サイズは「不在を証明すること」の性質ではない。不在がどれだけ構造を持っているかの性質である。

そして DRAT/LRAT だけが外れ値である理由が構造的に説明できる。他は全部同じ手を使っている——到達可能集合を上から（または co-到達可能集合を下から）近似し、閉じていて bad を外す集合を出し、閉性を局所的に検査する。FAR の条件 (4.10)–(4.12)、Certifaiger の Base/Step、CeTA の「書き換えで閉じた正規言語」、IC3 の帰納的不変量は文字どおりこれ。DRAT/LRAT は閉集合を提示する代わりに反駁を列挙する。だから 10⁶ 倍大きい。

PIN 6（圧縮・可読化）への直結：STEP 1886 の compose baseline は LRAT に固定されている。上の観察が正しければ、LRAT の巨大さは圧縮で縮める対象ではなく、証明書形式の選択によって桁で変わる量である。圧縮率の測定と並べて「なぜこの形式を選んだか」を申告する欄が要る。

5.3 差分候補の判定

候補 内容 判定
T-1 停止判定器の盲点曲線（機械サイズに対する UNKNOWN 率）を bbchallenge の公開データで引く SURVIVE（狭い）。方法論は既存（TestU01 / injection–recovery）。新規性は「t が定理で壊れている場所に当てられていない」一点のみ
T-2 「不在の証明書」の統一枠組み＋証明書サイズを構造量の指標として提示 SURVIVE。四枠組みは互いを包含せず、横断的定式化が見当たらない。ただし §5.2 の「同じ手」という観察が既出でないかの確認が要る
T-3 verdict の非対称性を型の欄として明示 CONFINE。片側誤りの概念は古い。記法の整理であって発明でない

6. 最小形

新 arc は立てない。bbchallenge の公開データで盲点曲線を1枚引くのが最小。

  1. decider 群（Loops / NGramCPS / RepWL / FAR）を n = 2,3,4,5 の完全な TNF 列挙に当てる
  2. カスケードでなく独立に当てる——各 decider が単体で何%を決定できるかを size の関数として出す
  3. UNKNOWN 率を size に対してプロットする
  4. n=6 については、現在の未決 964〜1101台と cryptid 20台を residue として併記する
  5. 申告欄を verdict の一部にする（どの decider を、どの深さまで、どの列挙に対して走らせたか）

データはすべて公開されている。計算量は BB(5) の再証明（45分〜13時間）より小さい。compose baseline は「既存 decider を順に走らせて UNKNOWN を数える」で、それで曲線が出るなら T-1 は KILL。

7. 反証条件（事前登録）

# 条件 発火時の処置
(a) bbchallenge か隣接コミュニティが decider の size 別 UNKNOWN 率を既に公表している T-1 を KILL
(b) 既存 decider を順に走らせるだけで曲線が出る T-1 を KILL（Pattern 5）
(c) §5.2 の「すべて同じ手（閉集合の局所検査）」という観察が既出 T-2 を CONFINE に降格
(d) 「不在の証明書」を横断的に扱う枠組みが1件でも出る T-2 を KILL
(e) Hamkins & Nenu の帰属訂正が査読で覆る §4.3 を撤回
(f) 「チューリングマシンを超える」の語が、§2 の四欄と t の破れ以外の根拠で使われている 語を撤回。「停止判定の較正」に降格

恒久禁止事項（Pattern L 予防）：

8. 引用一覧

✓ = 本 audit で直接確認 / △ = 二次情報・要確認

直接確認 ✓

二次情報・要確認 △

9. この audit の限界