よくある質問

数値シミュレーションとは何が違うのか

数値シミュレーションは、浮動小数点で軌道を近似的にたどり、「これから何が起きるか」を答える。Structure Computer は、誤差のない数（有限体と有理数）で計算し、「どこに着くか、決して着かないか」「何が変わらないか」を、証明書つきで答える。

一方で、有限体には大小も距離もないので、軌道がどれだけ近づくか、誤差がどう広がるかといった「近さ」の問いには答えない。数値シミュレーションの代わりではなく、それを補うものである。

数式処理システムは式を正確に計算できるが、その答えに、ほかの人が独立に確かめるための証明書は付かない。また、「s から t へ何歩で着くか」のような問いには、一般には軌道を 1 歩ずつたどるしかない。系ごとに専門的な数学の変換を手で組めば答えられる場合もあるが、それを自動で行う汎用の仕組みはない。

Structure Computer は、既知の族については、Lean で証明した定理にもとづいて軌道をたどらずに答え、証明書を付ける。ℚ 上の「決して着かない」のように、たどる方法ではいつまでも結論が出ない問いにも答える（高度な例題）。

有限体では値がいつも 0 から q − 1 の整数で、丸め誤差がなく、状態の数も有限になる。ℚ（分数）の問いにも答える。体は試すページで選べる。

q は素数なら何でもよい。

既知の族なら、大きい q でもよい。Lyness 写像は q ≈ 2⁶¹ でも 1 秒以内で答える。Euler のコマは q ≈ 2⁴⁰ で 1 秒以内、2⁴⁵ 程度までが実用の範囲である。
既知の族でない系は、軌道を 1 歩ずつたどるので、軌道が歩く上限（既定 100 万歩）に収まる小さめの q を選ぶ。
Q2（周期構造）は、状態の数が少ないときだけ、すべての状態を数えて確定で答える。

変数の数だけ、カンマで区切って数を並べる（例：2, 5）。分数も書ける。𝔽_q では、分数や負の数は q を法とした値として扱う（q = 1009 なら 1/2 は 505、−1 は 1008）。

理由がカードに出る。よくある理由は次のとおり。

Q6（ホロノミー）は、系ファイルで対称性を宣言した系だけに答える。宣言の書き方は「系ファイルの書き方」にある。

Q7 と Q11 は、選んだ体によらず、いつも ℚ 上の歩数について答える。𝔽_q で「着く」状態の組でも、ℚ 上では「着かない」ことがあるので、答えが違って見えることがある。

大きい q での Q2（周期構造）や、式の大きい系での Q3（可積分性）には、数分（長いと 10 分近く）かかることがある。1 問の上限は 10 分で、カードの「取り消す」で止められる。Id(s, t) は既知の族なら多くの場合 1 秒以内に答える。

計算サーバーは多くの人で共有しているので、1 人が同時に動かせる計算の数と、短い時間に送れる計算の数に上限がある。「全部計算する」1 回分は上限におさまる。上限に達したときは、表示される秒数ほど待つか、動いている計算が終わってからもう一度試す。

試すページの「保存量の次数の上限」を上げると、より高い次数の式も探す。多項式の保存量については「これで全部か」まで確定で答えるが、分数の形の保存量は、見つけたものを挙げるだけで、全部とは限らない。

そのまま入力してよい。既知の族は、座標を取り替えて書かれていても見抜かれる。見抜かれなければ、軌道をたどって答える。

確定の答えは、検査器が証明書を確かめ、Lean で証明した定理から従うものである。何を信頼の土台にしているか、どこが証明されていないかは、「証明書と検査」にまとめてある。

保存して、あとで検査し直したり、ほかの人に渡して検査してもらったりできる。試すページの検査の道具に読み込むと、計算した側を信じなくても答えを確かめられる。