実在しない機械から機構だけを引き剥がして使えるか。ジョン・タイターの C204 と、 惑星ウンモの IBOZOO UU を標本に、抽出と投影を分ける篩を作り、抜いた骨を Lean 4 で検定し、 動く模型に落とすところまでをやった記録です。
最初、私はこの類を「記述しかないので取り出す物がない」と整理しました。それが取り違えでした。 残余ゼロというのは分解の抵抗がゼロという意味です。実機は物理的制約と設計者の癖が絡み合っていて機構を剥がしにくい。 空想の機械は最初から骨組みしかないので、すでに抽象化が済んでいる。
この方法自体には重い前例があります。マクスウェルの悪魔は実在しませんが、そこから情報と熱力学の接続が生まれた。 チューリング機械に至っては、無限テープという物理的に不可能な仕様書でありながら計算の定義そのものになりました。 実在しない機械が最も遠くまで届いた例が、計算機科学の土台に座っている。
性格が正反対の二つを並べました。片方は機械の仕様書で、原理の説明が薄い代わりに操作的な数が置いてある。 もう片方は物理体系のほうが本体で、語彙は豊かだが数がひとつも出てこない。
この方法の失敗様式は一つに集約されます。抽出は投影と見分けがつきにくい。 骨が綺麗に出てきたとき、それは元の文書に骨があったからなのか、こちらが持っていた骨を投影したからなのか、 文書の側からは決まりません。出所の検証は原理的に無理なので、判定基準を別に置きました。
| 問い | C204 | IBOZOO UU |
|---|---|---|
| 数は出るか導出でなくてよい。操作的な意味を持つ数がひとつでもあるか | ○10 年/時、1〜2%、質量で変わる消費 | ×数値がひとつも出ない |
| 参照を切っても立つか元の文書に一切触れずに骨を述べられるか | ○いずれも独立に述べられる | ○関係的前幾何としてなら立つ |
| 外れられるか形式化したとき、偽になりうる命題が出てくるか | △機械の仕様なので該当が薄い | ×合成規則が無く定義が閉じない |
三つ目が実質的に一番効きます。証明支援系は難易度の前に良設定性を弾くので、篩の実装がそのまま既存の作業になる。 そしてここから一般則が出ます。本物の先進性は現在の物理より具体的になる ── 数が出る。 偽の先進性は必ず逆に振れて、語彙が増えて数値が減る。
IBOZOO UU の「孤立した軸束は存在しない」「意味は他との角度差にのみ宿る」は、無自性・縁起とほぼ同型です。 D-FUMT₈ で ¬N = N、つまり否定しても真に戻らないのは、 空を否定しても有に戻らないという中観の運動の形式化として素直に効きます。
ただし重なるのは半分だけです。龍樹は「関係こそが実在である」とは言っていません。 IBOZOO UU は点から自性を剥がして関係に移し替えた体系で、実体を置く構えは残っている。 位置づけとしては中観よりも華厳の因陀羅網に近い。似て見えるのは、否定の段階までは同じ道を通るからです。
実務的な線引きはこうなります。否定側 ── 位置を持たない、孤立しない、絶対枠が無い ── は中観の裏付けで安全に持っていける。 肯定側 ── 関係が実体である ── は華厳の像であって、中観の保証は付いてこない。 そして ⟲ をどこに置くかは、龍樹が答えをくれない場所として残ります。
⟲ ∧ ⊤ = ⟲⟲ ∧ N = ⟲⟲ ∧ 〜 = ⟲⟲ ∨ ⊥ = ⟲
⟲ は AND でも OR でも吸収元。記憶からの再生ではなく、実装の表を直接引いた値です。
これで選択肢がほぼ決まります。⟲ を入力側のどこかに置くと、そこから先が全部 ⟲ になる。 一箇所でも辺のラベルに許した瞬間、その辺を通る合成はすべて潰れて、体系が何も言わなくなります。
採用理由は四つあります。吸収性と整合する（出力側にしか現れないなら、吸収は終端の印になる）。 関係だけから定義できる（閉路は辺の並びで、余分な要素を要求しない）。 独立に立つ（点ごとの値ではなく閉路の合成に物理的内容が宿るのは、ゲージ理論のホロノミーとウィルソンループそのもので、ウンモを参照せずに述べられる）。 そして「反復する意味は自身を超える」から導出される ── 閉路は反復が戻る形そのものなので、公理として置くのではなく出てくる。
IBOZOO UU 型の関係的前幾何に D-FUMT₈ を乗せた最小構成。⟲ が閉路からしか出ないことの形式的保証。
C204 操作卓・IBOZOO UU 空間・断面図の三部構成。外部音源ゼロで BGM と効果音を生成。
形式化で効いたのは、証明を書く前の型設計でした。辺ラベルの型 Label に SELF を構成子として持たせない。合成 Label.comp の値域も Label にする。これで「⟲ は原始ラベルに現れない」「合成それ自体は ⟲ を作れない」が 証明ではなく構造として保証されます。残ったのが主定理です。
theorem self_only_from_cycle (G : Pregeom V) (w : List V) (h : compose G w = D8.SELF) : isClosed w = true ∧ 3 ≤ w.length -- ⟲ が出たなら閉じている。⟲ は錨ではなく結果である。