判定を下す装置を四つの欄で型付けし、較正がどの層にあるかを見る手続き。オートマトン・ウルフラム・Lean4/Mathlib・チューリングマシン・アルゲブラ／コアルゲブラの五つに当てた記録。
装置
判定器 D = (V, e, t, c) として書く。この四欄は、対象が数学の証明であれ細胞オートマトンの分類であれ同じ形で埋まる。
装置が返しうる判定の集合。二値か、多値か、順序や演算を持つか。
非ゼロの誤りを許すか。許すなら、その量が得られるか。
どの入力にも答えるか。棄権できるか。「分からない」が型にあるか。
誤り率が健全性定理で構造的に保証されるか、既知の正解に対して実測されるか。
主軸は c の二分にある。THEOREM（定理で保証）と MEASURED（実測で較正）は別物で、この区別が三件すべての判定を分けた。
オートマトンは c を持たないが e = 0 なので較正が不要。誤りを許しながら c を持たない装置が、型として最も危うい位置に立つ。
適用
番号は順序を意味する。後の件が前の件の判定を訂正しているため、読む順に依存関係がある。01–03 は c（較正）の欄を扱い、04 は t（全域性）——他の件が前提として使ってしまった欄。05 は対象ではなく型そのものの棲家で、四欄が二つに割れることを示す。
型を定義した回。停止条件較正・修正機器・Ctx チェッカの三装置を同じ四欄に載せた。
「超える」を主張できる条件は一つだけ——値域を二値に縮約し e→0 と置いたときオートマトンの判定型に一致することを示すこと。差分候補三点のうち、棄権が副情報の申告義務と結合する形だけが SURVIVE。
→ 全文を読む
Class 1–4 分類・「Class 3 = ランダム」判定・計算的既約性・PCE を、それぞれ判定器として型付けした。
四欄のうち c を一つも持たない。Weinberg・Shalizi・Mitchell・Kadanoff の批判が同じ一点に収束する理由がこれで説明できる。彼らは「複雑性の独立した定義がない」と言っているが、装置の言葉では「判定に較正がない」。ただし Culik–Yu により、クラス所属は決定不能——誤り率は未測定なのではなく一般には測定不能で、較正は宣言された族に限るほかない。
→ 全文を読む
単一の判定器ではなく層の積み重ねとして型付けした。層ごとに c の状態が違う。
前二件の論法が通らない。Lean 4 のカーネル判定は三件で最も較正されている——Mathlib は毎日、全コーパスを独立カーネルで再検証している。空いているのは Lean が保証していない層：「S の証明が正しい」は保証され、「S が意図した命題である」は保証されない。この層は benchmark では激しく測られ、Mathlib と AFP では一度も測られていない。
→ 全文を読む
他の三件が前提として使ってしまった欄。部分性が設計選択ではなく数学的必然になる、最初の装置。
sound + complete + total: pick two. HALT は半決定可能——壊れているのは全域性だけ。そして「どれだけ待ったら『停止しない』と呼ぶか」は停止条件較正の問題そのもので、その発生源がここにある。BB(5) = 47,176,870 が 2024年に Coq で全機械検証されたのが、探索し尽くして不在を確定した完成例。ただし判定器の盲点を機械サイズの関数として測った曲線は、データが公開されているのに誰も引いていない。
→ 全文を読む
五件目の対象ではない。判定器の型そのものが棲んでいる数学で、そこで四欄が二つに割れる。
Lawvere 1973 により、2値・多値・距離は「同じ定義の quantale 違い」である。「真」は距離ゼロ、「偽」は到達不能な無限の費用。だから多値の値域は設計空間ではなく、50年前からあるパラメータ。一方、量的コアルゲブラは verdict に測定された誤り率を一度も付けていない——verdict が定義そのものなので、「誤りである」という概念が存在しない。前四件がすべて c の話だったのは偶然ではなかった。
→ 全文を読む
通した結果
同じ手続きを当てて、c なし・c あり・層で分離・欄が違う・そして欄が二つに割れる、と五通りに分かれた。手続きが対象に合わせて答えを作っていない証拠として、これを残す。
適用 03 → 01。01 は「申告ゲートはすべて社会的・編集的で誤り率を持たない」と書いたが、ICMJE の臨床試験事前登録（公表の条件として事前申告を要求し、不履行は掲載不可）と MLPerf（敵対的異議申立てと公表後削除を伴う強制）の二件が出たことで、前半は弱すぎる記述だった。訂正後に残る空白は「未申告による棄権が、それ自体の発火率を実測される」ことの一点のみ。
適用 04 → 01。01 は「計算可能性で超える」を KILL したが、多くの人が使う対角線論法による反駁は無効である。対角線論法は相対化する障害であって絶対的な不可能性証明ではない。判定は維持し、根拠を Davis の deflationary dilemma と Piccinini の usability constraint に差し替えた。
適用 04 → 02。02 は計算的既約性を「反証条件なし」と判定したが、より深い問題が立つ。Blum の高速化定理により、漸近的に最適なプログラムが存在しない関数がある。すると「この関数が要求する計算量」が well-defined でなく、「近道は存在しない」という主張に指示対象がない。この接続を明示した唯一の文献は、それを切り捨てるために言及している。
適用 05 → 01（取りこぼし）。01 は「表現力で超える」の分岐に register automata や VASS を挙げながら、コアルゲブラを名指ししていなかった。オートマトンの標準的な圏論的抽象であり、分岐の最上位に来るべきだった。判定は変わらないが、理由を「既存 tool との差分が困難」から「一般化は既に完了しており、その外に出る提案が存在しない」に更新した。
適用 05 → 04。04 で「型は受理と却下の非対称を表現できない」と書いたが、それは新しい欄ではなく代数側と余代数側のどちらを見ているかの区別だった。可観測性は余代数（finality）、到達可能性は代数（initiality）。決定性オートマトンの五つ組がこの二つに割れることが具体形。
副産物
同じ型の証拠が繰り返し出た。いずれも「全員が繰り返している記述が一次資料と合っていない」事例で、一次資料 audit を前置する原則の実例として残す。
| 適用 | 広く言われていること | 一次資料 |
|---|---|---|
| 01 | B₅ の Burau 核元は 118 文字 | Bigelow 1999 の原文は "a word of length 120 in the generators"。118 の出典は見つからず |
| 02 | Li–Packard は rule 110 を Class IV に分類した | 本文では 54 と 137 を Class IV と名指ししながら、分類表では両方とも chaotic の列に入っている |
| 04 | Turing が 1936 年に停止問題の決定不能性を証明した | 彼が証明したのは circle-free 問題（Π⁰₂完全、停止問題より真に難しい）と印字問題。自己言及論法は Kleene 1952、「halting problem」の語は Davis 1958 |
撤回条件
各文書は反証条件を事前登録している。以下は三件を横断して最も効くもの。全文は各文書の該当節にある。
| 適用 | 条件 | 発火時 |
|---|---|---|
| 01 | 縮退条件が書けない（e→0 でオートマトンに戻ることを示せない） | 語を撤回 「別の判定器」に降格 |
| 01 | 未申告ゲートと誤り率を同時に持つ既存装置が一件でも出る | KILL 差分候補 (ii) |
| 02 | Zenil 2010 と TestU01 の f-module を素朴に合成して盲点閾値が出てしまう | KILL 既存 tool の compose で足りる |
| 02 | 宣言された族の外で較正を主張している | 族内に戻す Culik–Yu により外挿は不可能 |
| 03 | 2026年の Lean 証明書取り込み群との差分が明示できない | KILL 新規性主張を撤回し追試に位置づけ直す |
| 03 | Mathlib / AFP の仕様忠実度を測った既存研究が一件でも出る | KILL 残る空白が消える |
| 04 | 既存 decider を順に走らせるだけで盲点曲線が出る | KILL 既存 tool の compose で足りる |
| 04 | 「不在の証明書」を横断的に扱う枠組みが一件でも出る | KILL 差分候補 T-2 |
| 05 | 量的コアルゲブラが verdict を外部 ground truth に対して較正した例が出る | 全体が消える 五件の SURVIVE がすべて立たなくなる |
| 05 | 扱っている多値の値域が semi-primal または quantale の構造を持つ | KILL 値域の新規性主張を全面禁止 |
| 全件 | 「超える」の語が、四欄の比較以外の根拠で使われている | 語を撤回 「較正の測定」に降格 |
恒久禁止