「全ての未解決問題を証明する装置」を 7 段のピンに分解し、各ピンに既存研究を当てて生存判定をつけたもの。装置・チップ・回路・端子・マシンの提案は、必ずこの 7 ピンのどれかに刺さる。刺さらない提案は用途が定まっていない兆候。
「全ての未解決問題を証明する装置」は原理的に存在しない。根拠は三つ。
ただし重要な非対称がある。RH・Goldbach・Collatz などの個別問題は、どれも決定不能と証明されてはいない。障害は原理ではなく探索空間である。したがって「一様な全能機械」は不可能だが、「個別問題への装置」は正当な工学対象になる。設計目標はこう書き換わる。
目標:人間+機械の証明パイプラインの単位時間あたり通過量を上げること。および、不可能な領域を装置の外側として明示的に切り分けること。
左端の色帯は信頼等級。■ oracle 側は証明書を出せないノード(出力は「予想」以上に昇格させない)、■ certificate 側は出力に機械検査可能な証明書が付くノード。PIN 5 が信頼の基点で、ここより上流の全ての誤りはここで止まるべきという設計になっている。
#check ループ。これ以上を主張するなら差分を測る。cadical → drat-trim → cake_lpr をそのまま繋いだときの検査時間・消費電力・TCB 行数。FPGA 版はこれと同じ証明書を入力にして比較する。cadical → frat-rs / drat-trim → zstd -19 のバイト数と検査時間。ZCE 系はこれを下回るのではなく、同じバイト数を 4 口座に分解して見せることが成果物になる。300 K の Landauer 限界は kT ln2 ≈ 2.871×10⁻²¹ J/bit。不可逆ビット演算 2n 回に必要な最小エネルギーは以下(実機はこの 108–1010 倍を消費するので、あくまで下限)。
| 探索規模 | 最小エネルギー | 人間スケールでの比較 | 該当する実績 |
|---|---|---|---|
| 268 | 0.85 J | 単三電池 1 本の 1 万分の 1 | Collatz 検証の到達点 |
| 280 | 3.5×10³ J | ノート PC 数分ぶん | — |
| 2100 | 3.6×10⁹ J | 約 1,000 kWh(一般家庭の数か月) | — |
| 2128 | 9.8×10¹⁷ J | 日本の年間電力消費と同オーダー | 暗号の安全域 |
| 2160 | 4.2×10²⁷ J | 世界の年間一次エネルギーの 10⁷ 倍 | 実質的な壁 |
| 2256 | 3.3×10⁵⁶ J | 太陽の年間放射の 10²² 倍 | 不可能 |
量子計算を入れても構図は変わらない。Grover は非構造探索を二次加速するだけなので 2160 が 280 になるが、決定不能な問題は決定可能にならない。量子が効くのは周期発見に帰着する数論計算(因数分解、類群計算など)という狭い切片で、証明探索一般ではない。
Tang Nano 9K は約 8.6K LUT・0.5 Mb BSRAM 級。CDCL の学習節データベースは載らないので、PIN 4 の方向は最初から閉じている。Tang Console でも桁が変わるだけで、性質は同じ。
開くのは PIN 5 の方向だけである。LRAT の逐次検査ループは、状態が小さく・規則的・ストリーム処理なので、この規模でも1 カーネルの demonstrator として成立する。作るべきものは「速い検査器」ではなく、検査行数/ジュールとTCB 行数を測るための小さな実機である。
ASIC は検討しない。fab へのアクセスも量産理由もない。FPGA で測れる量(電力効率と TCB サイズ)だけが、規模で負けている側から出せる主張である。
SURVIVE が立っているのは PIN 5・6 と、PIN 7 の非 ATP ノード部分のみ。着手順はこうなる。
cadical → drat-trim / frat-rs → cake_lpr と zstd -19 を素直に繋ぎ、証明書バイト数・検査時間・TCB 行数を記録する。これを測る前に新機構の設計に入らない(Pattern 5 予防)。この領域は「世界初」が出やすく、そのほとんどが既に存在する。以下は本マップの時点で明示的に禁止する。