論文・技術資料

体 K 上の有限次元空間の有理写像 σ と二つの状態 s, t について、歩数の集合 Id(s, t) = {n ∈ ℤ : σⁿ s = t}（力学系の作用亜群における s から t への射の集合）を、写像を反復せずに決定する。Lyness 写像、Euler のコマの Kahan–Hirota–Kimura 離散化、面積を保つ線形写像、双曲測地線の Kahan 離散化について、任意の体（必要な場合は標数 ≠ 2）上で、保存量の各等位集合において写像がその等位集合に付随するアーベル群 A の固定された元 P による平行移動として表され、それを実現する単射な座標 ψ が存在することを、Lean 4 と Mathlib を用いて証明する。したがって σⁿ s = t は ψ(t) − ψ(s) = nP と同値である。よって歩数は離散対数として求まり、Id(s, t) は空集合か P の位数を法とする剰余類である。また ψ(s) の ⟨P⟩ を法とする類は軌道の完全不変量となる。定理は退化した等位集合（結節点を持つ曲線、可約な曲線、Euler のコマで座標が消える等位集合）も扱う。さらに次の二つの結果により、この理論は決定手続きとなる。第一に、写像が定義されない状態は各等位の有限個の明示的な状態なので、軌道が零除算に至るかどうか（状態の正則性）は、正則・非正則のいずれの場合も数個の離散対数で判定でき、正則でない状態の有限な連鎖も同じ対数から読める。第二に、部分有理写像についての還元定理により、正則性と道のないことは素数を法とする還元から ℚ に引き戻され、ℚ 上の歩数は還元でも歩数であるので、ℚ 上の問いは上界の範囲で有限個の素数と一回の厳密な反復で決まり、ある素数で道がなければ否定の答え「決して」が無条件に得られる。力学はまた、道の定数 path : Πx. Id(x, step x) を持つ Martin-Löf 型理論の小さな理論として公理化され、HoTTLean の亜群モデルで解釈される。そこで s と t の間の恒等型はちょうど集合 Id(s, t) である。開発は定理 1,146 個からなり、sorry はなく標準の公理だけを使い、健全性を Lean で証明した実行可能な証明書検査器を含む。これは、これらの問いに独立に検査できる証明書つきで答える Structure Computer の数学的基礎である。2 コアの機械で、𝔽_{2⁶¹−1} 上で 7.9 × 10¹⁵ 歩先にある状態の歩数が 0.4 秒で求まる（反復では約 96 年かかる）。

Structure Computer は、有理写像で与えられる離散力学系についての構造に関する問い（とりわけ「状態 s から状態 t には何歩で着くか、あるいは決して着かないか」）に、有限体上と有理数上で厳密に答え、すべての答えに、計算したプログラムを信頼せずに独立の検査器が確かめる証明書を付ける。Lyness 写像、Euler のコマの Kahan–Hirota–Kimura 離散化、面積を保つ線形写像、双曲測地線の Kahan 離散化については、答えは Lean で証明した定理にもとづき、保存量の等位集合に付随する群の離散対数として計算される。10¹⁷ 個の状態を持つ軌道についての問いが 1 秒未満で解け、ℚ 上では反復では得られない答え「決して」も得られる。計算し、証明書を作り、独立に検査し、すべての結果に保証の種類を付けるという同じ方針を、次の十一の問いにも適用する。可逆性、周期構造、可積分性、保存量の発見と検証、ホロノミー、整数不変量の復元、道と系の同値、共役に沿った検査済みの結果の輸送、力学の型理論の閉じた項の評価である。系は名前か短いテキストファイルで与え、見慣れない座標で書かれた系も、アフィン座標変換で既知の族に移るならその族として認識され、変換は証明書に記録されて検査器が検証し直す。𝔽_q 上の Lyness 写像については検査器が Lean で書かれ健全性を証明された第二の形で存在する。長い反復は、オプションとして、ミリ秒単位で検証できる STARK 証明で証明することもできる。小さい体上の総当たりとの比較では 12,156 組の状態で、軌道を実際にたどって得た正解と一致し 5,950 通の証明書が検査器を通った。改竄試験では改変した 1,363 件をすべて検査器が却下した。Lean の検査器と独立の検査器は、両方が読めた範囲で、2,004 通の証明書と 14,025 件の改変について判定が一致した。2 コアの機械で、𝔽_{2⁶¹−1} 上 7.9 × 10¹⁵ 歩先にある Lyness の状態の歩数が、証明書の作成と検査を含めて 0.4 秒で求まる。